Between restarts and backjumps

Abstract

This paper introduces a novel technique that significantly reduces the computational costs to perform a restart in conflict-driven clause learning (CDCL) solvers. Our technique exploits the observation that CDCL solvers make many redundant propagations after a restart. It efficiently predicts which decisions will be made after a restart. This prediction is used to backtrack to the first level at which heuristics may select a new decision rather than performing a complete restart. In general, the number of conflicts that are encountered while solving a problem can be reduced by increasing the restart frequency, even though the solving time may increase. Our technique counters the latter effect. As a consequence CDCL solvers will favor more frequent restarts. © 2011 Springer-Verlag.