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

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

单位：华东师范大学计算机科学与软件工程学院; 上海200062