Smallest MUS extraction with minimal hitting set dualization

Alexey Ignatiev, Alessandro Previti, Mark Liffiton, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

41 Citations (Scopus)


Minimal explanations of infeasibility are of great interest in many domains. In propositional logic, these are referred to as Minimal Unsatisfiable Subsets (MUSes). An unsatisfiable formula can have multiple MUSes, some of which provide more insights than others. Different criteria can be considered in order to identify a good minimal explanation. Among these, the size of an MUS is arguably one of the most intuitive. Moreover, computing the smallest MUS (SMUS) finds several practical applications that include validating the quality of the MUSes computed by MUS extractors and finding equivalent subformulae of smallest size, among others. This paper develops a novel algorithm for computing a smallest MUS, and we show that it outperforms all the previous alternatives pushing the state of the art in SMUS solving. Although described in the context of propositional logic, the presented technique can also be applied to other constraint systems.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings
EditorsGilles Pesant
Place of PublicationCham Switzerland
Number of pages10
ISBN (Electronic)9783319232195
ISBN (Print)9783319232188
Publication statusPublished - 2015
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2015 - Cork, Ireland
Duration: 31 Aug 20154 Sep 2015
Conference number: 21st

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Principles and Practice of Constraint Programming 2015
Abbreviated titleCP 2015
Internet address


  • Propositional Logic
  • Conjunctive Normal Form
  • Propositional Formula
  • Conjunctive Normal Form Formula
  • Minimal Explanation

Cite this