Cold Restart Technique for CDCL Algorithms
Author:
Affiliation:

Clc Number:

TP301

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    The CDCL algorithm for SAT solving is widely applied 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 is explored before restarts, which may lead to being trapped in an unfavorable local search space for a long time, lacking exploration of other regions. This study first tests the existing CDCL algorithms and confirms that under different initial search settings, the runtime for mainstream CDCL solvers exhibits significant fluctuations. To leverage this observation, the proposed “cold restart” technique forgets search information, specifically by periodically forgetting variable order, assignment preferences, and learnt clauses. Experimental results demonstrate that this technique can effectively improve mainstream CDCL algorithms. In addition, this study 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 on satisfiable instances, providing new insights for designing satisfiable-oriented solvers. Specifically, the proposed parallel cold restart technique improves the PAR2 score of PaKis on satisfiable instances by 41.81% on average. The parallel SAT solver named ParKissat-RS, which integrates the proposed ideas, wins the parallel track of the SAT competition with a significant margin of 24% over the runner-up.

    Reference
    Related
    Cited by
Get Citation

张昕荻,陈志翰,蔡少伟. CDCL算法的冷重启技术.软件学报,2026,37(4):1634-1649

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 12,2024
  • Revised:May 28,2025
  • Adopted:
  • Online: September 02,2025
  • Published: April 06,2026
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063