# G2SAT: Learning to Generate SAT Formulas

arXiv: https://arxiv.org/abs/1910.13445 · HTML: https://mlsanity.com/paper/1910.13445/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Oct 2019.

## Built on by (most cited first, 20 of 20)

- [Identity-aware Graph Neural Networks](https://mlsanity.com/paper/2101.10320/) (2021)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [A Deep Instance Generative Framework for MILP Solvers Under Limited Data Availability](https://mlsanity.com/paper/2310.02807/) (2023)
- [MILP-StuDio: MILP Instance Generation via Block Structure Decomposition](https://mlsanity.com/paper/2410.22806/) (2024)
- [Data Imputation with Iterative Graph Reconstruction](https://mlsanity.com/paper/2212.02810/) (2022)
- [HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline](https://mlsanity.com/paper/2302.02104/) (2023)
- [Continuous-Depth Neural Models for Dynamic Graph Prediction](https://mlsanity.com/paper/2106.11581/) (2021)
- [Machine Learning Insides OptVerse AI Solver: Design Principles and Applications](https://mlsanity.com/paper/2401.05960/) (2024)
- [GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection](https://mlsanity.com/paper/2405.11024/) (2024)
- [A Unified Framework for Combinatorial Optimization Based on Graph Neural Networks](https://mlsanity.com/paper/2406.13125/) (2024)
- [W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs](https://mlsanity.com/paper/2302.00272/) (2023)
- [Lightweight Online Learning for Sets of Related Problems in Automated Reasoning](https://mlsanity.com/paper/2305.11087/) (2023)
- [Learning to Solve Combinatorial Optimization under Positive Linear Constraints via Non-Autoregressive Neural Networks](https://mlsanity.com/paper/2409.04495/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Unrealized Expectations: Comparing AI Methods vs Classical Algorithms for Maximum Independent Set](https://mlsanity.com/paper/2502.03669/) (2025)
- [Structure based SAT dataset for analysing GNN generalisation](https://mlsanity.com/paper/2502.11410/) (2025)
- [IVGAE: Handling Incomplete Heterogeneous Data with a Variational Graph Autoencoder](https://mlsanity.com/paper/2511.22116/) (2025)
- [On the Expressive Power of GNNs for Boolean Satisfiability](https://mlsanity.com/paper/2602.08745/) (2026)
- [Boolean Satisfiability via Imitation Learning](https://mlsanity.com/paper/2509.25411/) (2025)
- [Target-Aware Data Augmentation for SAT Prediction](https://mlsanity.com/paper/2605.06931/) (2026)

## Abstract (arXiv)

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 model using a specialized deep generative neural network. We show that G2SAT can generate SAT formulas that closely resemble given real-world SAT instances, as measured by both graph metrics and SAT solver behavior. Further, we show that our synthetic SAT formulas could 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.