Technical Summary: Target-Aware Data Augmentation for SAT Prediction

1. Problem Statement

The application of machine learning, particularly Graph Neural Networks (GNNs), to NP-hard problems like Boolean Satisfiability (SAT) is fundamentally constrained by the high cost of generating labeled training data. Standard pipelines rely on a "solver-in-the-loop" approach, where random formulas are generated and then solved by complete SAT solvers (e.g., CaDiCaL) to determine their labels (SAT or UNSAT). As problem sizes increase, especially near the satisfiability phase transition, this labeling process becomes exponentially expensive, severely limiting the scale of usable supervision. This bottleneck hinders the ability to leverage large-scale data to capture the structural properties of hard combinatorial problems, a prerequisite for the success of modern deep learning paradigms.

2. Methodology

The authors propose a two-pronged approach: a target-aware, solver-free data generation framework and an optimization-aware GNN architecture.

2.1 Target-Aware Solver-Free Data Generation

The core insight is an asymmetry: while finding a satisfying assignment for a given formula is NP-hard, constructing a formula around a known assignment (or contradiction) is computationally efficient. The authors adopt a "solution-first" viewpoint, constructing instances by construction rather than sampling and verifying.

• SAT Instance Generation: The method samples a random reference assignment $x^*$. For each clause, it samples a target "slack" $s^*$ from the empirical distribution of a target benchmark (e.g., G4SATBench). The slack represents the number of literals in a clause satisfied beyond the single one required for feasibility. The generator then deterministically constructs clauses with specific polarities such that exactly $s^* + 1$ literals are satisfied by $x^*$. This ensures the instance is satisfiable by construction and matches the benchmark's slack distribution.
• UNSAT Instance Generation: The method embeds a small, guaranteed UNSAT core (a set of clauses covering all polarity combinations of a subset of variables) within a larger set of "filler" clauses. The filler clauses are generated using the same slack-planted method as SAT instances, aligning with the benchmark's UNSAT slack distribution. The label is known by construction (UNSAT) without requiring a solver.
• Target-Awareness: Unlike generic planted constructions, this framework explicitly matches structural statistics (clause width, occurrence skew, and slack distributions) of a target benchmark to minimize distributional mismatch.

2.2 Linear-Programming-Aware Graph Neural Network (LPGNN)

To leverage the algebraic structure of the generated data, the authors introduce the LPGNN.

• Encoding: CNF formulas are mapped to a binary linear feasibility problem $Ax \geq b$. Slack variables $s$ are introduced to convert inequalities to equalities: $Ax - s = b$.
• Graph Structure: The graph contains two node types: variable nodes ($x$) and slack nodes ($s$). Edges connect variables to the slack nodes of clauses they participate in.
• Message Passing with Residuals: The architecture incorporates a Linear Programming (LP) residual mechanism. At each layer, the network projects node embeddings to a continuous surrogate $\tilde{z}$. It computes a constraint residual $r = \tilde{A}\tilde{z} - b$ in constraint space. This residual is mapped back to node space via the transpose $\tilde{A}^T r$, providing a feasibility signal (gradient of the constraint violation) that is injected into the node updates. This allows the GNN to exploit the underlying optimization structure directly.

3. Key Contributions

1. Solver-Free Generation Framework: A CNF-native method to generate correctly labeled SAT and UNSAT instances by construction, eliminating the need for expensive solver calls during data creation.
2. Target-Aware Alignment: A strategy that aligns synthetic data with the structural and algebraic properties (specifically slack distributions) of target benchmarks, making the data effective for downstream learning.
3. LPGNN Architecture: A novel GNN design that integrates LP-based constraint-violation residuals into message passing, exposing algebraic feasibility structure to the model.
4. Data-Centric Paradigm: A demonstration that for NP-hard problems, scalable, task-aligned data generation is as critical as model architecture design.

4. Experimental Results

• Generation Efficiency: The proposed method achieves orders-of-magnitude speedups compared to solver-in-the-loop baselines. For large instances (e.g., $n=1000$), the solver-free method is approximately $10^{14}$ times faster than the extrapolated CaDiCaL baseline.
• Distributional Alignment: The generated instances faithfully reproduce the slack distributions of the target G4SATBench dataset (Figure 1).
• Scaling Behavior: Training LPGNN on the generated synthetic data shows consistent improvement in performance as the training volume increases.
  • SAT Prediction: The Constraint Satisfaction Rate (CSR) improves from ~88% to ~99% as data volume increases from 250 to 10k instances.
  • UNSAT Prediction: The fraction of violated clauses ($k/m$) decreases, indicating better assignment quality for unsatisfiable instances.
• Generalization: The benefits of target-aware data extend to other architectures (NLocalSAT, QuerySAT) and generalize to out-of-distribution test sets (harder 3-SAT tiers and SR families).
• Ablation: Removing the LP residual mechanism from LPGNN results in lower accuracy and CSR, confirming the value of the optimization-aware signal.
• Comparison with Generic Data: Training on generic, non-aligned synthetic data yields near-random performance, highlighting that structural alignment is the key factor for success.

5. Significance and Claims

The paper claims that the primary bottleneck in learning-based SAT solvers is not model capacity but the cost of obtaining labeled data. By introducing a scalable, solver-free generation pipeline that produces benchmark-aligned synthetic data, the authors demonstrate that it is possible to train GNNs effectively without relying on expensive solvers for supervision.

The authors position this work as a shift toward a data-centric paradigm for NP-hard problems. They argue that just as next-token prediction enabled the scaling of language models, scalable and task-aligned data generation is the key enabler for unlocking the potential of machine learning in combinatorial optimization. The work does not claim to solve SAT instances that are intractable for current solvers, but rather to provide a mechanism for generating the large-scale, high-quality training data necessary to improve heuristic search and assignment prediction in GNNs. The authors acknowledge limitations regarding the "synthetic-to-real" gap, noting that manufactured instances may not perfectly capture the hidden community structures of specialized industrial problems, but argue that the approach serves as a powerful regularizer for in-distribution learning.