No Cover Image

Conference Paper/Proceeding/Abstract 671 views

Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads / Marijn J. H Heule, Oliver Kullmann, Siert Wieringa, Armin Biere

Hardware and Software: Verification and Testing, Volume: 7261, Pages: 50 - 65

Swansea University Author: Oliver Kullmann

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

Abstract

We present a new SAT approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes t...

Full description

Published in: Hardware and Software: Verification and Testing
ISSN: 0302-9743 1611-3349
Published: Heidelberg Springer 2011
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa8073
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: We present a new SAT approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard SAT-competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelise, it is a competitive alternative for solving SAT problems in parallel. This approach was originally developed for solving hard van-der-Waerden problems, and for these (hard, unsatisfiable) problems the approach is not only very well parallelisable, but outperforms all other (parallel or not) SAT-solvers in terms of total run-time by at least a factor of two.
College: College of Science
Start Page: 50
End Page: 65