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

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

从结果中可以得知, 定期执行 FO 冷重启可以提升求解器的求解性能, 尤其是对于可满足实例. 具体地, 通过
引入 FO, 3 个基求解器平均在 SC20 和 SC21 实例集合上, 求解数目分别平均提高 6.3 和 6.7 个实例. 对于可满足
实例, 上述数据分别为 5.7 和 4.0 个. 可满足实例的求解性能提升主要归功于不同初始搜索顺序下巨大的运行时间
扰动, 在求解时, 定期的切换搜索空间, 可以帮助求解器减少卡死在某不利的搜索空间的概率.
根据实验结果, 我们同样也发现 FO 的引入也有助于改进不可满足实例的求解能力, 这对于 kissat-MAB 求解
器尤为明显. 一个合理的解释为, CDCL 的 UNSAT 证明可以看作启发式寻找冲突归结路径的技术, 而冷重启可以
帮助 CDCL 找到一个更优的冲突归结路径 [23] .
观察 2. 遗忘变元序的冷重启技术可以帮助求解器同时提高可满足和不可满足实例的求解能力.
3.2 遗忘赋值倾向的冷重启技术 (FP)
变元赋值倾向和选择顺序都主要作用于算法的搜索方向. 本节的 FP 技术主要作用于相位保存 [35] 技术. 每次
FP 重启被执行时, 本文均会将 CDCL 变元的相位随机重置为 0 或 1.
本文采用了与第 3.1 节类似的实验设置, 实验结果也同样被汇报于表 2.
实验结果表明, FP 冷重启技术可以帮助 CDCL 提高综合求解能力. 借助 FP 冷重启, Maple-DL、CaDiCaLWS
和 kissat-MAB 平均在两组实例集合上, 各自平均多求解了 4.5、7.0 和 4.5 个实例. 同时, FP 的实验结果与 FO 的
实验结果整体上类似, 算法的综合性能改进主要归功于 FP 在可满足实例上的提高.
观察 3. 遗忘赋值倾向的冷重启技术可以帮助求解器大幅提高可满足实例的求解能力, 小幅度提高不可满足
实例的求解能力.
3.3 遗忘学习子句的冷重启技术 (FC)
与变元序和相位主要作用于搜索顺序上不同, 学习子句在 CDCL 求解器中主要的作用为帮助剪枝, 过多的学
习子句会影响求解器的推理速度.
本文设计了一种简单的学习子句遗忘策略. 我们选中的 CDCL 求解器均为学习子句维护了一个数据库, 并设
计了相关的管理算法. 每次执行 FC 冷重启时, 求解器会清空学习子句数据库中所有的学习子句.
实验结果同样被汇报于表 2 中, 从中可以得知, FC 冷重启总是会使得不可满足实例的求解性能衰退. 但是,
FC 冷重启技术有时可以帮助求解器提升可满足实例的求解性能. 事实上, FC 可以帮助本文选择的所有 3 个求解
器提高求解性能. 例如, 在 SC20 实例集合上, FC 冷重启可以帮助 Maple-DL 和 kissat-MAB 分别多求解 7 个实例.
这个结果让人十分吃惊. 主流的 CDCL 求解器维护了一个子句管理组件, 并会定期地删除一部分质量较差的学习
子句, 来减少推理负担. 本文有关于 FC 冷重启的实验表明, 定期删除全部子句数据库的学习子句对于可满足实例
有巨大的收益. 这从另一方面说明, 在设计一个可满足性问题导向的 CDCL 求解器时, 目前学习子句起到的作用
有待考虑, 且子句管理组件需要进一步的改进.
本文从两个方面对学习子句的作用进行了更深入的研究, 并尝试解释 FC 对于可满足性实例有效的原因.
3.3.1 FC 冷重启中学习子句的 LBD 阈值研究
为了更好地理解学习子句在 CDCL 中的作用, 本节为 FC 添加了一组补充实验, 以探究不同 LBD 质量的学习
子句对于求解效率的影响.
对于 FC 冷重启, 我们设置了一个遗忘学习子句的阈值 ρ, 并在冷重启时选择性地遗忘掉学习子句数据库中所
有 LBD > ρ 的学习子句. 在 3 层学习子句管理技术的工作中, Oh [16] 认为 LBD > 5 的学习子句在 CDCL 求解过程中
ρ 设置为 0, 1,…, 5, 并在冷重启时
被使用的概率和能起到的作用都极小. 因此, 我们沿用之前的经验, 分别将阈值
将高质量的学习子句保留下来. 其中, ρ = 0 表示的是默认版本的 FC.
本节选用 kissat-MAB [29] 作为基求解器, 并选用 SC20 与 SC21 实例集进行评估. 冷重启的参数 p 始终保持与默
认的 FC 版本一致, 即 p = 7×10 . 实验结果被汇总于表 3.
5
根据实验结果, 可以得到如下的结论.
(1) 遗忘更多的学习子句通常意味着更好的可满足实例求解能力和更差的不可满足实例的求解能力.