MASc Seminar: Towards a Theoretic Understanding of the Power of Restart in SAT solvers

Thursday, August 1, 2019 3:00 pm - 3:00 pm EDT (GMT -04:00)

Candidate: Chunxiao Li

Title: Towards a Theoretic Understanding of the Power of Restart in SAT solvers

Date: August 1, 2019

Time: 3:00pm

Place: EIT 3142

Supervisor(s): Ganesh, Vijay

Abstract:

Restarts are 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 empirically, to-date we still lack a deep theoretical understanding of why restart policies are crucial to the power of CDCL SAT solvers. 

This thesis first presents studies on three classes of formulas which were conjectured to be able to exponentially separate a solver configuration S with restarts and S with no restarts. We prove that these candidates classes of formulas are not even sufficient to super-polynomially separate the two solver configurations. 

We then provide a series of results that theoretically provide evidences for establishing the power of restarts for various models of Boolean SAT solvers. More precisely,  we make the following contributions. First, we introduce a new class of satisfiable instances called Ladder_n and use it to construct another formula F_T, and prove that for the drunk randomized DPLL SAT solver D (introduced by Alekhnovich and Razborov), the configuration D with restarts can solve Ladder_n formulas in sub-exponential time in size of Ladder_n, while D without restarts requires exponential time in the size of Ladder_n, with high probability. Two crucial insights enabled us to prove this separation result for restarts: first, we changed the focus from unsatisfiable instances to satisfiable ones; second, we observed that, at least for the models we considered, restart heuristics add proof-theoretic or algorithmic power by compensating for the weaknesses in some other important heuristic like value selection. Second, we introduce a key new notion used in above-mentioned proofs, called Decision Complexity dc(F), for DPLL proofs of an unsatisfiable formula F and show that size of DPLL proofs of F are lower bounded by 2^dc(F).