Towards a Theoretical Understanding of the Power of Restart in SAT solvers

Abstract

Restart policy is a widely used class of techniques integral to the efficiency of conflict-driven clause-learning (CDCL) SAT solvers. While the utility of such policies has been well-established, to-date we still lack a deep theoretical understanding of why restart policies are crucial to the power of CDCL SAT solvers.

In this paper, we provide a series of results that theoretically establish the power of restarts for various models of Boolean SAT solvers. More precisely, we make the following contributions. First, we show that certain model of CDCL solvers with restarts are no more powerful from a proof-complexity theoretic point of view than the same configurations without restarts. Second, we define \textit{decision depth} for DPLL proofs of an unsatisfiable formula $\varphi$, and then we relate decision depth of $\varphi$ and size of DPLL proofs (or the running time of a DPLL based solver) for $\varphi$. Third, we introduce a new class of satisfiable instances called $Ladder_n$, then we use decision depth as a tool to proved that a drunk style DPLL solver with restarts can solve $Ladder_n$ in polynomial time with high probability while the solvers with the same configuration without restarts have exponential run time with high probability. Finally, the crucial insight that drives this line of research is the fact that restarts add proof-theoretic or algorithmic power to solver configurations by compensating for the weaknesses of some other important heuristics like branching or value selection or clause learning.