On the Hierarchical Community Structure of Practical Boolean Formulas
Chunxiao Li, Jonathan Chung, Soham Mukherjee, Marc Vinyals, Noah, Fleming, Antonina Kolokolova, Alice Mu, Vijay Ganesh

TL;DR
This paper introduces Hierarchical Community Structure (HCS) parameters to characterize the recursive community structure of Boolean formulas, demonstrating strong correlation with solver performance and offering insights into the structure of industrial SAT instances.
Contribution
It proposes HCS-based parameters that are both strongly correlative with solver runtime and possess good theoretical properties, bridging the gap between empirical observations and theoretical rigor.
Findings
HCS parameters are strongly correlated with solver run time.
A classifier using HCS parameters accurately distinguishes industrial from random instances.
Theoretical analysis shows HCS avoids issues of traditional community measures.
Abstract
Modern CDCL SAT solvers easily solve industrial instances containing tens of millions of variables and clauses, despite the theoretical intractability of the SAT problem. This gap between practice and theory is a central problem in solver research. It is believed that SAT solvers exploit structure inherent in industrial instances, and hence there have been numerous attempts over the last 25 years at characterizing this structure via parameters. These can be classified as rigorous, i.e., they serve as a basis for complexity-theoretic upper bounds (e.g., backdoors), or correlative, i.e., they correlate well with solver run time and are observed in industrial instances (e.g., community structure). Unfortunately, no parameter proposed to date has been shown to be both strongly correlative and rigorous over a large fraction of industrial instances. Given the sheer difficulty of the problem,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Engineering Research · Formal Methods in Verification · Constraint Satisfaction and Optimization
