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

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

MCS calculation based on unsatisfiable reasons

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.