Source-linked AI summary
HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline
Yang Li, Xinyan Chen, Wenxuan Guo, Xijun Li, Wanqian Luo, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, Junchi Yan
TL;DR
Industrial SAT generators have difficulty matching both benchmark structure and computational hardness. HardSATGEN adds fine-grained, multi-stage control to neural split-merge generation. The authors report that it is the only method to maintain similar hardness while capturing global structure, and that it reduces relative error against prior methods by 88.4% on average.
Problem
Existing generators struggle to reproduce both the global structure and computational hardness of industrial SAT benchmarks.
Source: §1 · p. 2Method
HardSATGEN controls a multi-stage split-merge pipeline through core scrambling, in-community connections, and cross-community connections.
Source: §1 · p. 2Results
HardSATGEN is reported as the only method to maintain computational hardness similar to original instances, reducing relative error against prior best methods by 88.4% on average.
Source: §1 · p. 2, §5.3.2 · p. 8Takeaways & Limitations
The authors report that HardSATGEN outperforms state-of-the-art learning-based and handcrafted methods in structure and hardness mimicking.
Source: §6 · p. 9The analysis concerns one-stage split-merge generation, where limited control can produce homogeneous structures that fit CDCL solvers’ backtracking inference and collapse hardness.
Source: §3 · pp. 3–4
Abstract
from arXiv · showhide
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
1 INTRODUCTION
HardSATGEN targets the difficulty of generating industrial SAT instances that match both their global structure and computational hardness. The paper attributes prior hardness degradation to homogeneous split-merge generation and proposes a community- and core-aware multi-stage pipeline.
1 INTRODUCTION
- Prior learning-based generators can match global graph structure but often produce instances far easier to solve than the industrial benchmarks they model.The paper gives the example of benchmarks taking hundreds of seconds to solve while generated formulae take seconds, making them unreliable for applications such as solver parameter tuning.Source: §1 · p. 2
- Industrial formulae exhibit community structure correlated with CDCL solver runtime, while unsatisfiable cores have rigid logical structures that are harder to form from oversplit pieces.The paper argues that meaningful substructures make core formation more feasible, whereas existing methods split graphs into preliminary pieces.Source: §1 · p. 2
- The proposed pipeline combines core scrambling, in-community connections, and cross-community connections to control structure and hardness during generation.Community knowledge is embedded in the graph, and post-processing is used to keep the scrambled core dominant in computational performance.Source: §1 · p. 2
- HardSATGEN is reported as the only method to generate formulae with computational hardness similar to the originals while capturing global structural properties.The authors report superiority over state-of-the-art learning-based and hand-crafted methods on public benchmarks and a private corporate testbed.Source: §1 · p. 2
- The paper traces prior hardness-reproduction problems to homogeneous split-merge generation, where oversplit, low-diversity pieces are repeatedly merged into similar substructures.The authors argue this limits the ability to reproduce rigorous logical structures and computational hardness.Source: §1 · p. 2
2 PRELIMINARIES AND RELATED WORKS
The preliminaries introduce SAT graph representations and learning-based approaches, then review handcrafted and neural SAT generators. The section identifies one-stage node split-merge generation as a flexible graph-generation framework that still produces instances that are too easy for modern solvers.
2.1 SAT Problem and Its Graph Representation
- SAT formulae can be represented with several graph forms; the paper generally uses VCG diagrams for simplicity and comprehensibility.LCG is bipartite, with literal and clause nodes joined when a literal occurs in a clause; VCG and VIG merge each variable with its negation.Source: §2.1 · p. 3
2.2 Learning for SAT/CO Solving
- Learning for SAT includes end-to-end neural solvers and learning-aided components for existing solvers, while current learning-based solvers handle only small random instances relative to industrial benchmarks.The paper focuses instead on industrial instance generation and evaluates generated instances by tuning established non-learning solvers.Source: §2.2 · p. 3
2.3 SAT Generators and the Node Split-Merge Framework for ML Generators
- Handcrafted generators target selected structural metrics, while neural generators learn graph structure; the one-stage split-merge framework generates formulae by sequentially merging clause nodes.G2SAT introduced the framework for bipartite graphs, and later methods vary graph representations and GNN designs; generated instances nevertheless remain too easy for modern SAT solvers.Source: §2.3 · p. 3
3 EXISTING ONE-STAGE SPLIT-MERGE’S LIMITATION IN REPRODUCING HARDNESS
The section explains why one-stage split-merge generation can collapse hardness: oversplitting creates repetitive preliminary pieces, and limited learned merging encourages homogeneous structures that fit CDCL solvers. The authors use clause-feature visualizations to illustrate the collapse and discuss retaining structure and constraining merges as possible remedies.
3 EXISTING ONE-STAGE SPLIT-MERGE’S LIMITATION IN REPRODUCING HARDNESS
- Repeatedly splitting clause nodes until they connect to one variable creates many repetitive clauses and low-diversity starting substructures.Each variable occurrence in the original formula yields a clause node connected to that variable in the template.Source: §3 · p. 3
- Limited control over learned node-pair merging produces common substructures that fit CDCL backtracking, leading to hardness collapse.The learned policy assigns high predicted probability to preferred merges, which can organize generated formulae into tree-like logic structures.Source: §3 · pp. 3–4
- PCA visualizations show real-world clause features as scattered, while generated features collapse into a few patterns after merging.The plotted features come from the learned GNN; the axes are the first and second principal components.Source: §3 · p. 4, Figure 2 · p. 4
- The authors suggest stopping splitting at rigorous structures and constraining merge proposals to reduce repeated merging of similar substructures.These are presented as two ways to preserve key structures and moderate the homogeneous results of the aggregation policy.Source: §3 · p. 4
4 HARDSATGEN: STRUCTURE AND HARDNESS AWARE GENERATION PIPELINE
HardSATGEN extends node split-merge generation with community- and core-aware graph representations, staged splitting, and controlled multi-stage merging.
4.1 Graph Building: Community and Core Embedded Bipartite Graph Representations
- HardSATGEN represents formulae with community, variable, and clause nodes, linking communities to affiliated variables and variables to clauses in the formula.Community detection is applied to the variable-incidence graph, and core detection identifies a subset of self-unsatisfiable clauses.Source: §4.1 · p. 4
4.2 Node Splitting: Preparation for Training Data and Graph Templates
- Splitting retains the core and proceeds in cross-community and then in-community stages, producing graph templates and training pairs for generation.Positive pairs come from the split, while negative pairs are formed from same-affiliation alternatives.Source: §4.2 · pp. 4–5
4.3.1 Core Scrambling with Tie-in Post-processing.
- Tunable scrambling randomizes variable order, clause order, and literal phases while preserving the core’s rigorous logical structure.A post-processing step detects unexpected small cores and adds a new variable to a clause outside the original core to remove unnecessary substructures.Source: §4.3.1 · p. 5
4.3 Model Inference: General Multi-Stage Instance Generation Pipeline
- Inference starts from split templates and sequentially merges predicted node pairs through core scrambling, in-community connection, and cross-community connection.The pair proposals are controlled by set operations on community 2-hop neighborhoods.Source: §4.3 · p. 5, Figure 6 · p. 6
4.3.2 In-community and cross-community connection.
- Separate in-community and cross-community merging phases use learned pair probabilities, while α controls their phase boundary and resulting modularity.A larger α produces smaller modularity; α defaults to 1.Source: §4.3.2 · pp. 5–6
4.4 Model Training: Learn to Predict Merging Pairs with Two-stage Control
- Two GNN modules are trained as binary classifiers to predict merge pairs separately for in-community and cross-community connection.The two training datasets are formed sequentially during splitting, and the trained networks guide merging during generation.Source: §4.4 · p. 6
4.4.1 Graph Network Design.
- HardSATGEN is evaluated with both GCN and GraphSAGE backbones, using length-4 one-hot input features for four node types.The types are positive literal, negative literal, clause, and community.Source: §4.4.1 · p. 6
4.4.2 Training Loss.
- Binary cross-entropy trains the classifiers on positive and negative node-pair distributions.The same loss paradigm is used for both connection stages, with training data constructed separately by community affiliation.Source: §4.4.2 · pp. 6–7
5 EXPERIMENTS
HardSATGEN improves structural matching, reproduces solver hardness more closely, and yields stronger solver-tuning gains than prior methods. Experiments also show that its phase-transition parameter controls graph modularity.
5.1.1 Datasets.
- Experiments use separately trained MP1 and SP4 SAT Competition datasets and LEC-CORP industrial circuit instances converted to CNF, including multipliers from 4 × 4 to 22 × 22 bits.Evaluation considers structural statistics, computational hardness, and solver tuning on real-world benchmarks.Source: §5.1.1 · p. 7, §5.1 · p. 7
5.1.2 Baselines.
- Baselines include hand-crafted CA and PS generators and learning-based G2SAT, GCN2S, EGNN2S, and ECC2S, the latter methods using node split-merge with different network backbones.CA targets VIG modularity; PS targets modularity and variable-occurrence power-law distributions.Source: §5.1.2 · p. 7
5.2.1 Metrics.
- Structural evaluation measures modularity across four graph representations, VIG clustering, and clause scale-free parameter α_c; hardness evaluation uses solver rankings and CaDiCaL runtime.Ranking alignment is assessed against training data, including the fraction of exact ranking recoveries; runtime is evaluated separately for each ground-truth instance.Source: §5.2.1 · p. 7, §5.3.1 · p. 8
5.2.2 Results.
- 38.5% average relative-error reduction over the best previous methods, with the largest example improving SP4 VIG clustering error from 47.37% to 1.75%.On LEC-CORP, HardSATGEN best fits the ground-truth distributions across all plotted graph statistics.Source: §5.2.2 · p. 7, Figure 8 · p. 7, Table 2 · p. 8
5.3.2 Results.
- 88.4% average relative-error reduction over previous methods; HardSATGEN alone recovers the LEC-CORP solver ranking with 100% accuracy.Prior methods generally generate instances solvable in much less time than the original benchmarks, whereas HardSATGEN maintains similar performance.Source: §5.3.2 · p. 8, Table 3 · p. 8
5.4 Structural Control Ability Study
- Increasing α from 0.65 to 1.30 produces smaller modularity in VCG, LIG, and LCG graphs.The study presents this phase-transition parameter as a means of controlling structural statistics within a margin.Source: §5.4 · pp. 8–9, Figure 9 · p. 9
5.5.1 Experimental Settings.
- MP1 tuning grid-searches 49 Glucose variable-decay and clause-decay combinations, while LEC-CORP uses HEBO to tune three CaDiCaL parameters under a 1,000-second runtime limit.Both settings augment the original benchmarks fivefold with generated instances to guide hyperparameter selection.Source: §5.5.1 · p. 9, §5.5 · p. 9
- 22.19% performance gain on MP1 and +15.03% on LEC-CORP; on LEC-CORP, HardSATGEN alone achieves a positive gain, versus the previous best of -7.02%.On MP1, its gain surpasses the best previous method by 140.7%.Source: §5.5.2 · p. 9, Table 5 · p. 9
6 CONCLUSION
The conclusion attributes prior learning-based methods’ hardness-reproduction limitation, presumably, to homogeneity in single-stage split-merge procedures, and presents HardSATGEN as a multi-stage pipeline for better matching formula structure and computational properties.
6 CONCLUSION
- HardSATGEN introduces a multi-stage, fine-grained-control generation pipeline to better mimic SAT formula structure and computational properties.The authors say the limitation of earlier learning-based methods in reproducing hardness can presumably stem from homogeneity in their single-stage split-merge procedure.Source: §6 · p. 9
A IMPLEMENTATION DETAILS
The implementation uses graph networks and community-based phases to generate formulas, then scrambles and post-processes cores to target hardness; inputs and outputs use DIMACS CNF.
A.1 Details of the Model including Hyper-parameter Setting
- Three-layer GCN and SAGE networks use 4-element one-hot node-type features projected to 32 dimensions; training runs 200 epochs, and inference selects the highest-probability pair among 100 candidates.The phase-transition parameter α is 1.2 for MP1 and 0.9 for SP4 and LEC-CORP.Source: §A.1 · p. 11
A.2 Details of Community-based Phase Division
- Community information is represented in LCG using community nodes and a variable-to-community affiliation list; separate networks learn cross-community and in-community connections and guide sequential merges.The affiliation list supports community lookup using the variable nodes’ one-hop neighborhood.Source: §A.2 · p. 11
A.3 Details of Core Scrambling Algorithm
- Core scrambling obtains an unsatisfiable core by solving with CaDiCaL and analyzing its DRAT proof with DRAT-trim; the resulting core is not unique.The passage says detected cores in industrial instances with recognizable solving hardness have a major impact on computational hardness.Source: §A.3 · p. 11
A.4 Details of Post-processing
- Post-processing loosens unexpected small cores by adding a variable to a clause outside the original core, iterating until solver runtime reaches a tunable hardness threshold.The threshold can be set to fit the original formula and reference benchmark.Source: §A.4 · p. 11
A.5 CNF Representation
- The CNF inputs use textual DIMACS format: header lines specify comments or variable and clause counts, followed by clauses as disjunctions of integer-encoded literals.Variables are positive integers beginning at 1, with negation represented in the format.Source: §A.5 · p. 11
B.1 Evaluation
The evaluation estimates modularity with Louvain and scale-free parameters with maximum likelihood; experiments use different GPUs for competition and corporate datasets.
B.1 Evaluation
- Modularity uses the Louvain algorithm, while α_v and α_c are estimated by maximum likelihood.Source: §B.1 · p. 11
B.2 Computing Facilities
- MP1 and SP4 experiments run on a GeForce RTX 3090; LEC-CORP experiments run on a Tesla V100.Source: §B.2 · p. 11
C MORE EXPERIMENTAL RESULTS
The appendix reports HardSATGEN’s SAGE learning curves on MP1 datasets and visualizes generated LCGs against baselines using the same graph template.
C.1 Learning Curves
- Figure 10 reports HardSATGEN with SAGE on MP1 datasets using loss and training/testing AUC and ACC.Source: §C.1 · p. 11
C.2 Visualization of the Generations
- Figure 11 visualizes un-postprocessed generated LCGs; HardSATGEN and baselines share a template and use Fruchterman–Reingold layouts.Source: §C.2 · p. 11
C.3 More Results of Solver Runtime
HardSATGEN recovers computational hardness across all three mainstream SAT solvers; Tables 6 and 7 compare Kissat and Glucose runtimes with original benchmarks.
C.3 More Results of Solver Runtime
- HardSATGEN recovers computational hardness across all three mainstream SAT solvers.Source: §C.3 · p. 11
- Tables 6 and 7 report Kissat and Glucose CPU runtime comparisons between generated formulae and original benchmarks; Glucose runs use a 1200-second timeout.Source: §C.3 · p. 11, Table 6 · p. 12, Table 7 · p. 12
C.4 More Results of Solver Ranking
HardSATGEN is the only method reported to recover ground-truth solver rankings on all templates, which indicates better recovery of formula computational properties.
C.4 More Results of Solver Ranking
- HardSATGEN is the only method to recover ground-truth solver rankings on all templates, indicating better recovery of formula computational properties.Source: §C.4 · p. 12