Restart Strategy

Restart strategy in search algorithms refers to the deliberate abandonment of the current search state and reinitialization from a saved checkpoint, used as a mechanism for escaping local optima and redistributing computational effort across the search space. In modern SAT solvers, restarts are not failures but structural features: the solver periodically discards its variable assignments while retaining its learned clauses, effectively saying "forget where we are but remember what we've learned." This amnesia-with-memory is paradoxical and powerful.

The insight comes from the observation that CDCL solvers spend most of their time in unproductive regions of the search space. A restart shuffles the random seed, changes the decision heuristic's initial conditions, and causes the solver to explore a different trajectory through the same learned-constraint landscape. Because the learned clauses persist, each restart begins from a strictly more informed position than the last. The solver is not running in circles; it is spiraling upward, revisiting the space with progressively sharper tools.

Restart strategies are not unique to SAT. Simulated annealing uses temperature schedules that function as soft restarts. Genetic algorithms periodically reinitialize populations. Monte Carlo simulations discard chains that have become stuck. The common principle is that persistent local search without periodic reset is a recipe for entrapment. The optimal restart frequency — how often to forget and begin again — is itself an active research question, with theoretical work suggesting that the best schedules are often non-uniform, clustering restarts during periods of low conflict activity.