Premise Set Caching for Enumerating Minimal Correction Subsets


  • Alessandro Previti University of Helsinki
  • Carlos Mencía University of Oviedo
  • Matti Järvisalo University of Helsinki
  • Joao Marques-Silva University of Lisbon


inconsistency analysis, minimal corrections subsets, enumeration, caching


Methods for explaining the sources of inconsistency of overconstrained systems find an ever-increasing number of applications, ranging from diagnosis and configuration to ontology debugging and axiom pinpointing in description logics. Efficient enumeration of minimal correction subsets (MCSes), defined as sets of constraints whose removal from the system restores feasibility, is a central task in such domains. In this work, we propose a novel approach to speeding up MCS enumeration over conjunctive normal form propositional formulas by caching of so-called premise sets (PSes) seen during the enumeration process. Contrasting to earlier work, we move from caching unsatisfiable cores to caching PSes and propose a more effective way of implementing the cache. The proposed techniques noticeably improves on the performance of state-of-the-art MCS enumeration algorithms in practice.




How to Cite

Previti, A., Mencía, C., Järvisalo, M., & Marques-Silva, J. (2018). Premise Set Caching for Enumerating Minimal Correction Subsets. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1). Retrieved from



Main Track: Search and Constraint Satisfaction