A New Approach to Partial MUS Enumeration
A New Approach to Partial MUS Enumeration
复制标题
部分MUS枚举的新方法
DOI：
10.1007/978-3-319-24318-4_28
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
M. Kaufmann
中科院分区：
文献类型：
--
作者：
Christian Zielke;M. Kaufmann
在约束集中寻找不可行性的最小解释是多年来已知的问题。最近的发展缩小了枚举布尔域中不可满足公式的所有最小不可满足子集 (MUS) 的方法与仅提取一个 MUS 的方法之间的差距。这些新算法被描述为部分 MUS 枚举器。当在一定时间限制内不可能进行完整枚举时，它们提供了一个可行的选择。本文开发了一种新颖的方法来识别 MUS 中存在或不存在的相同子句。有了这个概念，我们使用其已经建立的框架提高了一些最先进的部分 MUS 枚举器的性能。在我们的方法中，我们主要关注更快地确定最小校正集，以随后改进 MUS 发现。广泛的实际分析表明我们的扩展性能有所提高。
Searching for minimal explanations of infeasibility in constraint sets is a problem known for many years. Recent developments closed a gap between approaches that enumerate all minimal unsatisfiable subsets (MUSes) of an unsatisfiable formula in the Boolean domain and approaches that extract only one single MUS. These new algorithms are described as partial MUS enumerators. They offer a viable option when complete enumeration is not possible within a certain time limit.This paper develops a novel method to identify clauses that are identical regarding their presence or absence in MUSes. With this concept we improve the performance of some of the state-of-the-art partial MUS enumerators using its already established framework. In our approach we focus mainly on determining minimal correction sets much faster to improve the MUS finding subsequently. An extensive practical analysis shows the increased performance of our extensions.