Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An ASP-Based Framework for MUSes

Mohimenul Kabir, Kuldeep S Meel

TL;DR

The work introduces MUS-$ASP$, an ASP-based framework for online enumeration and counting of minimal unsatisfiable subsets (MUS) of an unsatisfiable formula $F$. By encoding MUS identification as subset-minimal answer sets and leveraging ASP solvers, the method achieves competitive and often superior enumeration and counting performance, especially when integrated with hybrid strategies. The authors establish theoretical correctness via a bijection between answer sets and unsatisfiable cores, and they introduce heuristics (H1–H5) to prune the search space while preserving completeness. Experimental results across benchmarks show MUS-$ASP$ outperforms several baselines, with notable gains from the heuristics and hybridization, and a direction toward approximate MUS counting using XOR-enabled ASP is suggested for future work.

Abstract

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.

An ASP-Based Framework for MUSes

TL;DR

The work introduces MUS-, an ASP-based framework for online enumeration and counting of minimal unsatisfiable subsets (MUS) of an unsatisfiable formula . By encoding MUS identification as subset-minimal answer sets and leveraging ASP solvers, the method achieves competitive and often superior enumeration and counting performance, especially when integrated with hybrid strategies. The authors establish theoretical correctness via a bijection between answer sets and unsatisfiable cores, and they introduce heuristics (H1–H5) to prune the search space while preserving completeness. Experimental results across benchmarks show MUS- outperforms several baselines, with notable gains from the heuristics and hybridization, and a direction toward approximate MUS counting using XOR-enabled ASP is suggested for future work.

Abstract

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.

Paper Structure

This paper contains 27 sections, 4 theorems, 2 equations, 1 figure, 4 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Propositional Logic
  4. Minimal Hitting Set Duality
  5. Answer Set Programming
  6. Related Works
  7. MUS Enumeration.
  8. MUS Counting.
  9. Subset-minimal Answer Sets.
  10. Methodology
  11. ASP Encoding of $\mathsf{MUS}$-$\mathsf{ASP}$
  12. Theoretical Correctness
  13. Optimizing MUS Computation with Heuristics
  14. $\mathsf{\mathbf{H}}_{1}$ Union of MUSes.
  15. $\mathsf{\mathbf{H}}_{2}$ Minimum and Maximum Cardinalities of MUSes.
  16. ...and 12 more sections

Key Result

Theorem 1

There is a bijective correspondence between the answer sets of $\mathcal{P}_{F}$ and the unsatisfiable cores of $F$, under the projection onto $\Lambda$.

Figures (1)

  • Figure 1: Runtime performance of $\mathsf{MUS}$-$\mathsf{ASP}$ and existing MUS counters on MUS counting. A point $(x,y)$ on the plot denotes that a tool counted $x$ instances within $y$ seconds.

Theorems & Definitions (7)

  • Example 1
  • Theorem 1
  • Proposition 1
  • Example 1: continued
  • Proposition 2
  • Theorem 1
  • proof