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.

翻译：给定一个不可满足的公式，理解其不可满足的核心原因在多个应用场景中至关重要。捕捉这一原因的一种有效方式是通过最小不可满足子集（MUS），即保持不可满足性的子句集合中满足子集极小性的集合。当前研究主要聚焦于两个方向：（i）在给定时间限制内枚举尽可能多的MUS；（ii）计算给定不可满足公式的MUS总数。本文提出了一种基于回答集编程的框架，命名为MUS-ASP，专为在线枚举MUS而设计。ASP因其在知识表示方面的优势而成为一种强大工具，尤其适用于描述复杂的组合问题。通过将MUS枚举问题转化为回答集求解问题，MUS-ASP能够充分利用先进ASP系统的计算效率。我们广泛的实验评估证明了MUS-ASP的有效性，并突显了其在MUS枚举与计数任务中的加速效果，尤其是在与混合求解器（包括本文提出的框架）集成时。