On the Structure of the Boolean Satisfiability Problem: A Survey

The Boolean satisfiability problem (SAT) is a fundamental NP-complete decision problem in automated reasoning and mathematical logic. As evidenced by the results of SAT competitions, the performance of SAT solvers varies substantially between different SAT categories (random, crafted, and industrial). A suggested explanation is that SAT solvers may exploit the underlying structure inherent to SAT instances. There have been attempts to define the structure of SAT in terms of structural measures such as phase transition, backbones, backdoors, small-world, scale-free, treewidth, centrality, community, self-similarity, and entropy. Still, the empirical evidence of structural measures for SAT has been provided for only some SAT categories. Furthermore, the evidence has not been theoretically proven. Also, the impact of structural measures on the behavior of SAT solvers has not been extensively examined. This work provides a comprehensive study on structural measures for SAT that have been presented in the literature. We provide an overview of the works on structural measures for SAT and their relatedness to the performance of SAT solvers. Accordingly, a taxonomy of structural measures for SAT is presented. We also review in detail important applications of structural measures for SAT, focusing mainly on enhancing SAT solvers, generating SAT instances, and classifying SAT instances.

Automated summary

The Boolean satisfiability problem (SAT) is a fundamental NP-complete decision problem, and SAT solvers' performance may vary due to the underlying structure of SAT instances. Previous studies have attempted to define the structure of SAT using measures such as phase transition, backbones, backdoors, small-world, scale-free, treewidth, centrality, community, self-similarity, and entropy, but the empirical evidence is limited to certain SAT categories and lacks theoretical proof. Furthermore, the impact of structural measures on SAT solvers' behavior has not been extensively studied. This work provides a comprehensive study on structural measures for SAT, including an overview of related works, a taxonomy of measures, and detailed applications in enhancing SAT solvers, generating SAT instances, and classifying SAT instances.