Target-Aware Data Generation for SAT Learning

Learning-based methods for NP-hard problems are becoming increasingly effective, but their scalability is often limited by the cost of obtaining labeled training data. For Boolean satisfiability (SAT), standard dataset construction typically requires generating formulas and then invoking a solver to determine their labels, creating a solver-in-the-loop bottleneck that becomes increasingly expensive as problem size grows. In this work, we introduce a target-aware, solver-free framework for SAT data generation that constructs labeled SAT and UNSAT instances directly, without requiring solver-based verification. The generated formulas are designed to match structural properties of a target benchmark, improving their usefulness for downstream learning. We also introduce a linear-programming-aware graph neural network (LPGNN) that incorporates constraint-violation residuals into message passing, allowing the model to exploit the underlying optimization structure of SAT. Together, these components provide a data-centric approach to SAT learning in which scalable, benchmark-aligned data generation complements model architecture. Empirically, our framework achieves orders-of-magnitude faster data generation while producing synthetic instances that effectively improve GNN-based SAT prediction.