An ASP-Based Framework for MUSes

TL;DR

This paper introduces MUS-ASP, an answer set programming framework for efficiently enumerating and counting minimal unsatisfiable subsets (MUSes) in propositional formulas, enhancing performance in knowledge representation tasks.

Contribution

The paper presents a novel ASP-based approach for online MUS enumeration and counting, leveraging ASP's strengths for complex combinatorial problem solving.

Findings

MUS-ASP significantly accelerates MUS enumeration.

MUS-ASP improves MUS counting efficiency.

Hybrid solvers with MUS-ASP outperform existing methods.

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.