You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Reusing the Assignment Trail in CDCL Solvers


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.