No Cover Image

Book chapter 861 views 304 downloads

On Computing the Union of MUSes

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

Lecture Notes in Computer Science, Volume: 11628, Pages: 211 - 221

Swansea University Author: Oliver Kullmann Orcid Logo

Check full text

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

Full description

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

Similar Items