Boosting MCSes Enumeration
Abstract
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.
Cite
Text
Grégoire et al. "Boosting MCSes Enumeration." International Joint Conference on Artificial Intelligence, 2018. doi:10.24963/IJCAI.2018/182Markdown
[Grégoire et al. "Boosting MCSes Enumeration." International Joint Conference on Artificial Intelligence, 2018.](https://mlanthology.org/ijcai/2018/gregoire2018ijcai-boosting/) doi:10.24963/IJCAI.2018/182BibTeX
@inproceedings{gregoire2018ijcai-boosting,
title = {{Boosting MCSes Enumeration}},
author = {Grégoire, Éric and Izza, Yacine and Lagniez, Jean-Marie},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2018},
pages = {1309-1315},
doi = {10.24963/IJCAI.2018/182},
url = {https://mlanthology.org/ijcai/2018/gregoire2018ijcai-boosting/}
}