软件学报

作者：张昕荻，陈志翰，蔡少伟

单位：张昕荻，基础软件与系统重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学 计算机科学与技术学院, 北京 10004911,陈志翰，基础软件与系统重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学 计算机科学与技术学院, 北京 10004902,蔡少伟，基础软件与系统重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学 计算机科学与技术学院, 北京 10004903

关键词：可满足性问题;冷重启;信息遗忘

基金：中国科学院战略性先导科技专项 (前瞻战略科技先导专项) (XDA0320000, XDA0320300)

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

来源：2026年第4期

《软件学报》期刊编辑部

查看软件学报杂志2026年第4期