Abstract:The CDCL algorithm for SAT solving is widely used in the field of hardware and software verification, with restart being one of its core components. Currently, mainstream CDCL solvers often employ the "warm restart" technique, which retains key search information such as variable order, assignment preferences, and learnt clauses, and has a very high restart frequency. The warm restart technique tends to make CDCL solvers more inclined to visit the search space that was explored before restarts, which may lead to being trapped in an unfavorable local search space for a long time, lacking exploration for another regions. This paper first tests the existing CDCL algorithms and confirms that under different initial search settings, the runtime for an instance of mainstream CDCL solvers exhibits significant fluctuations. To leverage this observation, the paper proposes the "cold restart" technique that forgets search information, specifically by periodically forgetting variable order, assignment preferences, and learned clauses. Experimental results demonstrate that this technique can effectively improve mainstream CDCL algorithms. Additionally, the paper further extends its parallel version, where each thread explores different search spaces, enhancing the performance of the parallel algorithm. Moreover, the cold restart technique primarily improves the performance of sequential and parallel solvers for the solving ability on satisfiable instances, providing new insights for designing satisfiable-oriented solvers. Specifically, our parallel cold restart techniques can improve 41.84% of the PAR2 score of Pakis on satisfiable instances. The parallel SAT solvers named ParKissat-RS including the ideas in this paper won the parallel track of SAT competitions with a significantly margin of 24% faster.