On the superiority of conflict-driven search in MUs enumeration

Research output: Contribution to journalConference articleResearchpeer-review

Abstract

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
JournalCEUR Workshop Proceedings
Volume2289
Publication statusPublished - 1 Jan 2018
Event29th International Workshop on Principles of Diagnosis, DX 2018 - Warsaw, Poland
Duration: 27 Aug 201830 Aug 2018

Fingerprint

Model checking
Set theory

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

On the superiority of conflict-driven search in MUs enumeration. / Koitz-Hristov, Roxane; Wotawa, Franz.

In: CEUR Workshop Proceedings, Vol. 2289, 01.01.2018.

Research output: Contribution to journalConference articleResearchpeer-review

@article{3a3a355453fe4b389693be099fbcb3ff,
title = "On the superiority of conflict-driven search in MUs enumeration",
abstract = "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.",
author = "Roxane Koitz-Hristov and Franz Wotawa",
year = "2018",
month = "1",
day = "1",
language = "English",
volume = "2289",
journal = "CEUR Workshop Proceedings",
issn = "1613-0073",
publisher = "RWTH Aachen",

}

TY - JOUR

T1 - On the superiority of conflict-driven search in MUs enumeration

AU - Koitz-Hristov, Roxane

AU - Wotawa, Franz

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85059820193&partnerID=8YFLogxK

M3 - Conference article

VL - 2289

JO - CEUR Workshop Proceedings

JF - CEUR Workshop Proceedings

SN - 1613-0073

ER -