The Effect Of Structural Measures And Merges On Sat Solver Performance

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 treewidth, community structure parameters, and a measure of the number of "mergeable" pairs of input clauses. We first show that while most of these parameters correlate well with certain sub-categories of formulas, only the merge-based parameters seem to correlate well across most classes of industrial instances. To further methodically test this connection, we perform a scaling study of mergeability of randomly-generated formulas and CDCL solver running time. We show that as the number of resolvable merge pairs are scaled up for randomly-generated instances while keeping most properties invariant, unsatisfiable instances show a very strong negative correlation with solver runtime. We further show that there is strong negative correlation between the size of learnt clauses and the number of merges as the number of merge pairs are scaled up. A take-away of our work is that mergeability might be a powerful complexity theoretic parameter with which to explain the unusual efficiency of CDCL SAT solvers.