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

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

对于不可满足实例, CDCL 求解器运行时间的差异性相对较小. 从图 1(b) 可知, 通过扰动 kissat-MAB 的初始
±4 倍以内.
变元序, 不可满足实例的求解时间变化通常在

5
10 3 4×
10 2
T baseline T sample 10 1 32× T baseline T sample 10 0 1×

10 0 1×
0.25×
0.2
−1 0.125×
10
(a) 可满足实例 (b) 不可满足实例
图 1 不同初始变元搜索顺序下的运行时间扰动图

2.2 不同初始赋值倾向下的运行时间差异
变元赋值倾向 (相位) 是另一个对 CDCL 的搜索顺序有巨大影响的启发式. 我们同样也研究了随机相位对于
求解器性能的影响. 实验按照与第 2.1 节相似的方法和设置执行, 并将实验的结果进行了总结. 其中初始相位的结
果与图 1 中初始变元序的时间扰动图类似, 故不再过多赘述.
为了更加客观地呈现时间的变化情况, 表 1 中分别给出了在随机初始变元序和初始相位采样下, 时间变化的
统计数据. 本文根据可满足性将实例进行了分类, 并统计了每一个实例在 100 次采样下的求解情况. 对于每一个实
例, 我们统计了 100 次采样中基求解器可以求解, 但是扰动后无法求解的采样比例, 并将实例集合上的均值汇报于
“失败”列. 类似地, 我们也统计了相较于基求解器来说, 加速比超过 2 倍、4 倍、10 倍和 32 倍采样的平均比例 (加
速比率列), 以及求解速度变慢 0.5 倍和 0.254 倍的平均比率 (衰退比率列).

表 1 随机初始采样实验结果总结 (%)

实例集合 加速比率 衰退比率
实验 失败
(实例数) 2× 4× 10× 32× 0.5× 0.25×
SAT (151) 3.58 25.72 12.37 4.72 1.14 25.21 15.03
随机初始变元序实验 UNSAT (121) 2.1 1.7 0.06 0.0 0.0 7.78 5.22
ALL (272) 2.92 15.03 6.89 2.62 0.63 17.46 10.67
SAT (151) 3.71 25.29 13.23 3.87 1.03 21.95 10.91
随机初始相位实验 UNSAT (121) 1.02 2.95 0.79 0.03 0.0 5.31 2.2
ALL (272) 2.51 15.35 7.7 2.17 0.57 14.54 7.03

此外, 最近顶尖的 CDCL 求解器普遍采用了一种相位重置技术 (rephase) [18,36] , 该技术会定期地更新变元的相
位, 并优先将相位更新为 CDCL 搜索的较深的赋值倾向, 或者更新为局部搜索中取得的一致性较高的完全赋值.
尽管相位重置技术会引入一定概率的随机性, 但是采用了该技术的 CDCL 求解器的运行时间仍然存在明显的运
行时间扰动.
相位重置技术中定期更改相位为高一致性赋值会大幅提高性能, 于是本文进一步测试是否高一致性的初始赋
值会使得 100 次采样中出现求解性能更高的加速比. 我们尝试利用单元传播技术来构建高一致性的初始解, 该技
术类似于 Knuth [42] 的“warm-up”的想法, 也类似于“ReasonLS”系列求解器 [18] 中为局部搜索求解器赋值的技术. 本文
同样为每一个实例, 随机产生 100 组高一致性赋值, 并统计了其求解的运行时间.
虽然该方法有更好的加速比稳定性, 但是, 该方法并不能产生比随机初始赋值更好的加速比. 该技术失败的原
因有可能是高一致性赋值使得搜索方向有更高的趋同性, 缺乏了探索性.
2.3 热重启 CDCL 观察总结
本节对随机初始变元序和随机初始相位展开了细致的实验, 发现可满足实例上的运行时间扰动明显要高于不
可满足实例上的运行时间扰动. 对于每一个实例, 我们计算了这 100 次运行时间的变异系数 (coefficient of variation,