G2SAT: Learning to Generate SAT Formulas (NeurIPS 2019)
The Boolean Satisfiability (SAT) problem is the canonical NP-complete problem that is fundamental to Computer Science. Developing and evaluating practical SAT solvers relies on extensive empirical testing on a set of real-world benchmark formulas. However, the number of such real-world SAT formulas is limited, and while augmenting benchmark formulas via synthetic SAT formulas is possible, existing approaches are heavily hand-crafted and cannot simultaneously capture a wide range of characteristics of real-world SAT formulas. Here we present G2SAT, the first deep generative framework that learns to generate SAT formulas from a given set of input formulas. The core of G2SAT is a novel deep generative model for bipartite graphs, which generates graphs via iterative node merging operations. We show that G2SAT can generate SAT formulas that closely resemble given real-world SAT formulas, as measured by both graph metrics and SAT solver behavior. Furthermore, we show that our synthetic SAT formulas can be used to improve SAT solver performance on real-world benchmarks, which opens up new opportunities for the continued development of SAT solvers and a deeper understanding of their performance.