G2SAT: Learning to Generate SAT Formulas.

Area of Science:

• Computer Science
• Artificial Intelligence
• Computational Complexity

Background:

• The Boolean Satisfiability (SAT) problem is a fundamental NP-complete problem with applications in AI, planning, and verification.
• Practical SAT solver development requires extensive testing on real-world benchmark formulas, but their availability is limited.
• Existing methods for generating synthetic SAT formulas are often hand-crafted and fail to capture the complexity of real-world instances.

Purpose of the Study:

• To introduce G2SAT, the first deep generative framework for synthesizing SAT formulas.
• To address the limitations of current synthetic SAT formula generation techniques.
• To improve the development and evaluation of SAT solvers through realistic synthetic data.

Main Methods:

• Representing SAT formulas as latent bipartite graphs.
• Utilizing a specialized deep generative neural network to model these graph representations.
• Training the generative framework on a dataset of input formulas.

Main Results:

• G2SAT generates synthetic SAT formulas that closely mimic real-world instances based on graph metrics and SAT solver behavior.
• The generated formulas effectively augment real-world benchmarks.
• The synthetic formulas demonstrate potential for improving SAT solver performance.

Conclusions:

• G2SAT offers a powerful new approach for generating realistic SAT formulas.
• This framework can significantly aid in the empirical testing and development of SAT solvers.
• The ability to generate diverse and representative SAT instances opens avenues for deeper understanding of solver performance and advancement.