Boosting MCSes Enumeration

Boosting MCSes Enumeration

Éric Grégoire, Yacine Izza, Jean-Marie Lagniez

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Main track. Pages 1309-1315. https://doi.org/10.24963/ijcai.2018/182

The enumeration of all Maximal Satisfiable Subsets (MSSes) or all Minimal Correction Subsets (MCSes) of an unsatisfiable CNF Boolean formula is a useful and sometimes necessary step for solving a variety of important A.I. issues. Although the number of different MCSes of a CNF Boolean formula is exponential in the worst case, it remains low in many practical situations; this makes the tentative enumeration possibly successful in these latter cases. In the paper, a technique is introduced that boosts the currently most efficient practical approaches to enumerate MCSes. It implements a model rotation paradigm that allows the set of MCSes to be computed in an heuristically efficient way.
Keywords:
Constraints and SAT: Constraints and SAT
Constraints and SAT: SAT
Constraints and SAT: SAT: Solvers and Tools