On the superiority of conflict-driven search in MUS enumeration

Research output: Contribution to journalConference articlepeer-review


The extraction of minimal unsatisfiable cores from an unsatisfiable set of constraints is a computationally hard problem that finds application in a variety of tasks such as model checking, configuration, or diagnosis. Domain-agnostic algorithms for online minimal unsatisfiable subset enumeration allow the computation of all conflicts and can be applied to any type of constraint system. We aim at extending this research by combining two well-known approaches from different research communities; on the one hand, we exploit the traversal of the power set as suggested by the MARCO algorithm in the domain of infeasibility analysis and on the other hand, we take advantage of the implicit exploration of the search space as proposed by HS-DAG in model-based diagnosis. In particular, we show that the conflict-driven search utilized by HS-DAG renders MARCO’s SAT calls unnecessary and given a certain problem structure a combination of both is advantageous in domains where consistency checks are expensive.

Original languageEnglish
Number of pages7
JournalCEUR Workshop Proceedings
Publication statusPublished - 1 Jan 2018
Event29th International Workshop on Principles of Diagnosis, DX 2018 - Warsaw, Poland
Duration: 27 Aug 201830 Aug 2018

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'On the superiority of conflict-driven search in MUS enumeration'. Together they form a unique fingerprint.

Cite this