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.

翻译：SAT求解器在硬件与软件的形式化验证中不可或缺，具有众多重要应用。CDCL是现代SAT求解器最广泛使用的框架，而重启是CDCL的一项关键技术。重启时，CDCL求解器会取消当前变量赋值，同时保留分支顺序、变量相位及学习子句。本文将此类型重启称为热重启。尽管已有多种重启策略被研究，但重启后是否应保留此类信息尚未有研究涉及。本工作针对该问题展开探讨，并发现若干有趣现象。本文指出，在这种流行的热重启机制下，采用不同随机初始顺序与相位会导致运行时间存在显著差异，这促使我们考虑定期遗忘部分学习信息以避免陷入不利搜索空间。我们提出一种称为冷重启的新型重启机制，其与以往重启方式的区别在于会遗忘部分已学习信息。实验表明，现代CDCL求解器可通过定期执行冷重启获得性能提升。基于对冷重启策略的分析，我们开发了一款并行SAT求解器。冷重启的串行与并行版本均更适用于可满足实例，这表明若希望构建面向可满足性判定的SAT求解器，现有CDCL在信息管理方面的启发式策略需要重新审视。