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

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. [ABSTRACT FROM AUTHOR]