On computing the union of MUSes

Carlos Mencía; Oliver Kullmann; Alexey Ignatiev; Joao Marques-Silva

doi:10.1007/978-3-030-24258-9_15

On computing the union of MUSes

Carlos Mencía, Oliver Kullmann, Alexey Ignatiev, Joao Marques-Silva

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

4 Citations (Scopus)

Abstract

This paper considers unsatisfiable CNF formulas and addresses the problem of computing the union of the clauses included in some minimally unsatisfiable subformula (MUS). The union of MUSes represents a useful notion in infeasibility analysis since it summarizes all the causes for the unsatisfiability of a given formula. The paper proposes a novel algorithm for this problem, developing a refined recursive enumeration of MUSes based on powerful pruning techniques. Experimental results indicate the practical suitability of the approach.

Original language	English
Title of host publication	Theory and Applications of Satisfiability Testing – SAT 2019
Subtitle of host publication	22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings
Editors	Mikoláš Janota, Inês Lynce
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	211-221
Number of pages	11
ISBN (Electronic)	9783030242589
ISBN (Print)	9783030242572
DOIs	https://doi.org/10.1007/978-3-030-24258-9_15
Publication status	Published - 2019
Externally published	Yes
Event	International Conference on Theory and Applications of Satisfiability Testing 2019 - Lisbon, Portugal Duration: 7 Jul 2019 → 12 Jul 2019 Conference number: 22nd http://sat2019.tecnico.ulisboa.pt/

Publication series

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

Conference

Conference	International Conference on Theory and Applications of Satisfiability Testing 2019
Abbreviated title	SAT 2019
Country	Portugal
City	Lisbon
Period	7/07/19 → 12/07/19
Internet address	http://sat2019.tecnico.ulisboa.pt/

Access to Document

10.1007/978-3-030-24258-9_15

Link to publication in Scopus

Cite this

Mencía, C., Kullmann, O., Ignatiev, A., & Marques-Silva, J. (2019). On computing the union of MUSes. In M. Janota, & I. Lynce (Eds.), Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings (pp. 211-221). (Lecture Notes in Computer Science; Vol. 11628 ). Springer. https://doi.org/10.1007/978-3-030-24258-9_15

Mencía, Carlos ; Kullmann, Oliver ; Ignatiev, Alexey ; Marques-Silva, Joao. / On computing the union of MUSes. Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings. editor / Mikoláš Janota ; Inês Lynce. Cham Switzerland : Springer, 2019. pp. 211-221 (Lecture Notes in Computer Science).

@inproceedings{ecaf534948c64c26bd992f7f14f656ad,

title = "On computing the union of MUSes",

abstract = "This paper considers unsatisfiable CNF formulas and addresses the problem of computing the union of the clauses included in some minimally unsatisfiable subformula (MUS). The union of MUSes represents a useful notion in infeasibility analysis since it summarizes all the causes for the unsatisfiability of a given formula. The paper proposes a novel algorithm for this problem, developing a refined recursive enumeration of MUSes based on powerful pruning techniques. Experimental results indicate the practical suitability of the approach.",

author = "Carlos Menc{\'i}a and Oliver Kullmann and Alexey Ignatiev and Joao Marques-Silva",

year = "2019",

doi = "10.1007/978-3-030-24258-9_15",

language = "English",

isbn = "9783030242572",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "211--221",

editor = "Mikol{\'a}{\v s} Janota and In{\^e}s Lynce",

booktitle = "Theory and Applications of Satisfiability Testing – SAT 2019",

note = "International Conference on Theory and Applications of Satisfiability Testing 2019, SAT 2019 ; Conference date: 07-07-2019 Through 12-07-2019",

url = "http://sat2019.tecnico.ulisboa.pt/",

}

Mencía, C, Kullmann, O, Ignatiev, A & Marques-Silva, J 2019, On computing the union of MUSes. in M Janota & I Lynce (eds), Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings. Lecture Notes in Computer Science, vol. 11628 , Springer, Cham Switzerland, pp. 211-221, International Conference on Theory and Applications of Satisfiability Testing 2019, Lisbon, Portugal, 7/07/19. https://doi.org/10.1007/978-3-030-24258-9_15

On computing the union of MUSes. / Mencía, Carlos; Kullmann, Oliver; Ignatiev, Alexey; Marques-Silva, Joao.

Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings. ed. / Mikoláš Janota; Inês Lynce. Cham Switzerland : Springer, 2019. p. 211-221 (Lecture Notes in Computer Science; Vol. 11628 ).

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

TY - GEN

T1 - On computing the union of MUSes

AU - Mencía, Carlos

AU - Kullmann, Oliver

AU - Ignatiev, Alexey

AU - Marques-Silva, Joao

N1 - Conference code: 22nd

PY - 2019

Y1 - 2019

N2 - This paper considers unsatisfiable CNF formulas and addresses the problem of computing the union of the clauses included in some minimally unsatisfiable subformula (MUS). The union of MUSes represents a useful notion in infeasibility analysis since it summarizes all the causes for the unsatisfiability of a given formula. The paper proposes a novel algorithm for this problem, developing a refined recursive enumeration of MUSes based on powerful pruning techniques. Experimental results indicate the practical suitability of the approach.

AB - This paper considers unsatisfiable CNF formulas and addresses the problem of computing the union of the clauses included in some minimally unsatisfiable subformula (MUS). The union of MUSes represents a useful notion in infeasibility analysis since it summarizes all the causes for the unsatisfiability of a given formula. The paper proposes a novel algorithm for this problem, developing a refined recursive enumeration of MUSes based on powerful pruning techniques. Experimental results indicate the practical suitability of the approach.

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

U2 - 10.1007/978-3-030-24258-9_15

DO - 10.1007/978-3-030-24258-9_15

M3 - Conference Paper

SN - 9783030242572

T3 - Lecture Notes in Computer Science

SP - 211

EP - 221

BT - Theory and Applications of Satisfiability Testing – SAT 2019

A2 - Janota, Mikoláš

A2 - Lynce, Inês

PB - Springer

CY - Cham Switzerland

T2 - International Conference on Theory and Applications of Satisfiability Testing 2019

Y2 - 7 July 2019 through 12 July 2019

ER -

Mencía C, Kullmann O, Ignatiev A, Marques-Silva J. On computing the union of MUSes. In Janota M, Lynce I, editors, Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings. Cham Switzerland: Springer. 2019. p. 211-221. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-24258-9_15