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

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

表 2 遗忘变元序、遗忘赋值倾向和遗忘学习子句的冷重启结果汇总 (续)

数据集合 求解器 种类 #SAT PAR2 (SAT) #UNS PAR2 (UNS) #ALL PAR2 (ALL) p
默认 126 2 667.20 144 2 999.09 270 3 811.46 －
+FO 132 (+6) 2 483.37 144 2 994.74 276 (+6) 3 735.90 8E5
CaDiCaLWS
+FP 132 (+6) 2 501.37 143 (−1) 3 049.62 275 (+5) 3 768.62 3E5
SAT比赛2021年 +FC 130 (+4) 2 557.67 138 (−6) 3 251.08 268 (−2) 3 884.82 6E5
数据集合 (400个实例) 默认 142 1 654.57 147 2 714.55 289 3 274.09 －
+FO 143 (+1) 1 624.87 152 (+5) 2 555.97 295 (+6) 3 188.47 4E5
kissat-MAB
+FP 142 1 655.81 150 (+3) 2 634.91 292 (+3) 3 237.56 1E6
+FC 143 (+1) 1 677.60 137 (−10) 3 339.01 280 (−9) 3 573.68 7E5

3 种单独的冷重启策略如下.
● FO 冷重启: 重启之后遗忘所有变元排序启发式中的变元打分.
● FP 冷重启: 重启之后遗忘所有相位保留启发式的存储内容.
● FC 冷重启: 重启之后遗忘所有子句管理数据库中的学习子句.
本文在实现的过程中, 并没有直接将热重启全部替换为冷重启. 预实验表明, 在如此高的重启频率下, 完全采
用冷重启技术会使得求解器的性能大幅衰退. 因此, 本文选择在保留主流求解器中高频热重启的前提下, 混合低频
冷重启技术以增加算法的探索性.
事实上, 冷热重启的结合技术与搜索算法中的一个热门话题在本质上有一定联系: 如何处理好算法利用
(exploitation) 和探索 (exploration) 两者间的均衡. 其中热重启与利用相关, 冷重启与探索相关.
本文旨在以最简单的形式将冷重启技术插入在热重启算法中, 因此我们在设计混合策略时, 主要考虑如何设
置一个合理的冷重启间隔.
冷重启间隔设置: 本文选用了一种常见的线性递增间隔, 属于静态重启间隔的范畴. 令 r 表示算法自从上一次
冷重启到现在遇到的所有冲突次数, n 为算法累计执行的冷重启次数. 则当 r ⩾ p×n 时, 算法就会执行一次冷重启.

其中 p 是唯一需要调节的参数.
本文选择冲突次数作为标准, 是因为 CDCL 求解器普遍使用冲突作为一种运行时间刻度的单位, 且热重启也
同样采用该标准. 在统一标准下, 求解器执行冷重启的次数正相关于热重启的执行次数. 在本文的设置下, 一般求
解器执行冷重启的次数不会超过 10 次, 例如 kissat-MAB+FO 执行冷重启的次数最多为 3 次; 相比之下, 热重启技
术执行次数一般为冷重启执行次数的 3–4 个数量级.
5
参数调节: 本文提及的技术只包含一个超参 p. 对于每一组实例集合和求解器, 参数 p 的取值范围会从 10 –
6 10 , 即总计有
5
10 之间进行简单的人工调参, 且参数的调节精度为 10 种选择. 对于每一个求解器及一组实例集合,
每一种冷重启技术均会选择出一个最优的参数, 并汇报于表 2 中的“p”列. 参数的调节目标是达到最优的综合性能,
且所有的参数均以科学计数法表示. 更精细的参数调整有潜力带来更好的实验结果, 例如提高一倍精度的情况下,
kissat-MAB+FC 在 6.5E5 及 7.5E5 均可唯一求解出一个其他参数下无法求解的实例. 本文主要聚焦于规律的观察
总结, 因此未设置复杂的预测调参技术来进行优化.
3.1 遗忘变元序的冷重启技术 (FO)
变元的分支打分启发式会为每一个变元分配一个浮点数分数或者时间戳, 每次遇到冲突时会对这两个值更
新. 每一次 FO 冷重启被执行时, 若启发式维护了浮点打分, 则 FO 会将每一个变元的打分重置为 [0, 1] 之间的随
机值, 然后将变元打分增加量设置为 1, 并更新维护变元排序的数据结构 (一般为堆); 若启发式维护了时间戳, 则
FO 会重置时间戳, 产生一组随机赋值顺序并按照上述顺序重新加入数据结构 (一般为优先队列) [26] . 上述两种操作
既可以保证变元可以产生一组随机序列, 也可以使得随机扰动的影响被控制在一次冲突以内.
本文在 3 个基础求解器上实现了 FO 冷重启技术, 实验结果被汇总于表 2.