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!
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.
Keywords: Satisfiability, cube-and-conquer, Pythagorean triples
College: Faculty of Science and Engineering
Start Page: 4864
End Page: 4868