Book chapter 861 views 304 downloads
On Computing the Union of MUSes
Carlos Mencía,
Oliver Kullmann 
,
Alexey Ignatiev,
Joao Marques-Silva
,
Alexey Ignatiev,
Joao Marques-Silva
Lecture Notes in Computer Science, Volume: 11628, Pages: 211 - 221
Swansea University Author:
Oliver Kullmann
-
PDF | Accepted Manuscript
Download (384.9KB)
DOI (Published version): 10.1007/978-3-030-24258-9_15
Abstract
The situation is considered where a satisfiability problem represents for example a manufacturing specification, and thus unsatisfiability of the problem means that something is wrong with the specification. In response to this an infeasibility analysis is needed, where we consider the robust notion...
| Published in: | Lecture Notes in Computer Science |
|---|---|
| ISBN: | 9783030242572 9783030242589 |
| ISSN: | 0302-9743 1611-3349 |
| Published: |
Cham
Springer International Publishing
2019
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa50334 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
The situation is considered where a satisfiability problem represents for example a manufacturing specification, and thus unsatisfiability of the problem means that something is wrong with the specification. In response to this an infeasibility analysis is needed, where we consider the robust notion of "union of MUSes", that is, all clauses need to be computed, which are potentially necessary for the contradiction to arise (become necessary after some some other clauses are removed).The paper proposes a novel algorithm for this problem, proves its correctness, and provides experimental evidence for practical applicability. |
|---|---|
| Keywords: |
minimal unsatisfiable subsets, infeasibility analysis, algorithms |
| College: |
Faculty of Science and Engineering |
| Start Page: |
211 |
| End Page: |
221 |