@inproceedings{PrevitiMJM:SAT2017,
author = {Alessandro Previti and Carlos Mencia and Matti J\"arvisalo and Joao Marques-Silva},
title = {Improving {MCS} Enumeration via Caching},
booktitle = {Proceedings of the 20th International Conference on
             Theory and Applications of Satisfiability Testing (SAT 2017)},
editor = {Serge Gaspers and Toby Walsh},
pages = {184--194},
volume = {10491},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2017},
}

Abstract:

Enumeration of minimal correction sets (MCSes) of conjunctive normal form
formulas is a central and highly intractable problem in infeasibility
analysis of constraint systems. Often complete enumeration of MCSes is
impossible due to both high computational cost and worst-case exponential
number of MCSes. In such cases partial enumeration is sought for, finding
applications in various domains, including axiom pinpointing in
description logics among others. In this work we propose caching as a
means of further improving the practical efficiency of current MCS
enumeration approaches, and show the potential of caching via an empirical
evaluation.