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

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

CV), 即一组数据的标准差与该组数据平均数的比值. CV 值越高说明该组数据的离散程度越高. 我们进一步计算
了实例集合上所有数据 CV 的均值.
对于不同的初始随机变元序的运行时间, 可满足实例集合上的平均 CV 值为 71.5%, 不可满足实例集合上的
平均 CV 值为 27.2%. 对于不同的初始随机相位的运行时间, 可满足实例集合上的平均 CV 值为 71.8%, 不可满足
实例集合上的平均 CV 值为 36.8%.
于是, 我们可以得到如下的观察结论, 并回答了 RQ1.
观察 1. 目前主流 CDCL 的性能 (运行时间) 对于初始变元序和初始赋值倾向十分敏感, 尤其是对于可满足实例.
对于可满足问题, 分支启发式直接决定了算法搜索的大方向; 对于不可满足问题, 启发式影响了冲突归结产生
学习子句的顺序和质量, 影响了对搜索空间的剪枝效率. 热重启倾向于使用重启前的启发式信息, 使 CDCL 处于
一个不利于求解的上下文时, 难以跳出当前搜索空间去探索其他区域, 因此会出现求解时间的大幅扰动. 此外, 对
于可满足实例, SAT 求解器会在遇到第 1 个解时退出, 因此求解时间对搜索启发式更加敏感.

3 串行冷重启技术
很多组合优化问题的算法, 引入一定的随机噪声都会使得求解时间发生明显的变化 [21,43] . 早期学者普遍采用
重启技术增加算法的探索性, 以提升算法求解速度. 然而, 顶尖的 CDCL 求解器通常使用了一种高频热重启的策
略, 保留了所有搜索信息. 即, 重启后保留用于剪枝的学习子句的同时, 保留基于冲突历史的变元排序打分 [44] , 保
留变元回退前的赋值倾向 [35] . 因此, 当前的 CDCL 求解器倾向于重启之后快速地回到之前的搜索区域.
通过第 2 节的实验, 现存的 CDCL 算法仍然存在运行时间严重的不稳定现象, 这极有可能是目前 CDCL 普遍
采用热重启策略导致的. 为了减少求解器长时间卡在一个不利的搜索空间的概率, 本节提出了本文研究的核心问
题, 并给出了 4 项研究观察.
RQ2: 重启之后的搜索信息是否应该被保留?
本文称主流 CDCL 普遍采用的重启策略为热重启, 并保留了 3 种主要的搜索信息: 变元的搜索顺序 (通过保
留变元打分)、变元赋值倾向 (通过保留变元相位) 和学习子句. 对称地, 本文称在重启之后遗忘掉所有搜索信息的
重启策略为“完全冷重启”, 且遗忘掉部分搜索信息的重启策略为“部分冷重启”技术. 为了方便区别于主流 CDCL
中的技术, 上述两种策略都统称为“冷重启”技术.
本节, 我们首先研究了 3 种单独的基础冷重启策略 (表 2), 然后进一步研究三者的组合冷重启技术 (见第
3.4 节).

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

数据集合 求解器 种类 #SAT PAR2 (SAT) #UNS PAR2 (UNS) #ALL PAR2 (ALL) p
默认 107 5 043.39 113 3 095.50 220 5 078.55 －
+FO 113 (+6) 4 846.62 111 (−2) 3 175.93 224 (+4) 5 014.36 1E6
Maple-DL
+FP 114 (+7) 4 731.01 111 (−2) 3 179.28 225 (+5) 4 960.39 8E5
+FC 114 (+7) 4 869.95 105 (−8) 3 620.68 219 (−1) 5 190.05 1E6
默认 123 4 247.01 120 2 853.88 243 4 608.88 －
SAT比赛2020年 +FO 126 (+6) 3 998.46 123 (+3) 2 704.77 249 (+6) 4 435.03 1E6
CaDiCaLWS
数据集合 (400个实例) +FP 130 (+7) 3 891.82 122 (+2) 2 796.81 252 (+9) 4 418.14 3E5
+FC 125 (+2) 4 110.95 112 (−8) 3 298.22 237 (−5) 4 708.32 6E5
默认 151 2 510.49 121 2 557.91 272 3 670.18 －
+FO 159 (+8) 2 226.81 122 (+1) 2 515.19 281 (+9) 3 518.92 8E5
kissat-MAB
+FP 156 (+5) 2 363.07 122 (+1) 2 591.20 278 (+6) 3 614.02 1E6
+FC 158 (+7) 2 278.36 109 (−12) 3 421.98 267 (−5) 3 879.05 7E5
默认 115 3 458.14 143 3 076.04 258 4 163.22 －
SAT比赛2021年 +FO 120 (+5) 3 270.75 146 (+3) 3 067.84 266 (+8) 4 084.84 1E6
Maple-DL
数据集合 (400个实例) +FP 118 (+3) 3 279.54 144 (+1) 3 054.42 262 (+4) 4 082.84 1E6
+FC 115 3 520.02 132 (−11) 3 637.65 247 (−11) 4 449.51 1E6