No Cover Image

Conference Paper/Proceeding/Abstract 1604 views

Generalising and Unifying SLUR and Unit-Refutation Completeness

Matthew Gwynne, Oliver Kullmann Orcid Logo

SOFSEM 2013: Theory and Practice of Computer Science. LCNS, Volume: 7741, Pages: 220 - 232

Swansea University Author: Oliver Kullmann Orcid Logo

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

Check full text

DOI (Published version): 10.1007/978-3-642-35843-2_20

Abstract

The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). W...

Full description

Published in: SOFSEM 2013: Theory and Practice of Computer Science. LCNS
ISSN: 0302-9743 1611-3349
Published: Springer 2013
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa13748
first_indexed 2013-07-23T12:10:50Z
last_indexed 2018-02-09T04:44:39Z
id cronfa13748
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T14:56:09.1324491</datestamp><bib-version>v2</bib-version><id>13748</id><entry>2012-12-17</entry><title>Generalising and Unifying SLUR and Unit-Refutation Completeness</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>2012-12-17</date><deptcode>MACS</deptcode><abstract>The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). We introduce a hierarchy SLUR_k which we argue is the natural &#x201C;limit&#x201D; of such approaches. The second source for our investigations is the class UC of unit-refutation complete clause-sets introduced in [del Val 1994]. Via the theory of (tree-resolution based) &#x201C;hardness&#x201D; of clause-sets as developed in ECCC-report, Annals-paper and [Ansotegui, Bonet, Levy, Manya, 2008], we obtain a natural generalisation UC_k, containing those clause-sets which are &#x201C;unit-refutation complete of level k&#x201D;, which is the same as having hardness at most k. Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop fundamental methods for the determination of hardness (the level k in UCk ). A fundamental insight now is that SLUR_k = UC_k holds for all k. We can thus exploit both streams of intuitions and methods for the investigations of these hierarchies.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>SOFSEM 2013: Theory and Practice of Computer Science. LCNS</journal><volume>7741</volume><journalNumber></journalNumber><paginationStart>220</paginationStart><paginationEnd>232</paginationEnd><publisher>Springer</publisher><placeOfPublication/><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>algorithms, satisfiability, polynomial time, knowledge compilation</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2013</publishedYear><publishedDate>2013-12-31</publishedDate><doi>10.1007/978-3-642-35843-2_20</doi><url>http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2012SOFSEM</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T14:56:09.1324491</lastEdited><Created>2012-12-17T22:40:14.2987438</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>Matthew</firstname><surname>Gwynne</surname><order>1</order></author><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T14:56:09.1324491 v2 13748 2012-12-17 Generalising and Unifying SLUR and Unit-Refutation Completeness 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2012-12-17 MACS The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). We introduce a hierarchy SLUR_k which we argue is the natural “limit” of such approaches. The second source for our investigations is the class UC of unit-refutation complete clause-sets introduced in [del Val 1994]. Via the theory of (tree-resolution based) “hardness” of clause-sets as developed in ECCC-report, Annals-paper and [Ansotegui, Bonet, Levy, Manya, 2008], we obtain a natural generalisation UC_k, containing those clause-sets which are “unit-refutation complete of level k”, which is the same as having hardness at most k. Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop fundamental methods for the determination of hardness (the level k in UCk ). A fundamental insight now is that SLUR_k = UC_k holds for all k. We can thus exploit both streams of intuitions and methods for the investigations of these hierarchies. Conference Paper/Proceeding/Abstract SOFSEM 2013: Theory and Practice of Computer Science. LCNS 7741 220 232 Springer 0302-9743 1611-3349 algorithms, satisfiability, polynomial time, knowledge compilation 31 12 2013 2013-12-31 10.1007/978-3-642-35843-2_20 http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2012SOFSEM COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2013-10-17T14:56:09.1324491 2012-12-17T22:40:14.2987438 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Matthew Gwynne 1 Oliver Kullmann 0000-0003-3021-0095 2
title Generalising and Unifying SLUR and Unit-Refutation Completeness
spellingShingle Generalising and Unifying SLUR and Unit-Refutation Completeness
Oliver Kullmann
title_short Generalising and Unifying SLUR and Unit-Refutation Completeness
title_full Generalising and Unifying SLUR and Unit-Refutation Completeness
title_fullStr Generalising and Unifying SLUR and Unit-Refutation Completeness
title_full_unstemmed Generalising and Unifying SLUR and Unit-Refutation Completeness
title_sort Generalising and Unifying SLUR and Unit-Refutation Completeness
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Matthew Gwynne
Oliver Kullmann
format Conference Paper/Proceeding/Abstract
container_title SOFSEM 2013: Theory and Practice of Computer Science. LCNS
container_volume 7741
container_start_page 220
publishDate 2013
institution Swansea University
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-642-35843-2_20
publisher Springer
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://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2012SOFSEM
document_store_str 0
active_str 0
description The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). We introduce a hierarchy SLUR_k which we argue is the natural “limit” of such approaches. The second source for our investigations is the class UC of unit-refutation complete clause-sets introduced in [del Val 1994]. Via the theory of (tree-resolution based) “hardness” of clause-sets as developed in ECCC-report, Annals-paper and [Ansotegui, Bonet, Levy, Manya, 2008], we obtain a natural generalisation UC_k, containing those clause-sets which are “unit-refutation complete of level k”, which is the same as having hardness at most k. Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop fundamental methods for the determination of hardness (the level k in UCk ). A fundamental insight now is that SLUR_k = UC_k holds for all k. We can thus exploit both streams of intuitions and methods for the investigations of these hierarchies.
published_date 2013-12-31T04:22:41Z
_version_ 1850821953421574144
score 11.08895

Similar Items