Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads
Sprache des Titels:
Intl. Haifa Verification Conference (HVC'11)
Satisfiability (SAT) is considered as one of the most important
core technologies in formal verification and related areas. Even
though there is steady progress in improving practical SAT solving, there
are limits on scalability of SAT solvers. We address this issue and present
a new 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 competition benchmarks, our hybrid
approach outperforms both lookahead and conflict-driven solvers.
Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel.