Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings
Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings
复制标题
满意度测试的理论与应用 - SAT 2019 - 第 22 届国际会议，SAT 2019，葡萄牙里斯本，2019 年 7 月 9-12 日，会议记录
DOI：
10.1007/978-3-030-24258-9_15
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Mencía C
中科院分区：
文献类型：
--
作者：
Mencía C
本文研究了不可满足CNF公式，并讨论了极小不可满足子公式（MUS）中子句的并的计算问题。MUSes的并集是不可行性分析中的一个有用的概念，因为它总结了给定公式不可满足的所有原因。本文提出了一种新的算法，开发了一个完善的递归枚举的MUSes强大的修剪技术的基础上。实验结果表明，该方法的实用性。
This paper considers unsatisfiable CNF formulas and addresses the problem of computing the union of the clauses included in some minimally unsatisfiable subformula (MUS). The union of MUSes represents a useful notion in infeasibility analysis since it summarizes all the causes for the unsatisfiability of a given formula. The paper proposes a novel algorithm for this problem, developing a refined recursive enumeration of MUSes based on powerful pruning techniques. Experimental results indicate the practical suitability of the approach.