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

1638 软件学报 2026 年第 37 卷第 4 期

● kissat-MAB [29] : 最近几年的 SAT 比赛冠军多基于 kissat 求解器 [26] 进行开发, 本文选择的求解器为 2021 年
SAT 比赛的冠军求解器, 基于该技术的求解器在后面几年的竞赛中也被证明有高效的性能及稳定性.
本文选取了两个具有代表性的并行求解器作为基准并行求解器. 由于本文提及的技术被集成于 2022 年之后的
所有 SAT 比赛的冠军求解器之中, 因此, 本文没有选择 ParKissat-RS 系列求解器 [41] 或其改进版本作为基准求解器.
● PaKis [31] : 该求解器是第 1 个基于 kissat 研制的并行求解器. 它基于多样性技术研制, 其目标是探索具有最优
可满足实例求解能力的互补参数.
● P-mcomsps [30] : PaInleSS 系列并行求解器曾经取得国际 SAT 比赛并行组的 4 次冠军, 代表了目前综合性能
顶级的并行 SAT 求解器. 本文选取的 SAT 求解器为 2021 年夺冠的版本. 该求解器也是基于多样性并行技术.

2 热重启 CDCL 求解器运行时间的差异性

早期学者对 SAT 等组合优化问题开展研究时, 发现基于 DPLL 框架 (CDCL 的前身) 的回溯搜索算法存在一
种很有意思的现象: 求解器的性能会随着部分启发式的轻微扰动, 求解时间发生巨大的变化, 并发现运行时间的分
布满足重尾分布. 为了解决该问题, 2000 年左右, Gomes 等人 [20−22] 提出对 DPLL 求解器定期完全重启, 并在分支顺
序上引入一定的扰动, 来消除该现象并提高求解器的运行效率.
随后, 为了不浪费之前的搜索过程, 学者们提出了各式各样的重启算法, 并默认保留所有的搜索信息. 其中主
要保存的信息有变元序, 赋值倾向和学习子句. 我们称这类重启技术为“热重启”. 例如 2003 年研制的著名 CDCL
求解器 MiniSat 会在重启后保留上述信息 [15] .
随着热重启技术普及, CDCL 求解器的重启频率日益提高, 并衍生了很多加速重启的技术. 相关技术虽然提高
了 CDCL 求解器的求解性能, 但是代价是会使得求解器对启发式特别敏感, 例如对变元排序和赋值倾向等启发式.
由于其变元搜索顺序和赋值倾向均无变化, 故集成了热重启技术的 CDCL 求解器在重启之后更倾向于进入重启
前的搜索空间.
因此, 本节将深入探索以下问题.
RQ1: 对主流的热重启 CDCL 求解器的启发式进行扰动, 其运行时间是否存在剧烈的扰动?
如果 RQ1 成立, 则可以借助该现象, 引入彻底重启技术, 通过增加探索性, 来改进求解器的性能.
2.1 不同初始搜索顺序下的运行时间差异
变元搜索顺序是 CDCL 的核心启发式之一. 为了研究变元序对于运行时间的影响, 本文选择了 kissat-MAB [29]

作为研究对象. 默认情况下, kissat-MAB 会按照内部变元标号顺序作为初始变元搜索顺序. 另外, 本文从 SC20 标
准测试实例集合中, 选择出 kissat-MAB 可以在 5 000 s (同 SAT 比赛标准一致) 内求解的实例, 作为测试数据集. 其
中, 本文称某实例在 kissat-MAB 默认配置下的求解时间为 T baseline .
对于选中的每一个实例, 我们均随机生成了 100 组变元的随机序列 {o 1 ,o 2 ,...,o 100 }, 并作为 kissat-MAB 的初始
T sample (o i ) 非超时的
变元顺序. 然后, 本文统计了在所有采样的变元序 o i 下的运行时间, 记作 T sample (o i ). 然后, 对于
序列 o i , 本文计算了改变初始搜索顺序后, 运行时间的加速比 T baseline /T sample (o i ), 该指标可以用于衡量 kissat-MAB
运行时间的扰动情况. 该值大于 1 表示有加速, 小于 1 表示有性能衰退.
图 1 给出了 kissat-MAB 在求解所选实例时, 100 个采样顺序的加速比. 图中每一列代表一个实例, 并按照
T baseline 的大小进行排列. 图上的点表示某实例对应的加速比. 为了增加图片的可读性, 图中省略了 10 min 以内可
以求解的简单实例的求解情况, 并将纵坐标的加速比数值以对数刻度呈现. 图 1(a) 和 (b) 分别展示了可满足实例
和不可满足实例的求解情况.
根据图 1 的数据可以得到以下结论.
对于可满足性实例, CDCL 求解器的运行时间对于初始变元序的变化十分敏感. 在随机采样的变元序的帮助
下, 33% 的可满足实例的运行时间, 出现了 32 倍以上的加速. 此外, 通过随机采样的变元初始序, kissat-MAB 可以
求解 33 个在默认变元序下无法求解的可满足实例.