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

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

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.
Key words: satisfiability problem (SAT); cold restart; information forgetting

命题逻辑可满足性问题 (satisfiability problem, SAT) 是判断给定的命题逻辑公式可满足性的判定问题. 作为
第 1 个被证明的 NP-完全问题, SAT 是计算机科学和数理逻辑的基础问题, 其重要性也被包括 Knuth 在内的多位
图灵奖得主高度评价 [1] . 冲突驱动的子句学习技术 (conflict-driven clause learning, CDCL) 是目前求解 SAT 问题的
最主要方法, 它是一种深度优先的系统搜索算法, 并因拓展了非时序回溯和子句学习两种剪枝技术而得名 [2] .
CDCL 在大量的学术 [3] 和工业问题中得到应用, 如电子设计自动化领域 [4] 、软硬件测试 [5,6] 、模型检查 [7] 、密码分
析 [8] 、智能调度 [9] 等.
CDCL 维护了一棵二叉搜索树, 树上每一个节点会引出最多两个边, 代表对某一个布尔变元赋值为“真”或者
“假”, 树上从根节点出发的任一路径代表着一组变元赋值, 一般当前访问的分支所代表的部分赋值会被存放于一
个栈中 [1] . 伴随着重启 [10−13] 、赋值启发式 [14,15] 、子句管理 [16] 、化简 [17] 、混合求解 [18] 等技术的不断进步, CDCL 求
解器的性能相比早期版本, 得到了大幅改进 [19] .
重启策略是 CDCL 的核心组件之一, 对于 SAT 求解器的高效性贡献巨大. 1997 年, Gomes 等人 [20,21] 发现一些
系统性的回溯算法, 在求解一些随机可满足实例时, 对搜索顺序引入一定的随机性, 会使求解时间发生巨大的扰
动, 呈现出一种有趣的重尾分布现象. 因此, 重启技术被引入于系统搜索算法来防止求解器长时间陷入一个没有解
的搜索空间 [22] . 后来, 重启技术也被证明可以用来提升不可满足实例的求解能力, 相关的解释有两种: 一方面, 重
启可以被用来压缩赋值栈的大小, 以改进决策变元的顺序 [23] ; 另一方面, 有证据表明重启可以帮助求解器得到质
量更高的学习子句 [24] .
目前 CDCL 的重启策略聚焦于判断何时中断当前的搜索, 然后清空当前赋值后重新搜索 [10] . 为此, 学者们提
出了大量的重启技术. 其中一个比较著名的重启策略叫作 Luby 重启, 它会根据一组固定间隔序列进行重启, 属于
静态重启算法 [13] . 此外, Luby 重启策略在一类特殊的 Las Vegas 随机算法上, 已经被证明是最优的重启策略 [25] . 另
一方面, 动态重启算法则会利用求解过程中的信息来判断重启时机. 例如, Glucose-style 重启策略统计了最近学习
子句的平均文字块距离 (literal block distance, LBD), 当其明显差于全局的平均 LBD 值时, 则选择重启 [11] . Biere 等
人 [10] 也基于该算法提出了一套基于指数加权平均 (EMA) 的重启策略. 目前主流的 CDCL 求解器通常实现了多种
重启策略, 并定期切换 [16,26] . 在主流的重启策略下, CDCL 求解器的重启颇为频繁——求解器有时会每秒重启数百次.
主流的重启技术可以被视作“热重启”, 因为它们只会在重启时撤销变元的赋值, 并保留搜索过程中的全部信
息. 其中主要包含: 分支启发式中变元的打分 (变元序)、相位启发式中变元的期望赋值 (赋值倾向) 和用于局部剪
枝的学习子句 (学习子句) 这 3 类重要的搜索信息.
一方面, 热重启的使用减少了之前计算开销的浪费, 但另一方面也会让 CDCL 在重启后快速回到重启前的搜
索区域, 有可能会使搜索陷入一个不利的搜索方向, 缺乏对于其他搜索空间的探索性. 因此, 本文对如何合理地遗
忘搜索信息来增加算法的探索性, 以进一步提升 CDCL 串并行算法的性能展开了讨论, 并给出了一系列有趣的结果.
首先, 本文通过实验表明, 虽然目前主流的 CDCL 算法执行了大量的重启, 但是在不同的搜索顺序下, 求解同
一实例的时间变化巨大. 该现象的存在提示我们要对当前的“热重启”技术进行补充, 合理地利用不同搜索顺序下
运行时间的差异性, 通过更加彻底的重启, 来增加算法的探索性, 以提升算法的整体求解能力.
因此, 本文对于“重启时是否需要遗忘掉一些搜索信息?”这一未探索的关键问题开展讨论, 提出“冷重启”的概
念, 并研究 3 种不同的冷重启技术及其变种版本. 其中, “冷重启”指的是在重启之后会遗忘掉搜索信息的重启策略.
第 1 种冷重启策略会在重启后重置变元的打分为随机值, 被称为遗忘变元序 (记为 FO (forgetting order)); 第 2 种
冷重启策略会在重启后重置变元的相位为随机相位, 被称为遗忘赋值倾向 (记为 FP (forgetting phase)); 第 3 种冷
重启会在重启之后遗忘所有子句数据库中学习子句, 被称为遗忘子句 (记为 FC (forgetting clause)).