Random restarts for unsatisfiable instances

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?

Answer 1

There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from knowledge gained about persistently troublesome conflict variables sooner than backjumping would otherwise allow the partial assignment to be similarly reset. In effect, restarts allow the discovery of shorter proofs of unsatisfiability on average.