G2SAT: Learning to Generate SAT Formulas
Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, Jure, Leskovec

TL;DR
G2SAT is a deep generative framework that learns to produce realistic SAT formulas from input data, aiding in solver development and understanding by creating synthetic benchmarks that resemble real-world instances.
Contribution
This work introduces G2SAT, the first neural network-based method to generate SAT formulas that mimic real-world instances using graph representations.
Findings
G2SAT generates SAT formulas closely resembling real-world instances.
Synthetic formulas improve SAT solver performance on benchmarks.
The approach captures characteristics of real SAT formulas through graph metrics.
Abstract
The Boolean Satisfiability (SAT) problem is the canonical NP-complete problem and is fundamental to computer science, with a wide array of applications in planning, verification, and theorem proving. Developing and evaluating practical SAT solvers relies on extensive empirical testing on a set of real-world benchmark formulas. However, the availability of such real-world SAT formulas is limited. While these benchmark formulas can be augmented with synthetically generated ones, existing approaches for doing so are heavily hand-crafted and fail to simultaneously capture a wide range of characteristics exhibited by real-world SAT instances. In this work, we present G2SAT, the first deep generative framework that learns to generate SAT formulas from a given set of input formulas. Our key insight is that SAT formulas can be transformed into latent bipartite graph representations which we…
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.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Data Visualization and Analytics · Software Engineering Research
