HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation

Joseph Cotnareanu; Zhanguang Zhang; Hui-Ling Zhen; Yingxue Zhang; Mark Coates

cs.LGSep 27, 2024

HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation

Authors: Joseph Cotnareanu, Zhanguang Zhang, Hui-Ling Zhen, Yingxue Zhang, Mark Coates

Organizations: McGill University Montreal, Canada · Huawei Noah’s Ark Lab Montreal, Canada · Huawei Noah’s Ark Lab Hong Kong, China · Huawei Noah’s Ark Lab Toronto, Canada

Abstract

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 (%)	$\sim$ 0	267	$\sim$ 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.

Panel of Figure 4 — 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.

Panel of Figure 5 — 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.

Panel of Figure 6 — Figure 6 : HardCore (top) and HardSATGEN (bottom) Comparison of Solver Ranking Histograms for Original and Generated LEC data.

	$\uparrow$ Core Recovery Ratio $\frac{TP}{P}$	$\downarrow$ Core Size Discrepancy $\frac{\|TP-P\|}{P+N}$	$\uparrow$ Accuracy $\frac{TP+TN}{P+N}$
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.

Explore similar work

Target-Aware Data Augmentation for SAT Prediction
May 7, 2026Eshed Gal, Uri Ascher, Eldad HaberSatisfiability Np-Hard
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
Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
Jul 16, 2026Ruben MartinsSatisfiability Functional Code Solvers
Carnegie Mellon University
Targeting Clause Type Distributions: a Picklock for Random Satisfiability Problems
May 19, 2026J. Schwardt, J. C. BudichSatisfiability Large Neighborhood Search
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

May 7, 2026, cs.LGJ/K move · Enter open · S save

Target-Aware Data Augmentation for 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

Satisfiability Np-Hard Synthetic Benchmark Graph Neural Networks

Open paper AskPDF 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.

Abstract

Explore similar work

Target-Aware Data Augmentation for SAT Prediction

Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience

Targeting Clause Type Distributions: a Picklock for Random Satisfiability Problems