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

摘要：

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

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

所属期刊栏目：40

分类号：TP311(计算技术、计算机技术)

资助基金：国家973计划2009CB723803;国家自然科学基金60873120

在线出版日期：2018-07-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：1067-1074