Hypergraph Neural Networks Accelerate MUS Enumeration
A neural network speeds up a core debugging task in software and hardware verification — but only in experiments, not yet in production tools.
The Thesis
Constraint satisfaction problems (CSPs) — puzzles where a system must find assignments satisfying a set of rules — appear in hardware design, scheduling, and formal software verification. When a CSP is unsatisfiable (no solution exists), engineers need to know *which* constraints are causing the conflict. Finding a Minimal Unsatisfiable Subset, or MUS, is the standard diagnostic tool: the smallest group of constraints that are jointly impossible to satisfy. The catch is that finding all MUSes requires exponentially many 'satisfiability checks' — expensive calls to a solver that asks 'is this subset still solvable?' This paper proposes using a Hypergraph Neural Network (HGNN) — a neural net that operates on hypergraphs, where a single edge can connect more than two nodes — to learn which subsets are likely to contain an MUS, reducing the number of solver calls needed. The approach is domain-agnostic, meaning it is not limited to Boolean logic problems as earlier ML methods were.
Catalyst
Earlier machine learning approaches to MUS finding were tightly coupled to Boolean satisfiability (SAT) problems and required explicit variable-constraint structure that does not generalize. Hypergraph neural networks have matured enough to represent arbitrary constraint structures without that assumption. Reinforcement learning frameworks capable of training agents on combinatorial search problems are also now widely available as open infrastructure.
What's New
Prior ML-based MUS acceleration methods — such as those built on graph neural networks for SAT — encode constraints as bipartite graphs of variables and clauses, a structure that only exists in Boolean logic. This paper replaces that representation with a hypergraph where constraints are nodes and discovered MUSes become hyperedges, making the method applicable to any CSP regardless of domain. The authors claim their reinforcement-learning-trained HGNN agent finds more MUSes within a fixed solver-call budget than conventional heuristic enumeration methods.
The Counter
The paper benchmarks its method only on experimental CSP instances, with no reported results on industrial-scale verification problems from real chip design or software analysis workflows. Satisfiability checks in production hardware verification can take hours each; it is entirely unclear whether the HGNN's inference overhead amortizes favorably at that scale. The reinforcement learning agent must be retrained — or at least fine-tuned — for each new problem domain, which is a significant barrier for the 'domain-agnostic' claim the authors make. Conventional MUS enumeration tools like MARCO and FORQES have been heavily engineered over many years with problem-specific heuristics; beating them on wall-clock time in realistic settings is a much higher bar than reducing raw solver-call counts. The paper also does not release code or benchmarks publicly, making independent validation impossible at this stage.
Longs
- CDNS — Cadence Design Systems, whose formal verification tools depend on satisfiability solvers
- SNPS — Synopsys, a direct competitor in EDA formal verification
- BOTZ (robotics/automation ETF) — indirect exposure to constraint-solving in industrial automation
Shorts
- Vendors of hand-tuned MUS enumeration heuristics embedded in legacy EDA tools, if learned methods prove faster at scale
Enablers (Picks & Shovels)
- PyTorch Geometric — open-source library for graph and hypergraph neural networks
- MiniSAT / CaDiCaL — open-source SAT solvers used as the underlying satisfiability oracle
- OpenAI Gym / Gymnasium — RL environment frameworks used to train the agent
Private Watchlist
- Certora — formal verification for smart contracts, relies on constraint solving
- Formal Vindications — formal methods startup ecosystem
Resources
The Paper
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.