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