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

张昕荻 等: CDCL 算法的冷重启技术 1647

其他线程的输入共享内存中, 并最多一次共享 1 500 个文字. 每次线程内部重启的时候, 算法会将输入共享内存中
的学习子句读入内部学习子句数据库和相关数据结构中.
表 7 汇总了不同核心下的求解性能和对应的加速比, 从中, 我们可以得到如下的实验结果.
(1) 学习子句在串行 FC 冷重启技术中与在并行子句共享中发挥的作用类似.
(2) 子句共享可以进一步提高不可满足实例的求解性能, 但是对于可满足实例几乎没有影响, 甚至在某些实例
上会产生阻碍.
(3) P-mcomsps 求解器中实现了一种动态阈值的学习子句共享技术, 会根据文字共享数量对阈值进行动态更
新 [30] . 根据实验结果, 我们发现该版本与 LBD ⩽ 2 的版本具有类似的性能, 并可以得到类似的结论.
整体来看, 基于并行 FO 和简单的子句共享策略足以开发一个以可满足性实例求解导向的高性能并行求解器.
基于本节的观察结论, 可以得到如下的观察, 并回答了 RQ3.
观察 6. FO 冷重启技术有助于帮助并行 SAT 求解器更高效、便捷地产生互补配置, 这显著地提升了可满足
实例的求解性能, 但是对于不可满足实例的改进较弱. 子句共享技术的引入显著地提高了不可满足实例的求解性
能, 但对于可满足实例求解性能的改进有限.
5 相关工作

Gomes 等人 [21,22] 最早发现了组合优化回溯算法运行时间的重尾分布现象, 并引入了随机性和重启技术.
1998 年, 他们为基于 DPLL 的 SAT 求解器引入了一定的随机性平均打破机制, 并引入了线性增长间隔的重启策
略. CDCL 求解器 Chaff [33] 提出了著名的 VSIDS 分治策略, 并为赋值决策过程添加了一定的瞬时随机性, 但是它会
在重启时维持当前的变元选择顺序. 与上述工作不同的是, 本文的冷重启策略会彻底将变元选择顺序洗牌.
[2]
自从 CDCL 算法提出以来, 学者们对 GRASP 等求解器展开了研究, 发现在重启之后记录学习子句可以减少
一定的运行时间 [43] . 这种做法迅速地成为 CDCL 求解器的标准配置, 尽管后续衍生了多种学习子句管理启发式,
但是据我们所知, 没有一个串行 CDCL 求解器会和本文的 FC 冷重启一样, 即在重启的过程中遗忘所有学习子句
数据库中的学习子句.
除此之外, 大部分有关于重启的技术主要聚焦于何时进行重启 [10−13,15,16,44] . 但是所有相关技术均为热重启技
术. 与本文最为相关的技术为目前流行的相位重置技术, 其中会以一部分概率将相位重置为随机值, 类似于本文
的 FP 冷重启技术. 然而, 本文系统地提出了 3 种冷重启技术及相关复合冷重启技术, 详细针对该问题展开了讨论,
并探讨了相关的并行冷重启拓展.
目前主流的并行 CDCL 求解器普遍利用不同的求解器或参数设计多样性引入技术 [23,30,31,40] . 本文提出的并行
FO 技术是一种更便捷高效的多样性引入技术. 事实上, 基于本文中相关技术研制的 SAT 并行求解器 ParKissat-
RS [41] , 拓展了预处理器技术, 参加了 SAT 比赛 2022 年并行主赛道, 并以领先第 2 名 24% 的大幅优势取得了冠军.
同时, 其改进版本 PRS [46] 蝉联了 2023 年并行赛道的冠军.

6 总 结

主流的 CDCL 求解器在重启时普遍保留了所有搜索信息的热重启技术, 这会使得重启之后更倾向于保持之
前的搜索方向. 本文通过实验探讨了该现象, 发现主流 CDCL 方法存在明显的运行时间的扰动. 本文提出定期执
行冷重启技术, 遗忘一部分搜索信息, 以通过增加算法的探索性来提高 CDCL 的求解效率. 本文冷重启的并行拓
展版本, 进一步利用互补性优势, 为并行 SAT 求解器提出了一种简洁、高拓展性的多样性引入机制. 此外, 详细的
实验证明了方法的有效性.
未来, 我们将尝试利用更加先进的技术来设计一套动态冷重启交互机制, 面向具体的实例, 研究更智能的冷重
启间隔预测方法. 该工作为定制化 CDCL 的发展提出了一个有趣的发展构想. 同时, 本文的方法可以被视为一种
特殊的求解器, 它以可满足性求解能力为导向. 并且我们也准备对 CDCL 求解器内部的其他组件进行重新审视,
以进一步提升其专用性.