Reusing the Assignment Trail in CDCL Solvers

Abstract

We present the solver RestartSAT which includes a novel technique to reduce the cost to perform a restart in CDCL SAT solvers. This technique, called ReusedTrail, exploits the observation that CDCL solvers often reassign the same variables to the same truth values after a restart. It computes a partial restart level for which it is guaranteed that all variables below this level will be reassigned after a full restart. RestartSAT, an extended version of MiniSAT, incorporates ReusedTrail which can be implemented easily in almost any CDCL solver. On average, it saves over a third of the decisions and propagations necessary to solve a problem using a Luby restart policy with unit run 1. Experimental results show that RestartSAT solves over a dozen more application instances than the default MiniSAT.