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信息管理启发式策略。