Reusing the Assignment Trail in CDCL Solvers
Peter van der Tak, Antonio Ramos, Marijn J. H. Heule · Journal on Satisfiability Boolean Modeling and Computation · 2011
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.