Edward
Zulkoski,
PhD
candidate
David
R.
Cheriton
School
of
Computer
Science
We present two new characterizations of SAT formulas. The first, called “mergeability,” denotes the proportion of input clauses that resolve and merge (i.e., the two clauses share both an opposing literal and a common literal). Merge resolutions are important, as the resolvent of the resolution will have a size smaller than the two original clauses. We present a formula generator capable of scaling mergeability (given a “seed formula”), and show that mergeability tends to negatively correlate with solving time, particularly for unsatisfiable formulas.
The second characterization, called “learning-sensitive with restarts (LSR) backdoors,” describes the minimal set of variables that a CDCL solver must branch upon in order to solve the formula. LSR backdoors extend “learning-sensitive (LS) backdoors” to naturally allow restarts during search. We demonstrate an exponential separation between the size of LSR and LS backdoors, under the assumption that the solver cannot backjump. We further show that the backdoor size is dependent on the underlying clause-learning scheme. Empirically, we demonstrate that solvers that restart often tend to branch on fewer unique variables overall, but this does not necessarily improve performance.