Exploiting Structure: A Survey and Analysis of Structures and Hardness Measures for Propositional Formulas

The Boolean satisfiability problem (SAT) and its many variations lie at the core of many algorithmic problems in both academia and industry. Due to being NP-complete, general instances of SAT cannot be solved efficiently. However, exploiting certain structures or properties of a formula can greatly accelerate the computation of solutions or serve as a measure for the hardness of a SAT instance. In this paper, we describe and discuss such exploitable properties and structures. First, we describe known exploitable structures found in propositional formulas like blocked clauses, unit clauses, pure literals, backbones, and autark assignments. Second, we describe hardness indicators for propositional formulas such as the variable-to-clause ratio, as well as advanced structural measures like centrality, modularity, and self-similarity. In particular, we give an overview on the selected structures and measures and discuss their applications. We also identify relationships between them to clarify their complex interactions and potential for use in solvers.