Downloads provided by UsageCounts
doi: 10.3233/sat190082
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.
restart strategy, CDCL solver
restart strategy, CDCL solver
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 3 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 10 | |
| downloads | 2 |

Views provided by UsageCounts
Downloads provided by UsageCounts