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

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

表 5 复合策略冷重启技术的最优配置及参数

实例集合 求解器 C SAT Δ SAT p (SAT) C UNS Δ UNS p (UNS) C ALL Δ ALL p (ALL)
Maple-DL +FO+FC +8 1E6 +FO+FP −1 4E5 +FP +5 8E5
SAT比赛2020年标准
CaDiCaLWS +FO+FC +12 8E5 +FO +3 1E6 +FP +9 3E5
测试实例集合 (400个实例)
kissat-MAB +FO+FC +10 4E5 +FO +1 8E5 +FO +9 8E5
Maple-DL +FO +5 1E6 +FO +3 1E6 +FO +8 1E6
SAT比赛2021年标准 CaDiCaLWS +FO+FC +6 1E6 +FO+FP +1 1E6 +FO +6 8E5
测试实例集合 (400个实例)
kissat-MAB +FO+FC +3 4E5 +FO +5 4E5 +FO +6 4E5

实验结果表明, 复合冷重启策略可平均使得求解器多求解 7.3 个可满足实例, 5 个不可满足实例, 整体多求解
7.17 个实例. 且根据 6 组样本的统计信息, FO+FC 最有希望提高可满足实例的求解效率 (5/6), FO 最有希望提高不
可满足实例的求解效率 (4/6) 和全部实例的求解效率 (4/6).
实验结果表明, 对于可满足和不可满足实例, 各自存在对应的最优配置, 总结如下.
观察 5. FO+FC 复合冷重启策略有最优的可满足实例求解能力; 单独的 FO 冷重启策略能达到最优的不可满
足实例求解和整体求解能力.
3.5 细分实例求解性能分析
根据之前的实验结果, FO 冷重启有最优的综合性能, 这使我们对其在细分实例集合上的表现产生了兴趣. 本
文将 SC20 和 SC21 上的实例按照来源做了详细的分类. 对于所有细分实例的实验结果可以于本文的 GitHub 仓库
获得. 在此, 本文对实验数据进行了总结, 其中#k 表示某组细分实例集中的实例个数.
(1) 冷重启更适用于“hypertree 分解” (#14), “滑动瓷砖拼图” (#13), 一些如“最小 super-permutation 问题” (#13)
等旅行商问题和一些染色问题. FO 可以帮助基求解器在这些家族中至少多求解出 2 个实例.
(2) 另一方面, FO 在“原像攻击密码学问题”(#11) 用例上表现较差, 会少求解 2 个实例.
(3) 对于一些类型的实例来说, FO 的引入会使得基求解器产生一定的互补性, 例如 kissat-MAB 和 kissat-MAB
+FO 在“电路乘法” (#13) 这组实例都可以求解 8 个实例, 但其中 4 个有求解能力的互补性. 这也启示我们, 利用不
同冷重启变元顺序之间显著的互补性, 有潜力据此设计一个更进一步的算法. 实际上, 本文后续章节利用了该特
点, 研究了并行冷重启方法.
4 并行冷重启技术

冷重启的引入有助于提升求解器的综合求解能力, 但是第 3.5 节中提到冷重启技术引入后, 求解器也会在某
些实例上产生互补性或者产生退化现象. 这是因为冷重启会增加求解器的探索性, 但并不能保证重启之后进入的
新搜索空间有更好的搜索性质. 例如, 冷重启可能会中断一些求解器时间占据较长的分支, 这些分支虽然难以找到
可行解, 但实际上该分支已经是所有分支中距离真正解比较近的一个分支.
由于探索新分支所带来的风险性, 串行冷重启技术无法消除运行时间的变化. 实验表明, kissat-MAB+FO 的
CV 值与 kissat-MAB 的 CV 仅有 5.57% 的差距. 此外, 重尾现象也是 CNF 求解时间难以预测的重要因素, 该问题
已困扰 SAT 领域数十年. 既然难以克服, 则可从另一角度考虑, 利用运行时差异来帮助更高效的求解.
除了混合冷热重启之外, 另外一种方法为, 利用不同参数下冷重启的互补优势来设计一个并行冷重启策略. 本
节选择综合性能最好的 FO 冷重启技术作为研究案例, 介绍了并行冷重启技术, 并用于改进主流的求解器性能. 此
外, FC 冷重启的并行版本本质上等同于子句共享, 本节也对相关技术展开了分析.
RQ3: 是否可以借助冷重启的互补优势, 设计一套高效的并行求解器?
本节主要探讨以上的研究问题, 并给出了一项观察结论.
按照搜索信息对于 CDCL 的作用, 我们可以将第 3 节的冷重启技术分为两类. 第 1 类是可以为搜索引入多样
性的 FO 和 FP 冷重启技术, 另一类是负责搜索空间剪枝的 FC 冷重启技术. 本节分别对两类技术展开了其并行版
本的讨论.