• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

Computer Engineering & Science

Previous Articles     Next Articles

MCS calculation based on unsatisfiable reasons

HU Xiaosa,ZHANG Yueling,LI Jianwen,PU Geguang,ZHANG Min   

  1. (School of Computer Science and Software Engineering,East China Normal University,Shanghai 200062,China)
  • Received:2017-10-05 Revised:2017-12-17 Online:2018-06-25 Published:2018-06-25

Abstract:

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.
 

Key words: satisfiability, MCS, software verification