Question

In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.

One technique used, that has shown good results in practice, is random restart. Intuitively, randomly restarting means there is a chance of getting luckier with guessing the right variable assignments that would lead to a quick solution.

The same intuition suggests this should be much more effective when the problem instance is in fact satisfiable (so you only need to guess a set of variable assignments that constitute a solution) than if it is not (so in principle you have to check all possible assignments anyway, modulo sections of the search space that can be skipped via techniques like unit propagation and non-chronological backtracking, which are at least not obviously sensitive to the initial guesses).

Is the second intuition correct? Are random restarts in fact much more effective, on average, in cases where the problem instance is in fact satisfiable?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top