Peter van der Tak, Marijn Heule, Armin Biere,
, in Department of Computer Science Series of Publications B: Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions, Vol. B-2012-2, University of Helsinki, Helsinki, Seite(n) 15-16, 2012
Sprache des Titels:
Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions
The concurrent cube-and-conquer (CCC) solver implements
the ideas in the paper we submitted to the PoS 2012 workshop
. 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 , 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.