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

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

置 [23,30,31,40] . 与之前的多样性方法类似, 并行 FO 技术也会通过在不同线程上沿不同的求解方向搜索, 据此产生具
有互补性的配置.

表 7 并行 FO 冷重启的加速比分析

平均加速比
kissat-MAB+FO(p)版本 t #SAT PAR2 (SAT) #UNS PAR2 (UNS) #ALL PAR2 (ALL)
SAT UNS ALL
1 151 2 510 121 2 558 272 3 670 1.0 1.0 1.0
2 161 1 986 123 2 440 284 3 376 4.2 1.13 2.8
4 168 1 477 123 2 404 291 3 120 12.5 1.16 7.5
kissat-MAB+FO(p) 8 176 1 190 125 2 317 301 2 951 10.0 1.18 6.1
16 177 1 024 124 2 320 301 2 872 15.0 1.22 8.9
32 182 766 125 2 209 307 2 707 26.8 1.32 15.5
64 183 667 125 2 231 308 2 668 27.5 1.35 16.0
1 151 2 510 121 2 558 272 3 670 1.0 1.0 1.0
2 162 1 958 126 2 159 288 3 259 3.5 1.3 2.5
4 167 1 618 127 1 984 294 3 032 7.5 1.9 5.0
kissat-MAB+FO(p)+子句共享
8 171 1 329 129 1 723 300 2 797 9.4 2.9 6.5
(LBD ⩽ 2)
16 178 924 133 1 436 311 2 498 17.0 4.6 11.5
32 180 770 131 1 493 311 2 445 22.1 6.6 15.4
64 184 583 133 1 354 317 2 304 29.0 9.4 20.5
1 151 2 510 121 2 558 272 3 670 1.0 1.0 1.0
2 163 1 859 128 1 987 291 3 148 2.6 1.6 2.2
4 167 1 603 130 1 785 297 2 951 5.8 2.2 4.2
kissat-MAB+FO(p)+子句共享
8 173 1 197 131 1 556 304 2 672 10.2 3.4 7.2
(LBD ⩽ 3)
16 178 911 134 1 316 312 2 447 20.7 5.2 13.9
32 177 948 135 1 169 312 2 410 20.0 8.0 14.7
64 182 662 140 891 322 2 171 35.5 11.0 24.8

(1) 并行 FO 多样性产生方法是一种轻量级, 易于实现, 且可以支持所有 CDCL 算法的策略. 相比之下, 基于参
数的多样性策略需要人工选择不同的互补参数, 且不同求解器的参数种类和数量都不同.
(2) 并行 FO 多样性策略的产生不会影响求解器的综合性能. 根据前人的观点, 随机扰乱测试实例会小幅扰动
求解器的性能, 但不会影响求解器的排名 [45] . 相比之下, 基于参数的方法, 有可能会使得部分求解器的性能变弱,
不利于求解.
(3) 并行 FO 有良好的拓展性和动态适应性. 基于该方法可以很快地将一个串行 CDCL 求解器拓展到任意核
心数目的并行求解器上. 当使用的核心数目场景发生变化时, 无需修改代码. 且基于本文方法的求解器, 加速比在
到达 64 核心时, 仍然在持续增高, 有进一步增长的潜力. 相比之下, 面对不同线程数, 之前的方法需要人工选择参
数并调参, 甚至会面临参数数量不足以分配给所有线程的情形.
4.2 并行 FO 的共享子句选择
目前, 基于多样性的并行 SAT 求解器通常采用子句共享技术在线程之间交互学习子句, 用于剪枝高维度搜索
空间, 以减少不同的线程重复搜索同一空间的概率. 此外, 在多个线程之间“共享学习到的子句”的思想类似于当前
热重启之间“保留高质量的学习子句”的想法. 即清空所有子句的 FC 技术的冷重启技术类似于不采用子句共享技
术; 保留质量在 LBD ⩽ ρ 学习子句的 FC 冷重启技术类似于线程间共享一部分 LBD ⩽ ρ 的学习子句.
这引起了我们对研究“FC 中学习子句的阈值规律是否也适用于并行子句共享”的兴趣.
根据表 3 的结果, LBD ⩽ 3 的学习子句具有最高的综合性能收益. 本文在 PaInleSS 框架 [30] 的帮助下, 分别在
kissat-MAB+FO(p) 的基础上, 实现了线程间简单的子句共享技术, 分别仅简单共享 LBD ⩽ 2 和 LBD ⩽ 3 学习子句
的子句.
子句共享技术的实现: 每一个线程均设置一个读入共享内存和一个输出共享内存. 每个线程会收集 LBD ⩽ ρ
的学习子句, 存储于该线程的输出共享内存. 每隔 0.75 s, 每个线程的输出共享内存会将收集到的学习子句分发给