# Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 53 references that are in the map.
- First posted on arXiv 19 Feb 2024.

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

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Graph Neural Networks: A Review of Methods and Applications](https://mlsanity.com/paper/1812.08434/) (2018)
- [Weisfeiler and Leman Go Neural: Higher-order Graph Neural Networks](https://mlsanity.com/paper/1810.02244/) (2018)
- [Learning Combinatorial Optimization Algorithms over Graphs](https://mlsanity.com/paper/1704.01665/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [The Surprising Power of Graph Neural Networks with Random Node Initialization](https://mlsanity.com/paper/2010.01179/) (2020)
- [Random Features Strengthen Graph Neural Networks](https://mlsanity.com/paper/2002.03155/) (2020)
- [Combinatorial Optimization with Graph Convolutional Networks and Guided Tree Search](https://mlsanity.com/paper/1810.10659/) (2018)
- [A Survey on Heterogeneous Graph Embedding: Methods, Techniques, Applications and Sources](https://mlsanity.com/paper/2011.14867/) (2020)
- [Combinatorial Optimization with Physics-Inspired Graph Neural Networks](https://mlsanity.com/paper/2107.01188/) (2021)
- [Approximation Ratios of Graph Neural Networks for Combinatorial Problems](https://mlsanity.com/paper/1905.10261/) (2019)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Graph Neural Networks for Maximum Constraint Satisfaction](https://mlsanity.com/paper/1909.08387/) (2019)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [Deep Graph Similarity Learning: A Survey](https://mlsanity.com/paper/1912.11615/) (2019)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [RAPid-Learn: A Framework for Learning to Recover for Handling Novelties in Open-World Environments](https://mlsanity.com/paper/2206.12493/) (2022)
- [Learning to Reason: Leveraging Neural Networks for Approximate DNF Counting](https://mlsanity.com/paper/1904.02688/) (2019)
- [Recursive Online Enumeration of All Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/1708.00400/) (2017)
- [Tunable Online MUS/MSS Enumeration](https://mlsanity.com/paper/1606.03289/) (2016)
- [Towards Accurate Subgraph Similarity Computation via Neural Graph Pruning](https://mlsanity.com/paper/2210.10643/) (2022)

## Built on by (most cited first, 2 of 2)

- [An ASP-Based Framework for MUSes](https://mlsanity.com/paper/2507.03929/) (2025)
- [Hypergraph Neural Networks Accelerate MUS Enumeration](https://mlsanity.com/paper/2604.09001/) (2026)

## Abstract (arXiv)

Finding Minimal Unsatisfiable Subsets (MUSes) of binary constraints is a common problem in infeasibility analysis of over-constrained systems. However, because of the exponential search space of the problem, enumerating MUSes is extremely time-consuming in real applications. In this work, we propose to prune formulas using a learned model to speed up MUS enumeration. We represent formulas as graphs and then develop a graph-based learning model to predict which part of the formula should be pruned. Importantly, our algorithm does not require data labeling by only checking the satisfiability of pruned formulas. It does not even require training data from the target application because it extrapolates to data with different distributions. In our experiments we combine our algorithm with existing MUS enumerators and validate its effectiveness in multiple benchmarks including a set of real-world problems outside our training distribution. The experiment results show that our method significantly accelerates MUS enumeration on average on these benchmark problems.