No Cover Image

Conference Paper/Proceeding/Abstract 293 views 84 downloads

On Computing the Union of MUSes

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

Theory and Applications of Satisfiability Testing – SAT 2019, Volume: 11628, Pages: 211 - 221

Swansea University Author: Oliver Kullmann Orcid Logo

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

Full description

Published in: Theory and Applications of Satisfiability Testing – SAT 2019
ISBN: 978-3-030-24257-2 978-3-030-24258-9
ISSN: 0302-9743 1611-3349
Published: Springer, Cham
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"?><rfc1807><datestamp>2019-07-12T16:16:57.9724156</datestamp><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>Conference Paper/Proceeding/Abstract</type><journal>Theory and Applications of Satisfiability Testing &#x2013; SAT 2019</journal><volume>11628</volume><paginationStart>211</paginationStart><paginationEnd>221</paginationEnd><publisher>Springer, Cham</publisher><isbnPrint>978-3-030-24257-2</isbnPrint><isbnElectronic>978-3-030-24258-9</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>minimal unsatisfiable subsets, infeasibility analysis, algorithms</keywords><publishedDay>0</publishedDay><publishedMonth>0</publishedMonth><publishedYear>0</publishedYear><publishedDate>0001-01-01</publishedDate><doi>10.1007/978-3-030-24258-9_15</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-07-12T16:16:57.9724156</lastEdited><Created>2019-05-14T08:16:04.8296062</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Carlos</firstname><surname>Menc&#xED;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 2019-07-12T16:16:57.9724156 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. Conference Paper/Proceeding/Abstract Theory and Applications of Satisfiability Testing – SAT 2019 11628 211 221 Springer, Cham 978-3-030-24257-2 978-3-030-24258-9 0302-9743 1611-3349 minimal unsatisfiable subsets, infeasibility analysis, algorithms 0 0 0 0001-01-01 10.1007/978-3-030-24258-9_15 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2019-07-12T16:16:57.9724156 2019-05-14T08:16:04.8296062 College of 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_***_0000-0003-3021-0095
author Oliver, Kullmann
author2 Carlos Mencía
Oliver Kullmann
Alexey Ignatiev
Joao Marques-Silva
format Conference Paper/Proceeding/Abstract
container_title Theory and Applications of Satisfiability Testing – SAT 2019
container_volume 11628
container_start_page 211
institution Swansea University
isbn 978-3-030-24257-2
978-3-030-24258-9
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-030-24258-9_15
publisher Springer, Cham
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
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 0001-01-01T04:15:41Z
_version_ 1723079790695546880
score 10.853483