Efficiently determining the satisfiability of a boolean equation -- known as the SAT problem for brevity -- is crucial in various industrial problems. Recently, the advent of deep learning methods has introduced significant potential for enhancing SAT solving. However, a major barrier to the advancement of this field has been the scarcity of large, realistic datasets. The majority of current public datasets are either randomly generated or extremely limited, containing only a few examples from unrelated problem families. These datasets are inadequate for meaningful training of deep learning methods. In light of this, researchers have started exploring generative techniques to create data that more accurately reflect SAT problems encountered in practical situations. These methods have so far suffered from either the inability to produce challenging SAT problems or time-scalability obstacles. In this paper we address both by identifying and manipulating the key contributors to a problem's ``hardness'', known as cores. Although some previous work has addressed cores, the time costs are unacceptably high due to the expense of traditional heuristic core detection techniques. We introduce a fast core detection procedure that uses a graph neural network. Our empirical results demonstrate that we can efficiently generate problems that remain hard to solve and retain key attributes of the original example problems. We show via experiment that the generated synthetic SAT problems can be used in a data augmentation setting to provide improved prediction of solver runtimes.
Figures & tables
Figure 1 : Our method (HardCore) achieves the best trade-off of inference cost and SAT-problem hardness.
Figure 2 : Core Refinement . The core refinement process comes in two steps: (1) Core Prediction, in which we use a GNN-based architecture to identify the core of the generated instance; and (2) De-Coring, in which we add a non-conflicted literal to a clause in the core, rendering the core satisfiable and giving rise to a new, harder minimal unsatisfiable subset (core). As steps (1) and (2) are repeated, the easiest core of the problem is gradually refined, raising the hardness of the generated instances.
Figure 3 : Core Prediction GNN Architecture . We construct our GNN using three parallel message passing neural networks (MPNN) whose calculated node embeddings are aggregated at each layer to form the layer’s node embeddings. Readout is done by taking the sigmoid of a fully-connected layer on clause node embeddings and thresholding. Training is supervised by taking a binary classification loss between the true core labels and the clause nodes’ core prediction probabilities.
W2SAT
HardSATGEN
G2MILP
HardCore
Hardness (%)
∼ 0
267
∼ 0
176
Time per instance (s)
1.2
6441
3.3
4.3
Similarity (MMD)
—
0.492
—
0.004
Table 1 : Evaluation of generated datasets on LEC data. Hardness level (%): percentage of runtime of generated dataset relative to original dataset, closer to 100% is better. Speed (s): average time cost to generate one instance, lower is better. Maximum Mean Discrepancy (MMD): distance between distributions of generated and original datasets, lower is better.
Figure 4 : HardCore (Left) and HardSATGEN (Right). Boxplots of runtimes per solver for Original (Green) and Generated (Blue) instances on LEC data. HardCore appears to produce per-solver distributions which are much closer to the original than HardSATGEN, which tends to produce high-variance and on-average much harder problems than the original.
Figure 5 : LEC Internal Rank 1 Solvers. We compare original and synthetic best-solver observations for HardCore (left) and HardSATGEN (right).
K-SAT Random
LEC Internal
Data Size
10
20
30
40
100
200
300
400
500
HardSATGEN- N
2416
2306
2172
2182
666
797
605
617
463
HardSATGEN-Strict
2179
2578
2488
2456
627
742
565
638
513
W2SAT
2606
2046
1807
1377
724
704
634
611
535
Original
2750
2743
2109
1449
707
795
557
606
526
HardCore
2156
1796*
1615
930*
514
481*
369*
282*
338*
Table 2 : MAE of Runtime Prediction averaged across 7 solvers and 15 trials. Asterisks are placed at the best result which passes the Wilcoxon pairwise ranking test against the second-best for p<0.05 . For a boxplot visualization showing each trials result, see Appendix Figure 7
Appendix figures & tables6 assets
Supplementary material from the paper’s appendix.
Appendix
var.
clause
runtimes (s)
count
LEC
1328
5167
388
78730
K-SAT
398
1751
2700
1351
Appendix
Table 3 : Data Statistics. Note that LEC is a much larger dataset than Tseitin in every regard: average variable and clause counts, average hardness on Kissat solver and dataset size.
Figure 6 : HardCore (top) and HardSATGEN (bottom) Comparison of Solver Ranking Histograms for Original and Generated LEC data.
↑ Core Recovery Ratio PTP
↓ Core Size Discrepancy P+N∣TP−P∣
↑ Accuracy P+NTP+TN
Circuit-Split LEC
0.97
0.05
0.65
LEC
0.960
0.009
0.940
Appendix
Table 4 : GNN Core Prediction Performance
Figure 7 : Mean MAE on Runtime Prediction. Boxplot-view of results presented in Table 2 for LEC data.
Tseitin Dataset Size
Training Data
10
20
30
40
50
HardCore-Augmented
3618.9
3410.0
3311.4
3417.7
3419.4
Original (Un-Augmented)
3369.6
3581.9
3576.1
3544.7
3608.5
Appendix
Table 5 : Data Augmentation experiment: MAE of Runtime Prediction averaged across 7 solvers and 15 trials. We train a runtime prediction model according to the experimental setting in 6.4.2 of the paper. Columns in the table indicate the number of original problems used in the training set (we generate 4 times per original problem in the training set). Results in the “HardCore” row are MAE for a runtime prediction model trained on HardCore-augmented data, whereas “Original” indicates un-augmented performance.
FDMUS Dataset Size
Training Data
100
200
300
400
500
HardCore-Augmented
0.220
0.197
0.162
0.142
0.142
Original (Un-Augmented)
0.246
0.213
0.184
0.173
0.145
Appendix
Table 6 : Data Augmentation experiment: MAE of Runtime Prediction averaged across 7 solvers and 15 trials. We train a runtime prediction model according to the experimental setting in 6.4.2 of the paper. Columns in the table indicate the number of original problems used in the training set (we generate 4 times per original problem in the training set). Results in the “HardCore” row are MAE for a runtime prediction model trained on HardCore-augmented data, whereas “Original” indicates un-augmented performance.
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
We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase. The project focuses on unsatisfiability-based MaxSAT algorithms and follows an iterative workflow that combines paper discussions with ChatGPT, implementation through Codex prompts, and repeated LLM-assisted code audits and revisions. Although the codebase implements several algorithms and solver components, our evaluation focuses on configurations that combine core-guided optimization, lightweight preprocessing, core minimization, integration with integer linear optimization backends, and a new core-sequence lookahead approach. Our experience suggests that LLMs can support solver implementation from papers, while requiring external validation, benchmarking, and human guidance. In our experiments, fuzzing and MaxSAT Evaluation instances did not reveal wrong answers in the tested configurations, although performance remains below the best hand-engineered MaxSAT solvers. We summarize what worked, what remained difficult, and the lessons for future LLM-assisted solver development.
Optimization problems such as the NP-complete 3-SAT provide an important benchmark for the difficult task of finding ground-states in strongly correlated many-body systems with rugged energy landscapes. The study of random 3-SAT problems as Ising spin Hamiltonians in statistical physics has yielded major insights including the existence of a satisfiability phase transition, and the prediction of a critical parameter line of particularly hard instances. Yet, progress on solving those instances has been scarce for several decades. Here, introducing the Target-SAT (TSAT) algorithm, we roughly triple the tractable problem sizes in the hardest regime, with an even greater improvement in a vast range of neighboring regions. By leveraging statistical information hidden in the combinatorial constraints of the problem, TSAT is actively guided in its stochastic local search toward a target within the relevant parameter space. Our analysis also explains why established local search algorithms are limited to relatively small system sizes due to a vast low-energy trap. Furthermore, we characterize the aforementioned critical line in terms of a dominant additional complexity barrier, whose exponential scaling is quickly overcome by TSAT only in the surrounding parameter space. With TSAT, the lead in solving the hardest known random satisfiability problems returns to the realm of stochastic local search algorithms.
J. Schwardt, J. C. Budich
Max Planck Institute for the Physics of Complex Systems, Nöthnitzer Str. 38, 01187 Dresden, Germany · Institute of Theoretical Physics, Technische Universität Dresden and Würzburg-Dresden Cluster of Excellence ctd.qmat, 01062 Dresden, Germany