Hypergraph Neural Networks Accelerate MUS Enumeration

Hiroya Ijima; Koichiro Yawata

cs.AIApr 10, 2026

Hypergraph Neural Networks Accelerate MUS Enumeration

Authors: Hiroya Ijima, Koichiro Yawata

Organizations: Hitachi, Ltd.

Abstract

Enumerating Minimal Unsatisfiable Subsets (MUSes) is a fundamental task in constraint satisfaction problems (CSPs). Its major challenge is the exponential growth of the search space, which becomes particularly severe when satisfiability checks are expensive. Recent machine learning approaches reduce this cost for Boolean satisfiability problems but rely on explicit variable-constraint relationships, limiting their application domains. This paper proposes a domain-agnostic method to accelerate MUS enumeration using Hypergraph Neural Networks (HGNNs). The proposed method incrementally builds a hypergraph with constraints as vertices and MUSes enumerated until the current step as hyperedges, and employs an HGNN-based agent trained via reinforcement learning to minimize the number of satisfiability checks required to obtain an MUS. Experimental results demonstrate the effectiveness of our approach in accelerating MUS enumeration, showing that our method can enumerate more MUSes within the same satisfiability check budget compared to conventional methods.

Figures & tables

Figure 1: Overview of HyMUSE. HyMUSE is a domain-agnostic method to accelerate MUS/MSS enumeration using Hypergraph Neural Networks (HGNNs). HyMUSE constructs a hypergraph whose vertices are constraints and whose hyperedges are MUSes and MCSes (only MUSes are illustrated in this figure). The HGNN-based agent takes the hypergraph of MUSes/MCSes enumerated until the current step and the subset of constraints to shrink/grow as input, and outputs a tentative MUS/MSS candidate. The candidate is then corrected to a valid MUS/MSS. The agent is trained via reinforcement learning with reward designed to minimize the number of calls to the satisfiability checking oracle required for the correction.

Figure 2: Architecture of Hypergraph Neural Networks. The input is the MUS/MCS hypergraph and the subset of constraints to be shrunk/grown, shown as gray-colored nodes. The feature vectors of vertices are initialized with spectral embeddings based on the hypergraph Laplacian and updated by AllSetTransformer layers. Then, the feature vectors of constraints in the action candidate set are updated separately by two transformer decoders to output the policy and value.

Figure 3

Figure 4

Figure 3: Reward Transition during Training. The average reward and the standard deviation are plotted.

Figure 4: Comparison of MARCO with and without the Agent on

SAT_{small}

. The x-axis shows the number of MUSes/MSSes found with the agent, and the y-axis shows the number found without the agent within 10,000 checks. Points below the dashed

y=x

line indicate improvement by the agent. Points on the line are instances where both methods found all MUSes/MSSes.

Figure 5: Relation of Number of MUSes/MSSes and Number of Satisfiability Checks. The number of MUSes/MSSes is plotted against the number of satisfiability checks for both MARCO with and without the agent.

Quartile	1k checks	5k checks	10k checks
1Q	1.80 $\pm$ 0.57	2.05 $\pm$ 0.55	1.73 $\pm$ 0.58
2Q	1.78 $\pm$ 0.47	1.90 $\pm$ 0.40	1.89 $\pm$ 0.33
3Q	1.77 $\pm$ 0.36	1.82 $\pm$ 0.31	1.86 $\pm$ 0.33
4Q	1.57 $\pm$ 0.29	1.61 $\pm$ 0.31	1.67 $\pm$ 0.33
Overall	1.74 $\pm$ 0.45	1.85 $\pm$ 0.43	1.79 $\pm$ 0.42

Table 1: Improvement Ratio of MARCO with the Agent on

SAT_{small}

. The improvement ratio is calculated as the number of MUSes/MSSes with the agent divided by that without the agent at each instance and averaged across instances in each quartile group and overall. The quartiles are based on the number of MUSes/MSSes enumerated without the agent.

Dataset	# MUSes/MSSes		Ratio
$SAT_{small}$	w/o Agent	119.5 $\pm$ 60.3	1.79 $\pm$ 0.42
$SAT_{small}$	w/ Agent	$\bm{211.3}$ $\pm$ $\bm{99.4}$	1.79 $\pm$ 0.42
$SAT_{large}$	w/o Agent	54.1 $\pm$ 15.3	2.46 $\pm$ 0.42
$SAT_{large}$	w/ Agent	$\bm{130.6}$ $\pm$ $\bm{31.6}$	2.46 $\pm$ 0.42
$GC$	w/o Agent	15.1 $\pm$ 16.1	2.32 $\pm$ 0.96
$GC$	w/ Agent	$\bm{31.6}$ $\pm$ $\bm{28.4}$	2.32 $\pm$ 0.96

Table 2: The Number of MUSes/MSSes with and without the Agent and the Improvement Ratio on Different Datasets at 10k Checks. The number of MUSes/MSSes and the improvement ratio are averaged across instances in each dataset and shown with standard deviation.

Method	1k checks	5k checks	10k checks
TOME	0.92 $\pm$ 0.14	1.08 $\pm$ 0.18	1.11 $\pm$ 0.16
ReMUS	1.31 $\pm$ 0.29	1.05 $\pm$ 0.37	0.75 $\pm$ 0.29

Table 3: Improvement Ratio by Integrating the Agent with Different Enumeration Methods on

SAT_{small}

