Understanding and Enhancing CDCL-based SAT Solvers

SAT Solvers;Backdoors;Computer Algebra Systems

Zulkoski, Edwardadvisor:Czarnecki, Krzysztof ; affiliation1:Faculty of Mathematics ; advisor:Ganesh, Vijay ; Ganesh, Vijay ; Czarnecki, Krzysztof ;

University of Waterloo

关键词: Computer Algebra Systems;    Backdoors;    SAT Solvers;    Doctoral Thesis;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/13525/3/Zulkoski_Edward.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

Modern conflict-driven clause-learning (CDCL) Boolean satisfiability (SAT) solvers routinelysolve formulas from industrial domains with millions of variables and clauses, despite the Booleansatisfiability problem being NP-complete and widely regarded as intractable in general. At thesame time, very small crafted or randomly generated formulas are often infeasible for CDCLsolvers. A commonly proposed explanation is that these solvers somehow exploit the underlyingstructure inherent in industrial instances. A better understanding of the structure of Booleanformulas not only enables improvements to modern SAT solvers, but also lends insight as to whysolvers perform well or poorly on certain types of instances. Even further, examining solversthrough the lens of these underlying structures can help to distinguish the behavior of differentsolving heuristics, both in theory and practice.The first issue we address relates to the representation of SAT formulas. A given Booleansatisfiability problem can be represented in arbitrarily many ways, and the type of encoding canhave significant effects on SAT solver performance. Further, in some cases, a direct encodingto SAT may not be the best choice. We introduce a new system that integrates SAT solvingwith computer algebra systems (CAS) to address representation issues for several graph-theoreticproblems. We use this system to improve the bounds on several finitely-verified conjecturesrelated to graph-theoretic problems. We demonstrate how our approach is more appropriate forthese problems than other off-the-shelf SAT-based tools.For more typical SAT formulas, a better understanding of their underlying structural properties,and how they relate to SAT solving, can deepen our understanding of SAT. We perform a largescaleevaluation of many of the popular structural measures of formulas, such as communitystructure, treewidth, and backdoors. We investigate how these parameters correlate with CDCLsolving time, and whether they can effectively be used to distinguish formulas from differentdomains. We demonstrate how these measures can be used as a means to understand the behaviorof solvers during search. A common theme is that the solver exhibits locality during searchthrough the lens of these underlying structures, and that the choice of solving heuristic can greatlyinfluence this locality. We posit that this local behavior of modern SAT solvers is crucial to theirperformance.The remaining contributions dive deeper into two new measures of SAT formulas. We firstconsider a simple measure, denoted ;;mergeability,” which characterizes the proportion of inputclauses pairs that can resolve and merge. We develop a formula generator that takes as input a seedformula, and creates a sequence of increasingly more mergeable formulas, while maintaining manyof the properties of the original formula. Experiments over randomly-generated industrial-likeinstances suggest that mergeability strongly negatively correlates with CDCL solving time, i.e., as the mergeability of formulas increases, the solving time decreases, particularly for unsatisfiableinstances.Our final contribution considers whether one of the aforementioned measures, namely backdoorsize, is influenced by solver heuristics in theory. Starting from the notion of learning-sensitive(LS) backdoors, we consider various extensions of LS backdoors by incorporating different branchingheuristics and restart policies. We introduce learning-sensitive with restarts (LSR) backdoorsand show that, when backjumping is disallowed, LSR backdoors may be exponentially smallerthan LS backdoors. We further demonstrate that the size of LSR backdoors are dependent on thelearning scheme used during search. Finally, we present new algorithms to compute upper-boundson LSR backdoors that intrinsically rely upon restarts, and can be computed with a single run ofa SAT solver. We empirically demonstrate that this can often produce smaller backdoors thanprevious approaches to computing LS backdoors.