No Cover Image

Book chapter 1396 views

Computing Maximal Autarkies with Few and Simple Oracle Queries

Oliver Kullmann Orcid Logo, João Marques-Silva

Theory and Applications of Satisfiability Testing -- SAT 2015, Volume: 9340, Pages: 138 - 155

Swansea University Author: Oliver Kullmann Orcid Logo

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1007/978-3-319-24318-4_11

Abstract

We consider the algorithmic task of computing a maximal autarky for a clause-set F, i.e., a partial assignment which satisfies every clause of F it touches, and where this property is destroyed by adding any non-empty set of further assignments.We employ SAT solvers as oracles, using various capabil...

Full description

Published in: Theory and Applications of Satisfiability Testing -- SAT 2015
Published: 2015
URI: https://cronfa.swan.ac.uk/Record/cronfa26207
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2016-06-06T03:15:30Z
last_indexed 2018-02-09T05:07:55Z
id cronfa26207
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2016-07-25T14:57:16.9819153</datestamp><bib-version>v2</bib-version><id>26207</id><entry>2016-02-15</entry><title>Computing Maximal Autarkies with Few and Simple Oracle Queries</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>2016-02-15</date><deptcode>SCS</deptcode><abstract>We consider the algorithmic task of computing a maximal autarky for a clause-set F, i.e., a partial assignment which satisfies every clause of F it touches, and where this property is destroyed by adding any non-empty set of further assignments.We employ SAT solvers as oracles, using various capabilities. Using the standard SAT oracle, log_2(n(F)) oracle calls suffice, where n(F) is the number of variables, but the drawback is that (translated) cardinality constraints are employed, which makes this approach less efficient in practice.Using an extended SAT oracle, motivated by the capabilities of modern SAT solvers, we show how to compute maximal autarkies with 2 n(F)^{1/2} simpler oracle calls. This novel algorithm combines the previous two main approaches, based on the autarky-resolution duality and on SAT translations.</abstract><type>Book chapter</type><journal>Theory and Applications of Satisfiability Testing -- SAT 2015</journal><volume>9340</volume><paginationStart>138</paginationStart><paginationEnd>155</paginationEnd><publisher/><isbnPrint/><isbnElectronic/><issnPrint/><keywords>Algorithms for hard problems, SAT</keywords><publishedDay>27</publishedDay><publishedMonth>10</publishedMonth><publishedYear>2015</publishedYear><publishedDate>2015-10-27</publishedDate><doi>10.1007/978-3-319-24318-4_11</doi><url/><notes>Lecture Notes in Computer Science 9340</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2016-07-25T14:57:16.9819153</lastEdited><Created>2016-02-15T09:17:42.0808705</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>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>1</order></author><author><firstname>Jo&#xE3;o</firstname><surname>Marques-Silva</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2016-07-25T14:57:16.9819153 v2 26207 2016-02-15 Computing Maximal Autarkies with Few and Simple Oracle Queries 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2016-02-15 SCS We consider the algorithmic task of computing a maximal autarky for a clause-set F, i.e., a partial assignment which satisfies every clause of F it touches, and where this property is destroyed by adding any non-empty set of further assignments.We employ SAT solvers as oracles, using various capabilities. Using the standard SAT oracle, log_2(n(F)) oracle calls suffice, where n(F) is the number of variables, but the drawback is that (translated) cardinality constraints are employed, which makes this approach less efficient in practice.Using an extended SAT oracle, motivated by the capabilities of modern SAT solvers, we show how to compute maximal autarkies with 2 n(F)^{1/2} simpler oracle calls. This novel algorithm combines the previous two main approaches, based on the autarky-resolution duality and on SAT translations. Book chapter Theory and Applications of Satisfiability Testing -- SAT 2015 9340 138 155 Algorithms for hard problems, SAT 27 10 2015 2015-10-27 10.1007/978-3-319-24318-4_11 Lecture Notes in Computer Science 9340 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2016-07-25T14:57:16.9819153 2016-02-15T09:17:42.0808705 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Oliver Kullmann 0000-0003-3021-0095 1 João Marques-Silva 2
title Computing Maximal Autarkies with Few and Simple Oracle Queries
spellingShingle Computing Maximal Autarkies with Few and Simple Oracle Queries
Oliver Kullmann
title_short Computing Maximal Autarkies with Few and Simple Oracle Queries
title_full Computing Maximal Autarkies with Few and Simple Oracle Queries
title_fullStr Computing Maximal Autarkies with Few and Simple Oracle Queries
title_full_unstemmed Computing Maximal Autarkies with Few and Simple Oracle Queries
title_sort Computing Maximal Autarkies with Few and Simple Oracle Queries
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Oliver Kullmann
João Marques-Silva
format Book chapter
container_title Theory and Applications of Satisfiability Testing -- SAT 2015
container_volume 9340
container_start_page 138
publishDate 2015
institution Swansea University
doi_str_mv 10.1007/978-3-319-24318-4_11
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
document_store_str 0
active_str 0
description We consider the algorithmic task of computing a maximal autarky for a clause-set F, i.e., a partial assignment which satisfies every clause of F it touches, and where this property is destroyed by adding any non-empty set of further assignments.We employ SAT solvers as oracles, using various capabilities. Using the standard SAT oracle, log_2(n(F)) oracle calls suffice, where n(F) is the number of variables, but the drawback is that (translated) cardinality constraints are employed, which makes this approach less efficient in practice.Using an extended SAT oracle, motivated by the capabilities of modern SAT solvers, we show how to compute maximal autarkies with 2 n(F)^{1/2} simpler oracle calls. This novel algorithm combines the previous two main approaches, based on the autarky-resolution duality and on SAT translations.
published_date 2015-10-27T03:31:20Z
_version_ 1763751263469568000
score 11.035634

Similar Items