所有极小不可满足子集的递归在线枚举
计算机科学中的逻辑
2018-05-09 v3
摘要
在计算机科学的各个领域中，我们都要处理一组需要满足的约束。如果这些约束无法同时满足，则期望找出其中的核心问题。这类核心被称为极小不可满足子集。识别出的 MUS 越多，获得的关于约束间冲突的信息就越多。然而，由于可能的冲突数量巨大（甚至呈指数级），对所有 MUS 的完整枚举通常是难解的。此外，为了识别 MUS，算法必须测试约束集的同时可满足性。测试的类型取决于应用领域。对于时序逻辑、模型检测或 SMT 等领域，测试的复杂度可能极高。在本文中，我们提出了一种递归算法，以在线方式（即逐一）识别 MUS，并且可以随时终止。我们算法的关键特征在于它最小化了可满足性测试的次数，从而加速了计算。该算法适用于任意约束域，其有效性在可满足性检查代价高昂的领域中尤为凸显。我们在布尔和 SMT 约束域上将我们的算法与现有技术算法进行了基准测试，并证明我们的算法确实需要更少的可满足性测试，因此在给定的时间限制内能找到更多的 MUS。
引用
@article{arxiv.1708.00400,
title = {Recursive Online Enumeration of All Minimal Unsatisfiable Subsets},
author = {Jaroslav Bendik and Ivana Cerna and Nikola Benes},
journal= {arXiv preprint arXiv:1708.00400},
year = {2018}
}