# HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline

arXiv: https://arxiv.org/abs/2302.02104 · HTML: https://mlsanity.com/paper/2302.02104/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 54 references that are in the map.
- First posted on arXiv 4 Feb 2023.

## Builds on (most cited first, 12 of 12)

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Dynamic Edge-Conditioned Filters in Convolutional Neural Networks on Graphs](https://mlsanity.com/paper/1704.02901/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [HEBO Pushing The Limits of Sample-Efficient Hyperparameter Optimisation](https://mlsanity.com/paper/2012.03826/) (2020)
- [It's Not What Machines Can Learn, It's What We Cannot Teach](https://mlsanity.com/paper/2002.09398/) (2020)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [ASTERYX : A model-Agnostic SaT-basEd appRoach for sYmbolic and score-based eXplanations](https://mlsanity.com/paper/2206.11900/) (2022)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [Enhancing SAT solvers with glue variable predictions](https://mlsanity.com/paper/2007.02559/) (2020)

## Built on by (most cited first, 12 of 12)

- [SGFormer: Simplifying and Empowering Transformers for Large-Graph Representations](https://mlsanity.com/paper/2306.10759/) (2023)
- [A Deep Instance Generative Framework for MILP Solvers Under Limited Data Availability](https://mlsanity.com/paper/2310.02807/) (2023)
- [LinSATNet: The Positive Linear Satisfiability Neural Networks](https://mlsanity.com/paper/2407.13917/) (2024)
- [Benchmarking PtO and PnO Methods in the Predictive Combinatorial Optimization Regime](https://mlsanity.com/paper/2311.07633/) (2023)
- [Machine Learning Insides OptVerse AI Solver: Design Principles and Applications](https://mlsanity.com/paper/2401.05960/) (2024)
- [Tackling Prevalent Conditions in Unsupervised Combinatorial Optimization: Cardinality, Minimum, Covering, and More](https://mlsanity.com/paper/2405.08424/) (2024)
- [GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection](https://mlsanity.com/paper/2405.11024/) (2024)
- [STRCMP: Integrating Graph Structural Priors with Language Models for Combinatorial Optimization](https://mlsanity.com/paper/2506.11057/) (2025)
- [Unrealized Expectations: Comparing AI Methods vs Classical Algorithms for Maximum Independent Set](https://mlsanity.com/paper/2502.03669/) (2025)
- [Structure based SAT dataset for analysing GNN generalisation](https://mlsanity.com/paper/2502.11410/) (2025)
- [HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation](https://mlsanity.com/paper/2409.18778/) (2024)
- [Learning to Solve Weighted Maximum Satisfiability with a Co-Training Architecture](https://mlsanity.com/paper/2511.19544/) (2025)

## Abstract (arXiv)

Industrial SAT formula generation is a critical yet challenging task. Existing SAT generation approaches can hardly simultaneously capture the global structural properties and maintain plausible computational hardness. We first present an in-depth analysis for the limitation of previous learning methods in reproducing the computational hardness of original instances, which may stem from the inherent homogeneity in their adopted split-merge procedure. On top of the observations that industrial formulae exhibit clear community structure and oversplit substructures lead to the difficulty in semantic formation of logical structures, we propose HardSATGEN, which introduces a fine-grained control mechanism to the neural split-merge paradigm for SAT formula generation to better recover the structural and computational properties of the industrial benchmarks. Experiments including evaluations on private and practical corporate testbed show the superiority of HardSATGEN being the only method to successfully augment formulae maintaining similar computational hardness and capturing the global structural properties simultaneously. Compared to the best previous methods, the average performance gains achieve 38.5% in structural statistics, 88.4% in computational metrics, and over 140.7% in the effectiveness of guiding solver tuning by our generated instances. Source code is available at http://github.com/Thinklab-SJTU/HardSATGEN