No Cover Image

Conference Paper/Proceeding/Abstract 1376 views

Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method

Marijn J.H. Heule, Oliver Kullmann Orcid Logo

26th International Joint Conference on Artificial Intelligence (IJCAI 2017), Pages: 4864 - 4868

Swansea University Author: Oliver Kullmann Orcid Logo

Abstract

A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem by the authors, yielding the largest (but "clever") proof yet. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, integrating the...

Full description

Published in: 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)
ISBN: 978-0-9992411-0-3
Published: Melbourne, Australia International Joint Conference on Artificial Intelligence (IJCAI) 2017
Online Access: https://www.ijcai.org/proceedings/2017/0683.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa34731
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2017-09-18T13:01:37Z
last_indexed 2018-02-09T05:25:08Z
id cronfa34731
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2017-09-18T10:23:30.9410882</datestamp><bib-version>v2</bib-version><id>34731</id><entry>2017-07-24</entry><title>Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method</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>2017-07-24</date><deptcode>SCS</deptcode><abstract>A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem by the authors, yielding the largest (but "clever") proof yet. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, integrating the ``old'' and the ``new'' method of SAT solving.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>26th International Joint Conference on Artificial Intelligence (IJCAI 2017)</journal><paginationStart>4864</paginationStart><paginationEnd>4868</paginationEnd><publisher>International Joint Conference on Artificial Intelligence (IJCAI)</publisher><placeOfPublication>Melbourne, Australia</placeOfPublication><isbnElectronic>978-0-9992411-0-3</isbnElectronic><keywords>Satisfiability, cube-and-conquer, Pythagorean triples</keywords><publishedDay>19</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2017</publishedYear><publishedDate>2017-08-19</publishedDate><doi/><url>https://www.ijcai.org/proceedings/2017/0683.pdf</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2017-09-18T10:23:30.9410882</lastEdited><Created>2017-07-24T08:15:39.8440138</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>Marijn J.H.</firstname><surname>Heule</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 2017-09-18T10:23:30.9410882 v2 34731 2017-07-24 Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2017-07-24 SCS A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem by the authors, yielding the largest (but "clever") proof yet. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, integrating the ``old'' and the ``new'' method of SAT solving. Conference Paper/Proceeding/Abstract 26th International Joint Conference on Artificial Intelligence (IJCAI 2017) 4864 4868 International Joint Conference on Artificial Intelligence (IJCAI) Melbourne, Australia 978-0-9992411-0-3 Satisfiability, cube-and-conquer, Pythagorean triples 19 8 2017 2017-08-19 https://www.ijcai.org/proceedings/2017/0683.pdf COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2017-09-18T10:23:30.9410882 2017-07-24T08:15:39.8440138 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Marijn J.H. Heule 1 Oliver Kullmann 0000-0003-3021-0095 2
title Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method
spellingShingle Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method
Oliver Kullmann
title_short Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method
title_full Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method
title_fullStr Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method
title_full_unstemmed Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method
title_sort Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Marijn J.H. Heule
Oliver Kullmann
format Conference Paper/Proceeding/Abstract
container_title 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)
container_start_page 4864
publishDate 2017
institution Swansea University
isbn 978-0-9992411-0-3
publisher International Joint Conference on Artificial Intelligence (IJCAI)
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 https://www.ijcai.org/proceedings/2017/0683.pdf
document_store_str 0
active_str 0
description A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem by the authors, yielding the largest (but "clever") proof yet. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, integrating the ``old'' and the ``new'' method of SAT solving.
published_date 2017-08-19T03:43:06Z
_version_ 1763752003338502144
score 11.035634

Similar Items