Hypergraph Neural Networks Accelerate MUS Enumeration
2026-04-10 • Artificial Intelligence
Artificial IntelligenceMachine LearningLogic in Computer Science
AI summaryⓘ
The authors focus on a hard problem called finding Minimal Unsatisfiable Subsets (MUSes) in constraint satisfaction problems, which involves checking many possible combinations, making it very slow. They created a new method using Hypergraph Neural Networks that treats constraints and MUSes as parts of a graph to learn which checks are most useful. This method uses reinforcement learning to decide the best way to search, reducing the number of expensive checks needed. Their experiments show their approach can find more MUSes faster than traditional techniques without relying on specific problem details.
Minimal Unsatisfiable SubsetsConstraint Satisfaction ProblemsHypergraph Neural NetworksReinforcement LearningSatisfiability ChecksBoolean SatisfiabilityGraph Neural NetworksEnumeration Algorithms
Authors
Hiroya Ijima, Koichiro Yawata
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.