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

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

首先, 第 4.1 节从 FO、FP 以及 FO+FP 的并行拓展版本中, 我们选择 FO 作为代表, 设计了并行 FO 冷重启技
术展开讨论. 并行 FO 冷重启技术的实现方法与串行 FO 冷重启的技术实现类似, 区别在于, 并行 FO 在不同线程
上使用了不同的随机种子. 该技术可以视为多样性并行求解器中的一种多样性引入策略.
并行 FO 冷重启技术的实现: 对于 n 线程的并行 SAT 求解器, 每一个线程的随机种子依次设置为 0, 1,…, n–1,
并同时执行串行 FO 技术. 若其中任一线程完成求解, 则并行算法立刻停止其他线程的求解并返回该求解结果.
借助类似的方法, 我们可以简单地实现并行 FP 冷重启和并行 FO+FP 复合冷重启技术. 本文选择单独展开对
FO 技术讨论的原因有两个. 一方面 FO 拥有最佳的串行冷重启综合性; 另一方面, 拓展实验表明, 通过 3 种技术均
可以得到同样的实验结论, 且并行 FP 和并行 FO+FP 的实验效果没有并行 FO 的实验提升明显.
然后, 从本质上讲, 将完全 FC 冷重启技术并行化, 类似于线程间不共享学习子句, 即无子句共享技术, 于是,
本文的第 4.2 节根据串行的实验结果展开了并行子句共享的讨论.
4.1 并行 FO 实验评估与加速比分析

本文在 PaKis [31] 和 P-mcomsps [30] 两个具有代表性的并行 SAT 求解器上, 实现了并行 FO 冷重启技术, 形成了
PaKis+FO(p) 和 P-mcomsps+FO(p) 两个包含并行 FO 技术的并行求解器. 本文用尾缀 (p) 表示该求解器为并行求
解器, 默认在 32 线程下运行. 为了保证对比的公平性, 本文也将 PaKis 的基础求解器由 kissat-sc20 [26] 替换为性能更
好的 kissat-MAB [29] , 实验表明, 两个版本的性能相当.
表 6 给出了相关的实验结果, 其中 PaKis+FO(p) 和 P-mcomsps+FO(p) 的冷重启参数分别设置为 6E5 和 4E5.
实验结果表明, 并行 FO 技术可以帮助并行算法提高综合求解能力, 并显著提升了可满足性实例的求解性能. 具体
地, 在可满足实例集合上, P-mcomsps+FO(p) 的 PAR2 相比 P-mcomsps(p) 的打分改进了 13.7%; PaKis+FO(p) 的
PAR2 打分相较于 PaKis(p) 的打分改进了 41.81%.

表 6 并行 FO 冷重启策略在两个主流并行 SAT 求解器上的实验结果

实例集合 求解器 #SAT PAR2 (SAT) #UNS PAR2 (UNS) #ALL PAR2 (ALL)
P-mcomsps(p) 158 2 169.01 140 843.34 298 2 872.74
SAT比赛2020年标准 P-mcomsps+FO(p) 160 (+2) 2 112.08 141 (+1) 813.09 301 (+3) 2 834.36
测试实例集合 (400个实例) PaKis(p) 176 1 005.26 130 1 801.21 306 2 671.46
PaKis+FO(p) 181 (+5) 800.08 130 1 776.44 311 (+5) 2 564.32
P-mcomsps(p) 143 1 332.89 179 725.23 322 2 220.39
SAT比赛2021年标准 P-mcomsps+FO(p) 149 (+6) 1 002.65 178 (–1) 778.81 327 (+5) 2 113.21
测试实例集合 (400个实例) PaKis(p) 155 472.05 164 1 705.67 319 2 331.96
PaKis+FO(p) 158 (+3) 173.68 166 (+2) 1 678.34 324 (+5) 2 249.03

加速比是衡量一个并行技术最常见的指标. 为了更好地测试 FO 的性能, 排除其他原因的影响, 本文基于 kissat-
MAB 和并行 FO 技术实现了一个多样性并行求解器, 记作 kissat-MAB+FO(p). 本文计算了该求解器在 SC20 实例
集合上, 不同核心数目 t ( ) 下, 求解器可满足实例, 不可满足实例以及全部实例的求解数量, 以及对应的 PAR2 打分
和平均加速比.
表 7 中给出了 kissat-MAB+FO(p) 的不同版本在 1–64 线程下的求解情况. 从表 7 中数据可知, 仅利用并行
FO 技术带来的多样性, 即可获得一个不错的可满足实例求解能力, 相比之下, 不可满足实例的求解能力提升不明
显. 基于并行 FO 技术的求解器求解结果更加稳定. 本文选用了 SC21 实例集 (包含 400 个数据), 使用 32 线程的
kissat-MAB+FO(p), 以不同时间种子运行 5 次, PAR2 均值的最高最低分差距为 1.6%, 求解个数差距最多为 2.
从表 7 中数据可知, 该技术的并行拓展性较强, 随着核心数量的增多, 实例求解数量和加速比不断提高, PAR2
打分不断降低. 仅依赖 FO(p) 技术, 64 线程版本相比单核心版本, 求解数量整体提升 13.2%, PAR2 打分改进 27%,
平均加速比达到 16.0 倍; 若考虑简单子句共享技术 (第 4.2 节详细讨论), 64 线程版本相比单核心版本, 求解数量
整体提升 18.4%, PAR2 打分改进 40.8%, 加速比达 24.8 倍.
并行 FO 与其他多样性生成方法的对比讨论: 正如前文介绍, 并行冷重启技术可以在客观上被看作一种基于
多样性的并行方法. 前人的多样性生成方法主要是采用互补的不同求解器或者同一求解器的不同互补性参数配