基于不可满足原因的最小纠正集求解

计算机工程与科学

基于不可满足原因的最小纠正集求解

胡潇洒，张越岭，李建文，蒲戈光，张敏

（华东师范大学计算机科学与软件工程学院，上海 200062）

收稿日期:2017-10-05 修回日期:2017-12-17 出版日期:2018-06-25 发布日期:2018-06-25
基金资助:
国家973计划（2009CB723803）；国家自然科学基金（60873120）

MCS calculation based on unsatisfiable reasons

HU Xiaosa，ZHANG Yueling，LI Jianwen，PU Geguang，ZHANG Min

（School of Computer Science and Software Engineering,East China Normal University,Shanghai 200062,China）

Received:2017-10-05 Revised:2017-12-17 Online:2018-06-25 Published:2018-06-25

摘要/Abstract

摘要：

布尔公式的最小纠正集MCS是子句的集合。对于一个不可满足公式，移除MCS后，所得到的新公式可满足。任一MCS中的子句保留在公式中，所得到的新公式不可满足。通过求解MCS 并调整约束集合，能够求解最小不可满足核心、MaxSAT 问题和最大（小）可满足解问题；还能够应用于故障定位、模型检查配置优化等实际问题中。
提出了一种基于不可满足原因的MCS求解算法，实现了相应的CUC工具。通过与目前最好的MCS求解工具LBX进行比较，得到了CUC性能优于LBX的结论。CUC比LBX平均多解出5%（65个）的公式。对于CUC和LBX均可解出的公式，CUC的平均求解时间比LBX快2.5倍。

关键词: 可满足性, 最小纠正集, 软件验证

Abstract:

The minimal correction subset (MCS) of a Boolean formula is a set of clauses. By removing the MCS from a given unsatisfiable formula, the new generated formula becomes satisfiable. For any clause in the MCS, keeping the clause in the given unsatisfiable formula results in a new unsatisfiable formula. Minimal unsatisfiable core, MaxSAT and maximal (minimal) partial assignment can be solved by solving the MCS and adjusting the set of constraints. The MCS can also be applied to practical problems such as fault localization, model checking and configuration optimization. We propose an MCS calculation algorithm based on unsatisfiable reasons returned from SAT solvers, and implement a corresponding tool named CUC. Comparing with the state-of-theart tool LBX, the CUC outperforms LBX. The CUC can solve 5% (65) more formulas on average, and it is 2.5 times faster than LBX.

Key words: satisfiability, MCS, software verification

胡潇洒，张越岭，李建文，蒲戈光，张敏. 基于不可满足原因的最小纠正集求解[J]. 计算机工程与科学.

HU Xiaosa，ZHANG Yueling，LI Jianwen，PU Geguang，ZHANG Min. MCS calculation based on unsatisfiable reasons[J]. Computer Engineering & Science.

[1]	唐傲, 王晓峰, 何飞. 可满足性模理论综述[J]. 计算机工程与科学, 2024, 46(03): 400-415.
[2]	黎兴玉, 何星星, 马雪, 李莹芳. 命题逻辑中一种矛盾体生成新方法[J]. 计算机工程与科学, 2023, 45(06): 1134-1140.
[3]	王欣怡, 殷志祥, 唐震, 杨静, 崔建中, . 基于DNA折纸术求解可满足性问题的计算模型[J]. 计算机工程与科学, 2021, 43(09): 1529-1537.
[4]	张建民，黎铁军，马柯帆，肖立权. 基于一阶逻辑的可满足求解方法研究进展[J]. 计算机工程与科学, 2019, 41(12): 2119-2126.
[5]	罗炜麟，魏欧，黄鸣宇. 基于SAT求解器的故障树最小割集求解算法[J]. 计算机工程与科学, 2017, 39(04): 725-733.
[6]	马柯帆，肖立权,张建民，黎铁军. 基于硬件可编程逻辑的SAT求解算法研究与进展[J]. J4, 2016, 38(04): 634-639.
[7]	何安平，吴尽昭，梁艺，熊玲芳，吴昊. 基于几何规划的布尔可满足问题求解方法[J]. J4, 2013, 35(9): 122-126.
[8]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[9]	张建民, 沈胜宇, 李思昆. 可满足性求解技术研究[J]. J4, 2010, 32(1): 50-54.