MUST: Minimal Unsatisfiable Subsets Enumeration Tool
MUST: Minimal Unsatisfiable Subsets Enumeration Tool
复制标题
DOI：
10.1007/978-3-030-45190-5_8
复制
发表时间：
2020-03-13
期刊：
影响因子：
--
通讯作者：
Černá I
中科院分区：
文献类型：
--
作者：
Bendík J;Černá I
在计算机科学的许多领域，我们被给予一组不可满足的约束，目的是提供对不可满足性的洞察。一种常见的方法是识别约束集的最小不可满足子集(MUS)。发现的缪斯越多，获得的洞察力就越好。然而，由于可以有多个指数级的缪斯，它们的完整列举可能很难处理。因此，我们专注于在线列举缪斯女神的算法，即逐个列举，从而即使在难以处理的情况下也能找到至少一些缪斯女神。由于缪斯模型在不同的约束域中都有应用，新的应用也不断涌现，人们已经提出了几种领域无关的算法。这样的算法可以应用于任何约束域，因此理论上可以作为所有新兴应用的现成解决方案。然而，几乎没有领域不可知的工具，即既实现领域不可知算法又可以很容易地扩展以支持任何约束域的工具。在这项工作中，我们通过引入一个名为MASH的领域不可知工具来弥合这一差距。我们的工具超越了其他现有的领域不可知工具，而且，它甚至与完全特定于领域的解决方案竞争。
In many areas of computer science, we are given an unsatisfiable set of constraints with the goal to provide an insight into the unsatisfiability. One of common approaches is to identify minimal unsatisfiable subsets (MUSes) of the constraint set. The more MUSes are identified, the better insight is obtained. However, since there can be up to exponentially many MUSes, their complete enumeration might be intractable. Therefore, we focus on algorithms that enumerate MUSes online, i.e. one by one, and thus can find at least some MUSes even in the intractable cases. Since MUSes find applications in different constraint domains and new applications still arise, there have been proposed several domain agnostic algorithms. Such algorithms can be applied in any constraint domain and thus theoretically serve as ready-to-use solutions for all the emerging applications. However, there are almost no domain agnostic tools, i.e. tools that both implement domain agnostic algorithms and can be easily extended to support any constraint domain. In this work, we close this gap by introducing a domain agnostic tool called MUST. Our tool outperforms other existing domain agnostic tools and moreover, it is even competitive to fully domain specific solutions.
登录
查看更多内容
影响因子：
5
作者：
Cimatti, Alessandro;Griggio, Alberto;Sebastiani, Roberto
通讯作者：
Sebastiani, Roberto
DOI：
10.1007/978-3-540-24605-3_37
发表时间：
2004-01-01
期刊：
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
影响因子：
--
作者：
Eén, N;Sörensson, N
通讯作者：
Sörensson, N
DOI：
10.1109/3477.752801
发表时间：
1999-04-01
影响因子：
--
作者：
Han, B;Lee, SJ
通讯作者：
Lee, SJ
影响因子：
1.6
作者：
Liffiton, Mark H.;Previti, Alessandro;Marques-Silva, Joao
通讯作者：
Marques-Silva, Joao
影响因子：
0.8
作者：
Sperner, E
通讯作者：
Sperner, E