On the superiority of conflict-driven search in MUs enumeration

Publikation: Beitrag in einer Fachzeitschrift!!Conference articleForschungBegutachtung

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.

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

Fingerprint

Model checking
Set theory

ASJC Scopus subject areas

  • !!Computer Science(all)

Dies zitieren

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

in: CEUR Workshop Proceedings, Jahrgang 2289, 01.01.2018.

Publikation: Beitrag in einer Fachzeitschrift!!Conference articleForschungBegutachtung

@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 -