No Cover Image

Conference Paper/Proceeding/Abstract 1130 views 233 downloads

Unified Characterisations of Resolution Hardness Measures

Olaf Beyersdorff, Oliver Kullmann Orcid Logo

Theory and Applications of Satisfiability Testing – SAT 2014, Volume: 8561

Swansea University Author: Oliver Kullmann Orcid Logo

DOI (Published version): 10.1007/978-3-319-09284-3_13

Abstract

Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measur...

Full description

Published in: Theory and Applications of Satisfiability Testing – SAT 2014
Published: International Conference on Theory and Applications of Satisfiability Testing: Springer 2014
Online Access: http://www.cs.swan.ac.uk/~csoliver/papers.html#HARD2014
URI: https://cronfa.swan.ac.uk/Record/cronfa18004
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2014-05-29T10:24:51Z
last_indexed 2019-06-05T09:41:41Z
id cronfa18004
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-06-04T14:12:46.1563429</datestamp><bib-version>v2</bib-version><id>18004</id><entry>2014-05-27</entry><title>Unified Characterisations of Resolution Hardness Measures</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>2014-05-27</date><deptcode>SCS</deptcode><abstract>Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size of resolution proofs. Our main contribution is a unified game-theoretic characterisation of these measures. As consequences we obtain new relations between the different hardness measures. In particular, we prove a generalised version of Atserias and Dalmau's result on the relation between resolution width and space.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Theory and Applications of Satisfiability Testing &#x2013; SAT 2014</journal><volume>8561</volume><paginationEnd>187</paginationEnd><publisher>International Conference on Theory and Applications of Satisfiability Testing: Springer</publisher><keywords>SAT, proof complexity, games, resolution calculus, hardness measures</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-12-31</publishedDate><doi>10.1007/978-3-319-09284-3_13</doi><url>http://www.cs.swan.ac.uk/~csoliver/papers.html#HARD2014</url><notes></notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-06-04T14:12:46.1563429</lastEdited><Created>2014-05-27T06:37:37.6160739</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>Olaf</firstname><surname>Beyersdorff</surname><order>1</order></author><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>2</order></author></authors><documents><document><filename>0018004-15052015115552.pdf</filename><originalFilename>85610170.pdf</originalFilename><uploaded>2015-05-15T11:55:52.7770000</uploaded><type>Output</type><contentLength>386297</contentLength><contentType>application/pdf</contentType><version>Author's Original</version><cronfaStatus>true</cronfaStatus><embargoDate>2015-05-15T00:00:00.0000000</embargoDate><documentNotes/><copyrightCorrect>true</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2019-06-04T14:12:46.1563429 v2 18004 2014-05-27 Unified Characterisations of Resolution Hardness Measures 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2014-05-27 SCS Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size of resolution proofs. Our main contribution is a unified game-theoretic characterisation of these measures. As consequences we obtain new relations between the different hardness measures. In particular, we prove a generalised version of Atserias and Dalmau's result on the relation between resolution width and space. Conference Paper/Proceeding/Abstract Theory and Applications of Satisfiability Testing – SAT 2014 8561 187 International Conference on Theory and Applications of Satisfiability Testing: Springer SAT, proof complexity, games, resolution calculus, hardness measures 31 12 2014 2014-12-31 10.1007/978-3-319-09284-3_13 http://www.cs.swan.ac.uk/~csoliver/papers.html#HARD2014 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2019-06-04T14:12:46.1563429 2014-05-27T06:37:37.6160739 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Olaf Beyersdorff 1 Oliver Kullmann 0000-0003-3021-0095 2 0018004-15052015115552.pdf 85610170.pdf 2015-05-15T11:55:52.7770000 Output 386297 application/pdf Author's Original true 2015-05-15T00:00:00.0000000 true
title Unified Characterisations of Resolution Hardness Measures
spellingShingle Unified Characterisations of Resolution Hardness Measures
Oliver Kullmann
title_short Unified Characterisations of Resolution Hardness Measures
title_full Unified Characterisations of Resolution Hardness Measures
title_fullStr Unified Characterisations of Resolution Hardness Measures
title_full_unstemmed Unified Characterisations of Resolution Hardness Measures
title_sort Unified Characterisations of Resolution Hardness Measures
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Olaf Beyersdorff
Oliver Kullmann
format Conference Paper/Proceeding/Abstract
container_title Theory and Applications of Satisfiability Testing – SAT 2014
container_volume 8561
publishDate 2014
institution Swansea University
doi_str_mv 10.1007/978-3-319-09284-3_13
publisher International Conference on Theory and Applications of Satisfiability Testing: 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#HARD2014
document_store_str 1
active_str 0
description Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size of resolution proofs. Our main contribution is a unified game-theoretic characterisation of these measures. As consequences we obtain new relations between the different hardness measures. In particular, we prove a generalised version of Atserias and Dalmau's result on the relation between resolution width and space.
published_date 2014-12-31T03:20:59Z
_version_ 1763750612475838464
score 11.035634

Similar Items