HyperGEN: A Masked Variational Hypergraph Framework for Hard UNSAT Instance Generation

Realistic and challenging Boolean satisfiability (SAT) instances are essential for evaluating modern SAT solvers and training learning-based solver components, yet such instances are often scarce in application-specific domains. Existing SAT generators either rely on handcrafted structural priors or generate new formulas through predefined graph transformations, which do not explicitly model how clauses are formed. In this paper, we propose HyperGEN, a masked variational hypergraph framework for hard UNSAT instance generation. HyperGEN represents each formula in conjunctive normal form as a literal-clause hypergraph, where literals are vertices and clauses are hyperedges. It formulates instance generation as masked hyperedge reconstruction. HyperGEN employs a masked variational hypergraph autoencoder that combines a hypergraph neural network for structural encoding with latent variables, and reconstructs each masked clause through arity and membership prediction. Experiments on real-world SAT benchmarks show that HyperGEN consistently generates more challenging instances than existing generative baselines, generalizes to larger unseen instances without retraining, and provides effective data augmentation for downstream solver-runtime prediction.