Edward
Zulkoski,
PhD
candidate
David
R.
Cheriton
School
of
Computer
Science
Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instances. While some of these parameters have been studied empirically, until now there has not been a unified comparative study of their explanatory power on a comprehensive benchmark. We correct this state of affairs by conducting a large-scale empirical evaluation of CDCL SAT solver performance on nearly 7000 industrial and crafted formulas against several structural parameters such as backdoors, treewidth, backbones, and community structure.
We first show that while such parameters only weakly correlate with CDCL solving time, certain combinations of them yield much better regression models. Further, we show how some of these parameters can be used as a “lens” to better understand the effects of different solving heuristics. We experiment over three branching heuristics and three restart policies, and demonstrate their effect on solver performance.