HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation

TL;DR

The paper tackles the data scarcity problem in learning-based SAT solving by introducing HardCore, a fast generator that preserves problem hardness through core-aware refinement guided by a graph neural network. By predicting and manipulations of minimally unsatisfiable cores, HardCore iteratively expands hard cores while adding diversity, enabling the production of thousands of challenging UNSAT instances in minutes to hours. Empirical results on proprietary LEC data and synthetic K-SAT data show that HardCore yields solver runtime distributions closely matching the originals and substantially improves runtime-prediction accuracy (MAE reduced by ~20–50% with augmentation). This approach offers a practical path to scalable, realistic data augmentation for learning-to-solve SAT problems, with clear limitations to UNSAT problems and scalability to very large instances.

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 (7)

• 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, larger minimal unsatisfiable subset (core). As steps (1) and (2) are repeated, the core gradually becomes larger, raising the hardness of the generated instance.
• 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.
• 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).