# Recursive Online Enumeration of All Minimal Unsatisfiable Subsets

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Aug 2017.

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

- [Logic-Based Explainability in Machine Learning](https://mlsanity.com/paper/2211.00541/) (2022)
- [Eliminating The Impossible, Whatever Remains Must Be True](https://mlsanity.com/paper/2206.09551/) (2022)
- [Anytime Approximate Formal Feature Attribution](https://mlsanity.com/paper/2312.06973/) (2023)
- [Flexible and Robust Counterfactual Explanations with Minimal Satisfiable Perturbations](https://mlsanity.com/paper/2309.04676/) (2023)
- [Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/2402.15524/) (2024)
- [An ASP-Based Framework for MUSes](https://mlsanity.com/paper/2507.03929/) (2025)
- [A Reduction of Input/Output Logics to SAT](https://mlsanity.com/paper/2508.16242/) (2025)
- [Hypergraph Neural Networks Accelerate MUS Enumeration](https://mlsanity.com/paper/2604.09001/) (2026)

## Abstract (arXiv)

In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subsets (MUSes). The more MUSes are identified, the more information about the conflicts among the constraints is obtained. However, a full enumeration of all MUSes is in general intractable due to the large number (even exponential) of possible conflicts. Moreover, to identify MUSes algorithms must test sets of constraints for their simultaneous satisfiabilty. The type of the test depends on the application domains. The complexity of tests can be extremely high especially for domains like temporal logics, model checking, or SMT. In this paper, we propose a recursive algorithm that identifies MUSes in an online manner (i.e., one by one) and can be terminated at any time. The key feature of our algorithm is that it minimizes the number of satisfiability tests and thus speeds up the computation. The algorithm is applicable to an arbitrary constraint domain and its effectiveness demonstrates itself especially in domains with expensive satisfiability checks. We benchmark our algorithm against state of the art algorithm on Boolean and SMT constraint domains and demonstrate that our algorithm really requires less satisfiability tests and consequently finds more MUSes in given time limits.