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

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,Chin)

机构地区：[1]华东师范大学计算机科学与软件工程学院,上海200062

出　　处：《计算机工程与科学》2018年第6期1067-1074,共8页Computer Engineering & Science

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

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

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]