Conference Paper/Proceeding/Abstract 1421 views
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads
,
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.
DOI (Published version): 10.1007/978-3-642-34188-5_8
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...
| 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: |
Faculty of Science and Engineering |
| Start Page: |
50 |
| End Page: |
65 |