Revisiting Restarts of CDCL: Should the Search Information be Preserved?

TL;DR

This paper investigates the impact of preserving or forgetting learned information during restarts in CDCL SAT solvers, proposing a new cold restart strategy that improves performance, especially on satisfiable instances.

Contribution

It introduces the concept of cold restart, demonstrating its benefits over warm restart, and develops a parallel SAT solver utilizing this strategy.

Findings

Cold restart strategies improve solver performance on satisfiable instances.

Forgetting some learned information periodically helps avoid being stuck in disadvantageous search spaces.

Parallel solvers with cold restart outperform traditional methods on certain benchmarks.

Abstract

SAT solvers are indispensable in formal verification for hardware and software with many important applications. CDCL is the most widely used framework for modern SAT solvers, and restart is an essential technique of CDCL. When restarting, CDCL solvers cancel the current variable assignment while maintaining the branching order, variable phases, and learnt clauses. This type of restart is referred to as warm restart in this paper. Although different restart policies have been studied, there is no study on whether such information should be kept after restarts. This work addresses this question and finds some interesting observations. This paper indicates that under this popular warm restart scheme, there is a substantial variation in run-time with different randomized initial orders and phases, which motivates us to forget some learned information periodically to prevent being stuck in a disadvantageous search space. We propose a new type of restart called cold restart, which differs from previous restarts by forgetting some of the learned information. Experiments show that modern CDCL solvers can benefit from periodically conducting cold restarts. Based on the analysis of the cold-restart strategies, we develop a parallel SAT solver. Both the sequential and parallel versions of cold restart are more suitable for satisfiable instances, which suggests that existing CDCL heuristics for information management should be revised if one hopes to construct a satisfiable-oriented SAT solver.