Book chapter 971 views 318 downloads
On Computing the Union of MUSes
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!
|
first_indexed |
2019-07-12T21:35:41Z |
---|---|
last_indexed |
2019-07-12T21:35:41Z |
id |
cronfa50334 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>50334</id><entry>2019-05-14</entry><title>On Computing the Union of MUSes</title><swanseaauthors><author><sid>2b410f26f9324d6b06c2b98f67362d05</sid><ORCID>0000-0003-3021-0095</ORCID><firstname>Oliver</firstname><surname>Kullmann</surname><name>Oliver Kullmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2019-05-14</date><deptcode>SCS</deptcode><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.</abstract><type>Book chapter</type><journal>Lecture Notes in Computer Science</journal><volume>11628</volume><journalNumber/><paginationStart>211</paginationStart><paginationEnd>221</paginationEnd><publisher>Springer International Publishing</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783030242572</isbnPrint><isbnElectronic>9783030242589</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>minimal unsatisfiable subsets, infeasibility analysis, algorithms</keywords><publishedDay>1</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2019</publishedYear><publishedDate>2019-01-01</publishedDate><doi>10.1007/978-3-030-24258-9_15</doi><url>http://dx.doi.org/10.1007/978-3-030-24258-9_15</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2023-05-22T15:10:02.3866959</lastEdited><Created>2019-05-14T08:16:04.8296062</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Carlos</firstname><surname>Mencía</surname><order>1</order></author><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>2</order></author><author><firstname>Alexey</firstname><surname>Ignatiev</surname><order>3</order></author><author><firstname>Joao</firstname><surname>Marques-Silva</surname><order>4</order></author></authors><documents><document><filename>0050334-14052019081746.pdf</filename><originalFilename>paper_59.pdf</originalFilename><uploaded>2019-05-14T08:17:46.3070000</uploaded><type>Output</type><contentLength>338545</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2020-06-29T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807> |
spelling |
v2 50334 2019-05-14 On Computing the Union of MUSes 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2019-05-14 SCS 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. Book chapter Lecture Notes in Computer Science 11628 211 221 Springer International Publishing Cham 9783030242572 9783030242589 0302-9743 1611-3349 minimal unsatisfiable subsets, infeasibility analysis, algorithms 1 1 2019 2019-01-01 10.1007/978-3-030-24258-9_15 http://dx.doi.org/10.1007/978-3-030-24258-9_15 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2023-05-22T15:10:02.3866959 2019-05-14T08:16:04.8296062 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Carlos Mencía 1 Oliver Kullmann 0000-0003-3021-0095 2 Alexey Ignatiev 3 Joao Marques-Silva 4 0050334-14052019081746.pdf paper_59.pdf 2019-05-14T08:17:46.3070000 Output 338545 application/pdf Accepted Manuscript true 2020-06-29T00:00:00.0000000 true eng |
title |
On Computing the Union of MUSes |
spellingShingle |
On Computing the Union of MUSes Oliver Kullmann |
title_short |
On Computing the Union of MUSes |
title_full |
On Computing the Union of MUSes |
title_fullStr |
On Computing the Union of MUSes |
title_full_unstemmed |
On Computing the Union of MUSes |
title_sort |
On Computing the Union of MUSes |
author_id_str_mv |
2b410f26f9324d6b06c2b98f67362d05 |
author_id_fullname_str_mv |
2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann |
author |
Oliver Kullmann |
author2 |
Carlos Mencía Oliver Kullmann Alexey Ignatiev Joao Marques-Silva |
format |
Book chapter |
container_title |
Lecture Notes in Computer Science |
container_volume |
11628 |
container_start_page |
211 |
publishDate |
2019 |
institution |
Swansea University |
isbn |
9783030242572 9783030242589 |
issn |
0302-9743 1611-3349 |
doi_str_mv |
10.1007/978-3-030-24258-9_15 |
publisher |
Springer International Publishing |
college_str |
Faculty of Science and Engineering |
hierarchytype |
|
hierarchy_top_id |
facultyofscienceandengineering |
hierarchy_top_title |
Faculty of Science and Engineering |
hierarchy_parent_id |
facultyofscienceandengineering |
hierarchy_parent_title |
Faculty of Science and Engineering |
department_str |
School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science |
url |
http://dx.doi.org/10.1007/978-3-030-24258-9_15 |
document_store_str |
1 |
active_str |
0 |
description |
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. |
published_date |
2019-01-01T15:10:00Z |
_version_ |
1766603725942554624 |
score |
11.021648 |