Concurrent Cube-and-Conquer

The concurrent cube-and-conquer (CCC) solver implements the ideas in the paper we submitted to the PoS 2012 workshop [1]. This system description describes the main concepts, a more detailed explanation is in the paper. Recent work has introduced the cube-and-conquer (CC) technique [2], which first partitions the search space into disjunctive sets of assumptions (cubes) using a lookahead (LA) solver (the cube phase) and then solves each cube using a CDCL solver (the conquer phase). It uses a cutoff heuristic to control after what number of decisions the lookahead solver should be cut off and store its decision variables (its current cube) for the CDCL solver to solve in the conquer phase. However, this heuristic is not ideal particularly because no information about the performance of CDCL on the cubes is present in the cube phase. Concurrent cube-and-conquer uses a synchronized LA and CDCL solver concurrently in the cube phase to improve the cutoff heuristic.