# W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 48 references that are in the map.
- First posted on arXiv 1 Feb 2023.

## Builds on (most cited first, 14 of 14)

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Efficient Estimation of Word Representations in Vector Space](https://mlsanity.com/paper/1301.3781/) (2013)
- [Variational Graph Auto-Encoders](https://mlsanity.com/paper/1611.07308/) (2016)
- [Junction Tree Variational Autoencoder for Molecular Graph Generation](https://mlsanity.com/paper/1802.04364/) (2018)
- [Permutation Invariant Graph Generation via Score-Based Generative Modeling](https://mlsanity.com/paper/2003.00638/) (2020)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [NetGAN: Generating Graphs via Random Walks](https://mlsanity.com/paper/1803.00816/) (2018)
- [Graphite: Iterative Generative Modeling of Graphs](https://mlsanity.com/paper/1803.10459/) (2018)
- [SPECTRE: Spectral Conditioning Helps to Overcome the Expressivity Limits of One-shot Graph Generators](https://mlsanity.com/paper/2204.01613/) (2022)
- [Scalable Deep Generative Modeling for Sparse Graphs](https://mlsanity.com/paper/2006.15502/) (2020)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [Computing Clique Cover with Structural Parameterization](https://mlsanity.com/paper/2208.12438/) (2022)
- [Fixed-Parameter Tractability of the Weighted Edge Clique Partition Problem](https://mlsanity.com/paper/2002.07761/) (2020)

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

- [GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection](https://mlsanity.com/paper/2405.11024/) (2024)
- [Self-Satisfied: An end-to-end framework for SAT generation and prediction](https://mlsanity.com/paper/2410.14888/) (2024)
- [HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation](https://mlsanity.com/paper/2409.18778/) (2024)

## Abstract (arXiv)

The Boolean Satisfiability (SAT) problem stands out as an attractive NP-complete problem in theoretic computer science and plays a central role in a broad spectrum of computing-related applications. Exploiting and tuning SAT solvers under numerous scenarios require massive high-quality industry-level SAT instances, which unfortunately are quite limited in the real world. To address the data insufficiency issue, in this paper, we propose W2SAT, a framework to generate SAT formulas by learning intrinsic structures and properties from given real-world/industrial instances in an implicit fashion. To this end, we introduce a novel SAT representation called Weighted Literal Incidence Graph (WLIG), which exhibits strong representation ability and generalizability against existing counterparts, and can be efficiently generated via a specialized learning-based graph generative model. Decoding from WLIGs into SAT problems is then modeled as finding overlapping cliques with a novel hill-climbing optimization method termed Optimal Weight Coverage (OWC). Experiments demonstrate the superiority of our WLIG-induced approach in terms of graph metrics, efficiency, and scalability in comparison to previous methods. Additionally, we discuss the limitations of graph-based SAT generation for real-world applications, especially when utilizing generated instances for SAT solver parameter-tuning, and pose some potential directions.