# Hypergraph Neural Networks Accelerate MUS Enumeration

arXiv: https://arxiv.org/abs/2604.09001 · HTML: https://mlsanity.com/paper/2604.09001/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 26 of its 51 references that are in the map.
- First posted on arXiv 10 Apr 2026.

## Builds on (most cited first, 26 of 26)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Hypergraph Neural Networks](https://mlsanity.com/paper/1809.09401/) (2018)
- [Hypergraph Convolution and Hypergraph Attention](https://mlsanity.com/paper/1901.08150/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [UniGNN: a Unified Framework for Graph and Hypergraph Neural Networks](https://mlsanity.com/paper/2105.00956/) (2021)
- [You are AllSet: A Multiset Function Framework for Hypergraph Neural Networks](https://mlsanity.com/paper/2106.13264/) (2021)
- [HNHN: Hypergraph Networks with Hyperedge Neurons](https://mlsanity.com/paper/2006.12278/) (2020)
- [Hyper-SAGNN: a self-attention based graph neural network for hypergraphs](https://mlsanity.com/paper/1911.02613/) (2019)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [HyperSAGE: Generalizing Inductive Representation Learning on Hypergraphs](https://mlsanity.com/paper/2010.04558/) (2020)
- [One Model, Any CSP: Graph Neural Networks as Fast Global Search Heuristics for Constraint Satisfaction](https://mlsanity.com/paper/2208.10227/) (2022)
- [A Survey on Hypergraph Neural Networks: An In-Depth and Step-By-Step Guide](https://mlsanity.com/paper/2404.01039/) (2024)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [Graph Neural Networks and Boolean Satisfiability](https://mlsanity.com/paper/1702.03592/) (2017)
- [Recursive Online Enumeration of All Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/1708.00400/) (2017)
- [Recent Advances in Hypergraph Neural Networks](https://mlsanity.com/paper/2503.07959/) (2025)
- [Tunable Online MUS/MSS Enumeration](https://mlsanity.com/paper/1606.03289/) (2016)
- [Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/2402.15524/) (2024)
- [A Reinforcement Learning based Reset Policy for CDCL SAT Solvers](https://mlsanity.com/paper/2404.03753/) (2024)

## Abstract (arXiv)

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.