Cube-and-Conquer for Satisfiability

Satisfiability (SAT) is considered to be 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 the scalability of SAT solvers. In this chapter, we present the cube-and-conquer paradigm which addresses this issue and targets 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. We demonstrate the strength of cube-and-conquer on the Boolean Pythagorean Triples problem, a recently solved challenge from Ramsey Theory. Cube-and-conquer achieves linear-time speedups on this problem even when using thousands of cores. Moreover, we show how to compute a proof for such a hard problem when solving it using cube-and-conquer.