# Target-Aware Data Augmentation for SAT Prediction

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 24 of its 38 references that are in the map.
- First posted on arXiv 7 May 2026.

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Training Compute-Optimal Large Language Models](https://mlsanity.com/paper/2203.15556/) (2022)
- [RandAugment: Practical automated data augmentation with a reduced search space](https://mlsanity.com/paper/1909.13719/) (2019)
- [Graph Contrastive Learning with Augmentations](https://mlsanity.com/paper/2010.13902/) (2020)
- [DropEdge: Towards Deep Graph Convolutional Networks on Node Classification](https://mlsanity.com/paper/1907.10903/) (2019)
- [Exact Combinatorial Optimization with Graph Convolutional Neural Networks](https://mlsanity.com/paper/1906.01629/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Data Augmentation for Deep Graph Learning: A Survey](https://mlsanity.com/paper/2202.08235/) (2022)
- [A Kernel Theory of Modern Data Augmentation](https://mlsanity.com/paper/1803.06084/) (2018)
- [Graph Data Augmentation for Graph Machine Learning: A Survey](https://mlsanity.com/paper/2202.08871/) (2022)
- [MIP-GNN: A Data-Driven Framework for Guiding Combinatorial Solvers](https://mlsanity.com/paper/2205.14210/) (2022)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [The DRAT format and DRAT-trim checker](https://mlsanity.com/paper/1610.06229/) (2016)
- [Quadratic Binary Optimization with Graph Neural Networks](https://mlsanity.com/paper/2404.04874/) (2024)
- [Self-Satisfied: An end-to-end framework for SAT generation and prediction](https://mlsanity.com/paper/2410.14888/) (2024)
- [Structure based SAT dataset for analysing GNN generalisation](https://mlsanity.com/paper/2502.11410/) (2025)
- [MILP-SAT-GNN: Yet Another Neural SAT Solver](https://mlsanity.com/paper/2507.01825/) (2025)
- [On the Expressive Power of GNNs for Boolean Satisfiability](https://mlsanity.com/paper/2602.08745/) (2026)

## Abstract (arXiv)

Learning-based approaches to NP-hard problems have shown increasing promise, but their progress is fundamentally constrained by the high cost of generating labeled training data. In domains such as Boolean satisfiability (SAT), standard pipelines rely on solver-in-the-loop labeling, which scales poorly with problem size and limits the amount of usable supervision. This bottleneck hinders the broader goal of leveraging machine learning to capture structure in hard combinatorial problems. In this work, we propose a target-aware, solver-free data generation framework for SAT that produces correctly labeled SAT and UNSAT instances by construction, eliminating the need for expensive solver calls. Our method aligns generated instances with the structural properties of a target benchmark, making synthetic data effective for downstream learning. We further develop a linear-programming-aware graph neural network (LPGNN) architecture that incorporates constraint-violation residuals into message passing, enabling the model to exploit underlying optimization structure. Together, these contributions support a data-centric paradigm for learning on NP-hard problems, where scalable, task-aligned data generation is as critical as model design. Our approach yields orders-of-magnitude speedups in data generation, demonstrating that benchmark-aligned synthetic data can effectively augment solver-labeled datasets for GNN-based SAT prediction.