. The improvement ratio is calculated as the number of MUSes/MSSes found by each enumeration method with the agent divided by that without the agent at each instance and averaged across instances.

Appendix figures & tables8 assets

Supplementary material from the paper’s appendix.

Appendix

Dataset	$N_{check}$	$N^{\prime}_{check}$	$N_{infer}$	$r_{eff}$
$SAT_{small}$	85 $\pm$ 37	44 $\pm$ 17	48 $\pm$ 24	0.83 $\pm$ 0.11
$SAT_{large}$	196 $\pm$ 51	81 $\pm$ 22	127 $\pm$ 37	0.90 $\pm$ 0.08
$GC$	996 $\pm$ 540	478 $\pm$ 312	673 $\pm$ 422	0.77 $\pm$ 0.27
$SMT$	136 $\pm$ 313	117 $\pm$ 428	94 $\pm$ 243	0.25 $\pm$ 0.71

Appendix

Table 4: Average Number of Checks and Inference Calls for Extracting an MUS/MSS with and without the Agent and the Effective Ratio

r_{eff}

on Different Datasets. The numbers are averaged across instances in each dataset and shown with standard deviation.

Agent	1k checks	5k checks	10k checks
Trained	1.74 $\pm$ 0.45	1.85 $\pm$ 0.43	1.79 $\pm$ 0.42
Untrained	1.02 $\pm$ 0.22	0.93 $\pm$ 0.15	0.88 $\pm$ 0.11

Appendix

Table 5: The Improvement Ratio in the Number of MUSes/MSSes when Integrating Trained and Untrained Agents with MARCO on

SAT_{small}

. The numbers are averaged across instances and shown with standard deviation.

Method	MARCO	TOME	ReMUS
w/o Agent	(1.00)	1.52 $\pm$ 0.48	$\mathbf{3.29\pm 1.54}$
w/ Agent	1.79 $\pm$ 0.42	1.69 $\pm$ 0.57	2.16 $\pm$ 0.58

Appendix

Table 6: Normalized Number of MUSes/MSSes Enumerated with Different Enumeration Methods on

SAT_{small}

. The numbers are normalized by that of MARCO without the agent at each instance and averaged across instances.

Method	MARCO	TOME	ReMUS
w/o Agent	(1.00)	1.51 $\pm$ 0.48	$\mathbf{3.26\pm 1.48}$
w/ Agent	1.85 $\pm$ 0.44	1.67 $\pm$ 0.56	2.19 $\pm$ 0.59

Appendix

Table 7: Normalized Number of MUSes/MSSes Enumerated within 10,000 Satisfiability Checks on

SAT_{small}

with and without the Agent Trained with ReMUS.

Method	MARCO	TOME	ReMUS
w/o Agent	(1.00)	2.17 $\pm$ 0.40	2.00 $\pm$ 0.73
w/ Agent	2.50 $\pm$ 0.43	2.47 $\pm$ 0.47	$\mathbf{3.01\pm 0.41}$

Appendix

Table 8: Normalized Number of MUSes/MSSes Enumerated within 10,000 Satisfiability Checks on

SAT_{large}

with and without the Agent Trained with ReMUS.

Figure 6: Comparison of MARCO with and without the Agent on

SAT_{large}

Figure 7: Comparison of MARCO with and without the Agent on

GC

Figure 8: Comparison of MARCO with and without the Agent on

SMT

Constraint Satisfaction

Constraint satisfaction studies how to find or optimize assignments that obey interacting rules across discrete and structured problems.

See all 86 papers

Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems
Feb 20, 2026Geri Skenderi, Lorenzo Buffoni, Francesco D'Amico +6Constraint Satisfaction Neural Combinatorial Optimization
Department of Computing Sciences, Bocconi University, Milan, Italy · Bocconi Institute for Data Science and Analytics (BIDSA) · Department of Physics and Astronomy and INFN, University of Florence +4
Compute Time Scaling with Recursive Models for Combinatorial Optimization
Sep 28, 2026Zhengxi Zhang, Paul SwobodaTraveling Salesperson Problem Inference-Time Scaling
Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations
Apr 16, 2026Koyena Pal, Serdar KadiogluUnsupervised Representation Learning Transfer Learning
AI Center of Excellence, Fidelity Investments, USA · Khoury College of Computer Sciences, Northeastern University, USA · Department of Computer Science, Brown University, USA

Feb 20, 2026J/K move · Enter open · S save

Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems

Geri Skenderi, Lorenzo Buffoni, Francesco D'Amico, David Machado+5

Department of Computing Sciences, Bocconi University, Milan, Italy · Bocconi Institute for Data Science and Analytics (BIDSA) · Department of Physics and Astronomy and INFN, University of Florence+4

Constraint Satisfaction Neural Combinatorial Optimization

Open paper AskPDF arXiv

Graph neural networks (GNNs) are increasingly applied to hard optimization problems, often claiming superiority over classical heuristics. However, such claims risk being unsolid due to a lack of standard benchmarks on truly hard instances. From a statistical physics perspective, we propose new hard benchmarks based on random problems. We provide these benchmarks, along with performance results from both classical heuristics and GNNs. Our fair comparison shows that classical algorithms still outperform GNNs. We discuss the challenges for neural networks in this domain. Future claims of superiority can be made more robust using our benchmarks, available at https://github.com/ArtLabBocconi/RandCSPBench.

Abstract

Constraint Satisfaction

Explore similar work

Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems

Compute Time Scaling with Recursive Models for Combinatorial Optimization

Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations