Smallest MUS extraction with minimal hitting set dualization

Alexey Ignatiev; Alessandro Previti; Mark Liffiton; Joao Marques-Silva

doi:10.1007/978-3-319-23219-5_13

Smallest MUS extraction with minimal hitting set dualization

Alexey Ignatiev, Alessandro Previti, Mark Liffiton, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

41 Citations (Scopus)

Abstract

Minimal explanations of infeasibility are of great interest in many domains. In propositional logic, these are referred to as Minimal Unsatisfiable Subsets (MUSes). An unsatisfiable formula can have multiple MUSes, some of which provide more insights than others. Different criteria can be considered in order to identify a good minimal explanation. Among these, the size of an MUS is arguably one of the most intuitive. Moreover, computing the smallest MUS (SMUS) finds several practical applications that include validating the quality of the MUSes computed by MUS extractors and finding equivalent subformulae of smallest size, among others. This paper develops a novel algorithm for computing a smallest MUS, and we show that it outperforms all the previous alternatives pushing the state of the art in SMUS solving. Although described in the context of propositional logic, the presented technique can also be applied to other constraint systems.

Original language	English
Title of host publication	Principles and Practice of Constraint Programming
Subtitle of host publication	21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings
Editors	Gilles Pesant
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	173-182
Number of pages	10
ISBN (Electronic)	9783319232195
ISBN (Print)	9783319232188
DOIs	https://doi.org/10.1007/978-3-319-23219-5_13
Publication status	Published - 2015
Externally published	Yes
Event	International Conference on Principles and Practice of Constraint Programming 2015 - Cork, Ireland Duration: 31 Aug 2015 → 4 Sep 2015 Conference number: 21st https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9255
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Principles and Practice of Constraint Programming 2015
Abbreviated title	CP 2015
Country/Territory	Ireland
City	Cork
Period	31/08/15 → 4/09/15
Internet address	https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015

Keywords

Propositional Logic
Conjunctive Normal Form
Propositional Formula
Conjunctive Normal Form Formula
Minimal Explanation

Access to Document

10.1007/978-3-319-23219-5_13

Cite this

Ignatiev, A., Previti, A., Liffiton, M., & Marques-Silva, J. (2015). Smallest MUS extraction with minimal hitting set dualization. In G. Pesant (Ed.), Principles and Practice of Constraint Programming: 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings (pp. 173-182). (Lecture Notes in Computer Science ; Vol. 9255). Springer. https://doi.org/10.1007/978-3-319-23219-5_13

Ignatiev, Alexey ; Previti, Alessandro ; Liffiton, Mark et al. / Smallest MUS extraction with minimal hitting set dualization. Principles and Practice of Constraint Programming: 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. editor / Gilles Pesant. Cham Switzerland : Springer, 2015. pp. 173-182 (Lecture Notes in Computer Science ).

@inproceedings{09adff9885024d24867a400db5b5c4c3,

title = "Smallest MUS extraction with minimal hitting set dualization",

abstract = "Minimal explanations of infeasibility are of great interest in many domains. In propositional logic, these are referred to as Minimal Unsatisfiable Subsets (MUSes). An unsatisfiable formula can have multiple MUSes, some of which provide more insights than others. Different criteria can be considered in order to identify a good minimal explanation. Among these, the size of an MUS is arguably one of the most intuitive. Moreover, computing the smallest MUS (SMUS) finds several practical applications that include validating the quality of the MUSes computed by MUS extractors and finding equivalent subformulae of smallest size, among others. This paper develops a novel algorithm for computing a smallest MUS, and we show that it outperforms all the previous alternatives pushing the state of the art in SMUS solving. Although described in the context of propositional logic, the presented technique can also be applied to other constraint systems.",

keywords = "Propositional Logic, Conjunctive Normal Form, Propositional Formula, Conjunctive Normal Form Formula, Minimal Explanation",

author = "Alexey Ignatiev and Alessandro Previti and Mark Liffiton and Joao Marques-Silva",

year = "2015",

doi = "10.1007/978-3-319-23219-5_13",

language = "English",

isbn = "9783319232188",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "173--182",

editor = "Gilles Pesant",

booktitle = "Principles and Practice of Constraint Programming",

note = "International Conference on Principles and Practice of Constraint Programming 2015, CP 2015 ; Conference date: 31-08-2015 Through 04-09-2015",

url = "https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015",

}

Ignatiev, A, Previti, A, Liffiton, M & Marques-Silva, J 2015, Smallest MUS extraction with minimal hitting set dualization. in G Pesant (ed.), Principles and Practice of Constraint Programming: 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. Lecture Notes in Computer Science , vol. 9255, Springer, Cham Switzerland, pp. 173-182, International Conference on Principles and Practice of Constraint Programming 2015, Cork, Ireland, 31/08/15. https://doi.org/10.1007/978-3-319-23219-5_13

Smallest MUS extraction with minimal hitting set dualization. / Ignatiev, Alexey; Previti, Alessandro; Liffiton, Mark et al.

Principles and Practice of Constraint Programming: 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. ed. / Gilles Pesant. Cham Switzerland : Springer, 2015. p. 173-182 (Lecture Notes in Computer Science ; Vol. 9255).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Smallest MUS extraction with minimal hitting set dualization

AU - Ignatiev, Alexey

AU - Previti, Alessandro

AU - Liffiton, Mark

AU - Marques-Silva, Joao

N1 - Conference code: 21st

PY - 2015

Y1 - 2015

N2 - Minimal explanations of infeasibility are of great interest in many domains. In propositional logic, these are referred to as Minimal Unsatisfiable Subsets (MUSes). An unsatisfiable formula can have multiple MUSes, some of which provide more insights than others. Different criteria can be considered in order to identify a good minimal explanation. Among these, the size of an MUS is arguably one of the most intuitive. Moreover, computing the smallest MUS (SMUS) finds several practical applications that include validating the quality of the MUSes computed by MUS extractors and finding equivalent subformulae of smallest size, among others. This paper develops a novel algorithm for computing a smallest MUS, and we show that it outperforms all the previous alternatives pushing the state of the art in SMUS solving. Although described in the context of propositional logic, the presented technique can also be applied to other constraint systems.

AB - Minimal explanations of infeasibility are of great interest in many domains. In propositional logic, these are referred to as Minimal Unsatisfiable Subsets (MUSes). An unsatisfiable formula can have multiple MUSes, some of which provide more insights than others. Different criteria can be considered in order to identify a good minimal explanation. Among these, the size of an MUS is arguably one of the most intuitive. Moreover, computing the smallest MUS (SMUS) finds several practical applications that include validating the quality of the MUSes computed by MUS extractors and finding equivalent subformulae of smallest size, among others. This paper develops a novel algorithm for computing a smallest MUS, and we show that it outperforms all the previous alternatives pushing the state of the art in SMUS solving. Although described in the context of propositional logic, the presented technique can also be applied to other constraint systems.

KW - Propositional Logic

KW - Conjunctive Normal Form

KW - Propositional Formula

KW - Conjunctive Normal Form Formula

KW - Minimal Explanation

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

U2 - 10.1007/978-3-319-23219-5_13

DO - 10.1007/978-3-319-23219-5_13

M3 - Conference Paper

SN - 9783319232188

T3 - Lecture Notes in Computer Science

SP - 173

EP - 182

BT - Principles and Practice of Constraint Programming

A2 - Pesant, Gilles

PB - Springer

CY - Cham Switzerland

T2 - International Conference on Principles and Practice of Constraint Programming 2015

Y2 - 31 August 2015 through 4 September 2015

ER -

Ignatiev A, Previti A, Liffiton M, Marques-Silva J. Smallest MUS extraction with minimal hitting set dualization. In Pesant G, editor, Principles and Practice of Constraint Programming: 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. Cham Switzerland: Springer. 2015. p. 173-182. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-319-23219-5_13

Smallest MUS extraction with minimal hitting set dualization

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Cite this