Research map / Image generation / Autoregressive and latent generation
HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes HardCore, a fast generator of hard UNSAT SAT instances that iteratively refines unsatisfiable cores using a GNN core predictor, and shows augmentation reduces runtime-prediction MAE.
Problem
Deep-learning SAT research lacks large, realistic datasets; existing generators either produce easy problems (hardness collapse) or are too slow (hours per instance) to produce augmentation data.
Approach
Preserve the UNSAT core of a seed instance while adding random clauses, and after each addition re-identify the core with a fast GNN binary node classifier (trained on proof-producing Drat-Trim core labels) and "de-core" by adding a free literal to break trivially easy cores.
Key results
- HardCore generates instances at 176% of original hardness at about 4.3 s per instance, versus about 6441 s for HardSATGEN, with MMD 0.004 vs 0.492 on LEC data.
- Augmenting with HardCore reduces runtime-prediction MAE by 20-50% on K-SAT and LEC data (e.g., K-SAT 1796 vs 2750 at size 20), while other generators give no comparable gain.
- The GNN core predictor reaches 96% core recovery and 94% accuracy on LEC held-out problems.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use HardCore-generated instances to augment runtime-prediction training data | SATzilla · K-SAT Random, data size 20 | MAE: 2743 -> 1796* | Helped |
| Use HardCore-generated instances to augment runtime-prediction training data | SATzilla · K-SAT Random, data size 40 | MAE: 1449 -> 930* | Helped |
| Use HardCore-generated instances to augment runtime-prediction training data | SATzilla · LEC Internal, data size 100 | MAE: 707 -> 514 | Helped |
| Use HardCore-generated instances to augment runtime-prediction training data | SATzilla · LEC Internal, data size 200 | MAE: 795 -> 481* | Helped |
| Use HardCore-generated instances to augment runtime-prediction training data | SATzilla · LEC Internal, data size 300 | MAE: 557 -> 369* | Helped |
| Use HardCore-generated instances to augment runtime-prediction training data | SATzilla · LEC Internal, data size 400 | MAE: 606 -> 282* | Helped |
| Use HardCore-generated instances to augment runtime-prediction training data | SATzilla · LEC Internal, data size 500 | MAE: 526 -> 338* | Helped |
| Use HardCore to generate instances instead of W2SAT | SAT instance generation on LEC Internal · LEC Internal | hardness (%): ∼0 -> 176 | Helped |
| Use HardCore to generate instances instead of HardSATGEN | SAT instance generation on LEC Internal · LEC Internal | time per instance (s): 6441 -> 4.3 | Helped |
| Use HardCore instead of HardSATGEN for hardness-distribution similarity | SAT instance generation · LEC Internal | MMD: 0.492 -> 0.004 | Helped |
| Increase the core-prediction GCN configuration from the smallest tested model (3 layers, hidden dimension 32) (ablation) | HardCore core predictor · Core prediction | performance | No clear effect |
Surprising findings
- W2SAT and G2MILP suffer hardness collapse, generating instances at near 0% of original solver runtime.
- On the Tseitin SAT Competition family, HardCore-augmented data was worse than original at some dataset sizes (e.g., 3618.9 vs 3369.6 at size 10).
Limitations
- Restricted to UNSAT problems, since cores only exist in UNSAT instances.
- Memory and compute scale polynomially with instance size, so millions-of-clauses problems are out of reach.
- Evaluated on only two main datasets, one of which is synthetic and one proprietary.
Experimental setup
Datasets: LEC Internal circuit equivalence-checking SAT instances (proprietary) K-SAT Random synthetic instances SAT Competition Tseitin and FDMUS families
Benchmarks: LEC Internal K-SAT Random SAT Competition Tseitin SAT Competition FDMUS
Metrics: hardness percentage time per instance (s) maximum mean discrepancy mean absolute error of runtime prediction core recovery (recall) accuracy core size discrepancy
Baselines: HardSATGEN W2SAT G2MILP
Builds on: G2SAT SATGEN HardSATGEN Neurocore
Closest papers by meaning
- G2SAT: Learning to Generate SAT Formulas (NeurIPS 2019 · similarity 0.90)
- Predicting Propositional Satisfiability via End-to-End Learning (AAAI 2020 · similarity 0.88)
- MixSATGEN: Learning Graph Mixing for SAT Instance Generation (ICLR 2024 · similarity 0.87)
- Learning How to Cube (NeurIPS 2026 · similarity 0.86)
- SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.84)
- Automatic Core-Guided Reformulation via Constraint Explanation and Condition Learning (AAAI 2024 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.