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

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

● 变元赋值倾向启发式. CDCL 的赋值倾向被称为一个变元的相位 (phase). 最常用的技术为相位存储 (phase
saving) 技术 [35] , 即将变元赋值为最近一次的赋值, 若该变元从未赋值, 则赋值为默认值. 近期的 SAT 求解器进一
步集成了相位重置 (rephase) 技术 [18,26] , 会定期将变元的相位重置为较深搜索分支下的部分赋值 (靶相位) [36] , 局部
搜索的高一致性赋值 [18] 等.
● 学习子句管理技术. CDCL 的学习子句会帮助剪枝搜索空间, 但是过多的子句会给推理查询带来负担. 目前
主流的 SAT 求解器会定期地删除掉一部分质量差的学习子句. 代表性的技术有 Oh 等人 [16] 提出的 3 层子句管理
技术. 该技术根据子句的 LBD 将学习子句分为 3 组, 第 1 组高质量子句不会被清除, 第 3 组质量差的学习子句会
被定期减半, 中间一组的学习子句会根据使用频率决定是否需要移动到其他两组.
● 重启技术. 最顶级的 CDCL 求解器实现了多种重启技术, 并会在求解过程中定期在高频重启和低频重启之
间切换, 但是即便是低频重启, 频率有时也可以达到每秒钟数百次. 重启时, 为了保证算法的完备性, 求解器只会清
空变元赋值, 并保留所有学习子句, 变元序和赋值倾向. 为了提高重启的效率, 一些重启后赋同样值的变元不会清
空赋值. 以上所有的技术均会使得重启前后的搜索空间高度相似, 不利于空间的探索. 本文称主流的重启技术为
“热重启”, 代表技术有 Luby 重启 [13] , Glucose-style 重启 [11] 及其 EMA 的改进版本 [10] .
● 并行求解技术. 顶尖的并行 SAT 求解算法可以分为分治法和多样性算法. 分治法的代表技术为 cube-and-
conquer 技术 [37] , 它会使用前瞻求解器把原始问题拆分为众多子问题并在不同的线程上分别求解这些子问题. 应用
该技术取得了多个数学问题上的突破 [38,39] , 但是该技术存在严重的负载不均衡问题, 且在国际 SAT 比赛上的表现
显著弱于基于多样性的方法. 另一方面, 基于多样性的方法 [23,30,31,40] 会在不同线程上采用不同的求解器或者参数,
共同求解同一个问题. 该方法利用了不同技术间的互补性, 并在线程间共享部分高质量的学习子句. 历年 SAT 比
赛并行组的冠军多为基于该技术研制的求解器. 但是, 多样性方法的求解能力受最优参数限制, 且由于优质参数数
量有限且需要提前对参数间互补性进行调研, 故其大规模拓展能力受限.
1.3 实验环境设置
本文所有的实验均在一台高性能的服务器上运行, 该服务器包含 2 块 AMD EPYC 7763 中央处理器, 主频为
2.45 GHz, 总计 128 个实际物理核心. 机器的内存为 1 TB, 操作系统为 Ubuntu 20.04 LTS (64 bit).
实验数据集合为 2020 年与 2021 年国际 SAT 竞赛的标准测试实例集合, 分别简称为 SC20 和 SC21. 每组数据
集包含 400 个来自工业和学术背景的实际问题. 求解器的运行设置与国际 SAT 比赛保持一致, 即每个串行求解器
或并行求解器的线程独占一个 CPU 物理核心, 每一个实例的运行截止时间为 5 000 s.
对于每一个求解器, 本文汇报其在某一实例集合下的可满足实例求解数目 (#SAT), 不可满足实例求解数目
(#UNS) 和全部求解数目 (#ALL = #SAT + #UNS). 求解器的打分采用平均 PAR2 打分机制, 即求解器求解所有实
例的平均求解时间, 其中超时实例的求解时间算作截止时间的 2 倍. 在同一组实例集合下, 平均 PAR2 打分越小,
求解器性能越好. 由于官方没有提供具体可满足实例和不可满足实例, 本文汇总了本文以及 SAT 比赛上所有求解
器的求解结果, 形成了对应的子实例集合, 用于分别计算可满足和不可满足实例的 PAR2 打分.
给定一个测试实例, 若一个并行求解器使用 t 线程求解的运行时间为 T t , 其加速比为 T 1 /T t . 本文在统计一组
t 线程均可以求解的实例, 并去除了两者可以在 1 s 内求解的实例, 这
实例上的平均加速比时, 只考虑了单线程和
种过于简单的实例会由于操作系统调度开销导致加速比统计出现特别明显的误差. 另外, 为了考虑未求解实例, 本
文也汇报了不同线程下求解器的 PAR2, 作为性能改进的参考.
本文的代码和所有实验结果开源于 GitHub 仓库 (https://github.com/shaowei-cai-group/cold-restart).
本文选取了 3 个系列的代表求解器作为基准串行求解器.
● MapleLCMDistChronoBT-DL V3.0 (简记为 Maple-DL) [28] : 该求解器是 Maple 系列求解器的一个改进版本,
该系列求解器由不同团队开发. 自从首个以 Maple 冠名的求解器 MapleCOMSPS 提出以来, 该系列求解器在国际
SAT 竞赛中取得冠军 4 次. Maple-DL 为该系列在 SAT 比赛中夺冠的最新版本.
● CaDiCaL-watch-sat (简记为 CaDiCaLWS) [27] : 该求解器基于 CaDiCaL 系列求解器开发, 拥有更好的性能. 获
得了 2021 年和 2022 年 SAT 比赛 CaDiCaL Hack 的冠军.