Page 193 - 《软件学报》2026年第4期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2026,37(4):1634−1649 [doi: 10.13328/j.cnki.jos.007509] [CSTR: 32375.14.jos.007509] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
CDCL 算法的冷重启技术

张昕荻 1,2 , 陈志翰 1,2 , 蔡少伟 1,2

(基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190)
1
2
(中国科学院大学 计算机科学与技术学院, 北京 100049)
通信作者: 蔡少伟, E-mail: caisw@ios.ac.cn

摘 要: SAT 求解的 CDCL 算法被广泛应用于软硬件验证领域, 重启策略是其中的核心组件之一. 目前, 主流的
CDCL 求解器采用了“热重启”技术, 保留了变元序、赋值倾向、学习子句等主要搜索信息, 且重启频率极高. 热重
启技术会使 CDCL 重启之后更倾向于搜索重启前的搜索空间, 有可能会长期陷于一个不利的局部区域, 缺乏探索
性. 首先对现有的 CDCL 算法进行测试, 证实了在不同的初始搜索设置下, 主流 CDCL 求解器的求解时间有巨大的
扰动. 为了利用上述观察, 提出一种遗忘搜索信息的“冷重启”技术, 即阶段性的遗忘变元序、赋值倾向、学习子句,
实验证明了该技术可以有效地提高主流 CDCL 算法的性能. 同时, 也进一步拓展了其并行版本, 每个线程探索不同
的区域, 提高了并行算法的性能. 此外, 冷重启技术主要改进了串并行求解器可满足实例的求解能力, 为设计可满
足导向的 SAT 求解器提供了新的改进思路. 通过引入并行冷重启技术, PaKis 求解器可满足性实例的 PAR2 打分
平均改进 41.81%. 基于相关技术设计的并行 SAT 求解器 ParKissat-RS 以领先亚军 24% 的大幅领先优势取得国内
首个国际 SAT 竞赛并行组冠军.
关键词: 可满足性问题; 冷重启; 信息遗忘
中图法分类号: TP301

中文引用格式: 张昕荻, 陈志翰, 蔡少伟. CDCL算法的冷重启技术. 软件学报, 2026, 37(4): 1634–1649. http://www.jos.org.cn/1000-
9825/7509.htm
英文引用格式: Zhang XD, Chen ZH, Cai SW. Cold Restart Technique for CDCL Algorithms. Ruan Jian Xue Bao/Journal of Software,
2026, 37(4): 1634–1649 (in Chinese). http://www.jos.org.cn/1000-9825/7509.htm

Cold Restart Technique for CDCL Algorithms

1,2
1,2
ZHANG Xin-Di , CHEN Zhi-Han , CAI Shao-Wei 1,2
1
(Key Laboratory of Systems Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China)
2
(School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 100049, China)
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

* 基金项目: 中国科学院战略性先导科技专项 (前瞻战略科技先导专项) (XDA0320000, XDA0320300)
收稿时间: 2024-09-12; 修改时间: 2025-05-28; 采用时间: 2025-08-12; jos 在线出版时间: 2025-09-02
CNKI 网络首发时间: 2025-11-27