On the superiority of conflict-driven search in MUs enumeration

Publikation: Beitrag in einer FachzeitschriftKonferenzartikel


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.

FachzeitschriftCEUR Workshop Proceedings
PublikationsstatusVeröffentlicht - 1 Jan 2018
Veranstaltung29th International Workshop on Principles of Diagnosis, DX 2018 - Warsaw, Polen
Dauer: 27 Aug 201830 Aug 2018

ASJC Scopus subject areas

  • !!Computer Science(all)


Untersuchen Sie die Forschungsthemen von „On the superiority of conflict-driven search in MUs enumeration“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren