Published in

Association for Computing Machinery (ACM), ACM Computing Surveys, 3(55), p. 1-34, 2023

DOI: 10.1145/3491210



Export citation

Search in Google Scholar

On the Structure of the Boolean Satisfiability Problem: A Survey

Journal article published in 2023 by Tasniem Nasser Alyahya, Mohamed El Bachir Menai, Hassan Mathkour
This paper was not found in any repository, but could be made available legally by the author.
This paper was not found in any repository, but could be made available legally by the author.

Full text: Unavailable

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO


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.