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

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

本文在 3 个代表性的 CDCL 求解器上实现了本文的冷重启技术. 3 个求解器分别为 CaDiCaL-watch-sat [27] 、
MapleLCMDistChronoBT-DL [28] 和 kissat-MAB [29] . 实验结果表明, 结合冷重启和热重启可以帮助改进 CDCL 求解
器, 甚至有时可以获得显著的提高. FO 和 FP 策略可以帮助同时改进 CDCL 求解器的可满足性求解能力和不可满
足性求解能力, 可使基础求解器分别整体多求解出 6.5 和 5.3 个实例. FC 策略主要可以改进 CDCL 求解器的可满
足性求解能力, 但会使不可满足性求解能力显著下降. 考虑了多种冷重启的复合策略在可满足实例上, 可平均多求
解 7.3 个实例, 且最优策略几乎均为 FO+FC. 通过对于遗忘子句 LBD 加以约束, 只遗忘 LBD 大于给定阈值的学习
子句, 我们发现, 当求解目标为提高可满足性实例的求解能力时, 我们应该将该阈值设置得尽可能小. 通过对 3 种
技术的组合测试, 本文发现 FO 有最优的综合提高能力.
进一步, 本文在具有最优性能的串行冷重启技术 FO 上, 实现了其并行版本, 并集成于两个代表性的并行求解
器 (P-mcomsps [30] 和 PaKis [31] ) 中, 实验表明并行 FO 技术可以帮助提高并行 CDCL 求解器的性能. 并行 FO 可以更
好地利用 CDCL 在不同搜索顺序下的运行时间差异. 为了更深入探索并行冷重启技术的提升潜力, 本文基于 kissat-
MAB 求解器和并行 FO 技术, 形成的并行求解器即可拥有令人吃惊的可满足性求解能力和加速比, 如 PaKis 求解
器可满足性实例的 PAR2 打分平均改进了 41.81%. 此外, 基于串行 FC 冷重启相关的分析, 本文设计了一种简单的
子句共享机制, 只在线程间共享 LBD≤2 的学习子句, 从而形成了一个可以在可满足性求解能力上超过主流求解
器的算法. 本文提出的并行冷重启方法, 相比于主流的多样性并行方法, 有更好的拓展性. 在 64 线程的环境以内,
该方法的加速比效率持续提升.
本文围绕 CDCL 算法的冷重启技术提出了如下 3 个研究问题 (RQ).
RQ1: 对主流的热重启 CDCL 求解器的启发式进行扰动, 其运行时间是否存在剧烈的扰动?
RQ2: 重启之后的搜索信息是否应该被保留?
RQ3: 是否可以借助冷重启的互补优势, 设计一套高效的并行求解器?
本文第 1 节介绍相关基础知识. 第 2 节对现存基于热重启的 CDCL 算法的重尾现象进行实证研究. 第 3 节基
于上述实验结论, 提出 3 种不同类型的冷重启技术, 并研究多种冷重启技术的混合冷重启技术以及特性. 第 4 节进
一步提出并行冷重启技术并研究相关的信息交互机制. 最后总结全文.
1 基础知识

本节给出了可满足性问题的基础知识.
1.1 可满足性问题与 CDCL 框架
给定一组由布尔变元组成的集合 V = {V 1 ,V 2 ,...,V n }, 其中每一个变元只能被赋值为真 ( ⊤) 或者假 ( ⊥). 变元 v
的正文字由变元本身表示 v, 负文字则由其否定表示 ¬v. 子句 (clause) 为文字的析取组成. 合取范式 (conjunctive
norm form, CNF) 由子句的合取组成. 可满足性问题 (SAT) 为判断给定的命题逻辑公式可满足性的判定问题. SAT
求解器是求解 SAT 问题的工具, 一般输入为 CNF 公式.
目前主流的 SAT 求解器均基于 CDCL 框架 [2] . CDCL 会迭代地执行布尔约束传播 (BCP) 推理, 并根据推理过
程中的冲突归结出新的学习子句用于剪枝和回退. 若冲突出现在原始子句则返回不可满足. 若 BCP 无法推出矛盾
则会进入分支组件, 选择一个未赋值变元并赋值, 然后再重复 BCP. 若推理无矛盾且所有变元均已赋值则返回可
满足. CDCL 是一个回溯算法, 学习子句可以用于剪枝搜索空间, 变元选择顺序和赋值倾向则影响算法的分支搜索
顺序. 三者对于 CDCL 算法的性能影响巨大 [1] .
1.2 可满足性问题求解技术
● 变元排序启发式. CDCL 的变元分支启发式会根据搜索历史信息, 优先选择近期最有可能产生冲突的未赋
值变元 [32] . SAT 求解器为每一个变元维护一个分数, 并采用堆或者优先队列进行排序 [26] . 变元的打分依据主要为
变元参与到冲突的频率和时间. 例如经典的 VSIDS 启发式 [15,33] 会优先选择经常参与最近高质量学习子句中的变
元, LRB 启发式 [14] 会优先选择赋值期间参与冲突分析比率 (学习率) 比较高的变元, VMTF 启发式 [34] 会贪心地选
择参与最近一次冲突的变元.