用ASP框架在线枚举不可满足子集，提升求解效率。
An ASP-Based Framework for MUSes
- 将MUS枚举转为答案集编程求解，利用ASP高效建模能力。
- 实验显示在混合求解器中显著加速枚举与计数任务。
- 适合需快速定位不可满足根源的逻辑验证与调试场景。
给定一个不可满足公式，理解其不可满足的原因在多个应用中至关重要。一种有效方法是通过最小不可满足子集（MUS），即保持不可满足性的子集最小集合。当前研究主要集中在两个方向：(i) 在限定时间内尽可能多地枚举MUS；(ii) 计算给定不可满足公式的MUS总数。本文提出基于答案集编程（ASP）的框架MUS-ASP，用于在线枚举MUS。ASP具有强大的知识表示能力，特别适合描述复杂组合问题。通过将MUS枚举转化为答案集求解，MUS-ASP利用现代ASP系统在计算上的高效性。大量实验评估表明，MUS-ASP在性能上表现出色，尤其在集成到混合求解器中时，在MUS枚举与计数任务中均实现显著加速。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。