Relating Complexity-theoretic Parameters with SAT Solver Performance

TL;DR

This paper empirically evaluates how various structural parameters relate to CDCL SAT solver performance on large benchmarks, introduces a new parameter, and explores their combined explanatory power.

Contribution

It provides a comprehensive empirical comparison of structural parameters, introduces the LSR backdoor concept, and analyzes their impact on solver efficiency.

Findings

Certain parameter combinations improve regression models of solver time.

Some parameters serve as better insights into heuristic efficiency.

Minimal LSR-backdoors can be exponentially smaller than minimal-LS backdoors.

Abstract

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. Our study led us to several results. First, we show that while such parameters only weakly correlate with CDCL solving time, certain combinations of them yield much better regression models. Second, we show how some parameters can be used as a "lens" to better understand the efficiency of different solving heuristics. Finally, we propose a new complexity-theoretic parameter, which we call learning-sensitive with restarts (LSR) backdoors, that extends the notion of learning-sensitive (LS) backdoors to incorporate restarts and discuss algorithms to compute them. We mathematically prove that for certain class of instances minimal LSR-backdoors are exponentially smaller than minimal-LS backdoors.