# An ASP-Based Framework for MUSes

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 90 references that are in the map.
- First posted on arXiv 5 Jul 2025.

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

- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [ASP-Core-2 Input Language Format](https://mlsanity.com/paper/1911.04326/) (2019)
- [A Scalable Approximate Model Counter](https://mlsanity.com/paper/1306.5726/) (2013)
- [Recursive Online Enumeration of All Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/1708.00400/) (2017)
- [Debugging Non-Ground ASP Programs: Technique and Graphical Tools](https://mlsanity.com/paper/1808.00417/) (2018)
- [Partition Function Estimation: A Quantitative Study](https://mlsanity.com/paper/2105.11132/) (2021)
- [On the Tractability of Minimal Model Computation for Some CNF Theories](https://mlsanity.com/paper/1310.8120/) (2013)
- [Tunable Online MUS/MSS Enumeration](https://mlsanity.com/paper/1606.03289/) (2016)
- [Solving the Identifying Code Set Problem with Grouped Independent Support](https://mlsanity.com/paper/2306.15693/) (2023)
- [Exact ASP Counting with Compact Encodings](https://mlsanity.com/paper/2312.11936/) (2023)
- [On Lower Bounding Minimal Model Count](https://mlsanity.com/paper/2407.09744/) (2024)
- [Backdoors to Normality for Disjunctive Logic Programs](https://mlsanity.com/paper/1301.1391/) (2013)
- [Specifying and Exploiting Non-Monotonic Domain-Specific Declarative Heuristics in Answer Set Programming](https://mlsanity.com/paper/2209.09066/) (2022)
- [Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/2402.15524/) (2024)
- [Minimal Model Counting via Knowledge Compilation](https://mlsanity.com/paper/2409.10170/) (2024)
- [Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks](https://mlsanity.com/paper/2506.06013/) (2025)
- [Computing maximal autarkies with few and simple oracle queries](https://mlsanity.com/paper/1505.02371/) (2015)

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

- [Counting Answer Sets of Disjunctive Answer Set Programs](https://mlsanity.com/paper/2507.11655/) (2025)

## Abstract (arXiv)

Given an unsatisfiable formula, understanding the core reason for unsatisfiability is crucial in several applications. One effective way to capture this is through the minimal unsatisfiable subset (MUS), the subset-minimal set of clauses that remains unsatisfiable. Current research broadly focuses on two directions: (i) enumerating as many MUSes as possible within a given time limit, and (ii) counting the total number of MUSes for a given unsatisfiable formula. In this paper, we introduce an answer set programming-based framework, named MUS-ASP, designed for online enumeration of MUSes. ASP is a powerful tool for its strengths in knowledge representation and is particularly suitable for specifying complex combinatorial problems. By translating MUS enumeration into answer set solving, MUS-ASP leverages the computational efficiency of state-of-the-art ASP systems. Our extensive experimental evaluation demonstrates the effectiveness of MUS-ASP and highlights the acceleration in both MUS enumeration and counting tasks, particularly when integrated within hybrid solvers, including the framework proposed in this paper.