On the superiority of conflict-driven search in MUS enumeration

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.