Finding good branching orders is key to solving SAT problems efficiently, but finding such branching orders is a difficult problem. Using a learning based approach to predict a good branching order before solving, therefore, has potential. In this paper, we investigate predicting branching orders using graph neural networks as a preprocessing step to conflict-driven clause learning (CDCL) SAT solvers. We show that there are significant gains to be made in existing CDCL SAT solvers by providing a good initial branching. Further, we provide three labeling methods to find such initial branching orders in a tractable way. Finally, we train a graph neural network to predict these branching orders and show through our evaluations that a GNN-initialized ordering yields significant speedups on random 3-CNF and pseudo-industrial benchmarks, with generalization capabilities to instances much larger than the training set. However, we also find that the predictions fail at speeding up more difficult and industrial instances. We attribute this to the solver's dynamic heuristics, which rapidly overwrite the provided initialization, and to the complexity of these instances, making GNN prediction hard.
Figures & tables
Figure 1: Pipeline for training (top) and inference (bottom) for a branch order-predicting GNN preprocessing step. The orange boxes (dotted outline) signify steps that use a modified SAT solver, while purple boxes (dashed outline) signify steps using a graph neural network.
Figure 2: Mean solving time for setting one of 50 randomly sampled variables first, with the remaining order randomized. The shaded areas indicate a 95% confidence interval over 1000 iterations for each variable.
Instance
Variables
Clauses
Median (s)
Best speedup (%)
Top 10% speedup (%)
3-CNF 100
100
430
0.0007
2233.3
536.4
3-CNF 150
150
645
0.016
63.1
30.8
3-CNF 200
200
860
0.12
13.1
9.1
3-CNF 250
250
1075
0.98
5.6
4.1
Ramsey
37410
162400
3.41
0.8
0.5
Manthey
3996
29400
0.59
2.0
0.9
Table 1: Solving time and speedup when choosing the best and 10th-percentile variables, respectively, compared to the median, when forcing initial branching to start on a specific variable.
Figure 3: Graph of (x1∨¬x2)∧(x2∨x3)
Figure 4: Mean reduction in the number of propagations relative to the default variable order on SATLIB uniform random 3-CNF benchmarks. Top: CaDiCaL on SAT and UNSAT instances, respectively. Bottom: MiniSat on SAT and UNSAT instances, respectively. Shaded regions denote a 95% confidence interval across the dataset.
Figure 5: Number of propagations on the hard G4SATBench instances. Speedups of 10%-20% until roughly 105 propagations.
Figure 6: Solving time for CaDiCaL and MiniSat on the SAT competition 2024 main track.
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 7: Comparison of inference time and solving time using CaDiCaL (default order) when solving on CPU only for SAT (a) and UNSAT (b) instances. Note the logarithmic y-axis.
Hyperparameter
Value
Model Architecture
Graph Transformer from NeuroBack ( Wang et al., 2024 )
Optimizer
AdamW ( Loshchilov and Hutter, 2018 )
Adam β1
0.9
Adam β2
0.999
Learning Rate
0.001
Epochs
10
Appendix
Table 2: Model hyperparameters
Figure 8: Number of propagations on the hard G4SATBench instances. No distinct speedup.
Figure 9: Number of propagations for different reminding factors. Only the problems that all seven initializations solve are plotted.
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.
Eshed Gal, Uri Ascher, Eldad Haber
Department of Computer Science The University of British Columbia Vancouver, Canada · Department of Earth, Ocean and Atmospheric Sciences The University of British Columbia Vancouver, Canada
Machine learning is increasingly used to improve decisions within branch-and-bound algorithms for mixed-integer programming. Many existing approaches rely on deep learning, which often requires very large training datasets and substantial computational resources for both training and deployment, typically with GPU parallelization. In this work, we take a different path by developing interpretable models that are simple but effective. We focus on approximating strong branching (SB) scores, a highly effective yet computationally expensive branching rule. Using sparse learning methods, we build models with fewer than 4% of the parameters of a state-of-the-art graph neural network (GNN) while achieving competitive accuracy. Relative to SCIP's built-in branching rules and the GNN-based model, our CPU-only models are faster than the default solver and the GPU-accelerated GNN. The models are simple to train and deploy, and they remain effective with small training sets, which makes them practical in low-resource settings. Extensive experiments across diverse problem classes demonstrate the efficiency of this approach.
Selin Bayramoğlu, George L Nemhauser, Nikolaos V Sahinidis
H. Milton Stewart School of Industrial and Systems Engineering, Georgia Institute of Technology · School of Chemical & Biomolecular Engineering, Georgia Institute of Technology
Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn effective cubing heuristics. We introduce a neuro-symbolic post-training framework for this task. We design an MCTS-based data curation pipeline that uses symbolic heuristics to explore splitting decisions over SAT competition formulas, producing preference data grounded in solver statistics and augmented with reasoning traces from a teacher model. Our two-stage post-training, supervised fine-tuning (SFT) followed by direct preference optimization (DPO), enables a 4B-parameter model to achieve a pass@5 score of 53 on 100 SAT competition benchmarks, surpassing frontier LLMs such as Claude-Sonnet-4 (50) and matching the best symbolic heuristic (53). Ablations show that SFT alone improves pass@5 from 46 to 51, with DPO adding 2 additional benchmarks; an entropy/agreement ablation on realized first-cube decisions further shows that SFT, not DPO, accounts for the root-level decision diversity that produces complementary per-run coverage over deterministic symbolic methods. This demonstrates that transformers can be trained to make effective cubing decisions in a domain traditionally dominated by symbolic methods.