Page 202 - 《软件学报》2026年第4期
P. 202
张昕荻 等: CDCL 算法的冷重启技术 1643
(2) 保留 LBD ⩽ 3 的学习子句能帮助求解器取得最优的综合性能. 实际上, 很多主流的学习子句管理算法也会
将 LBD = 3 作为学习子句分组的标准 [16] .
表 3 遗忘变元序、遗忘赋值倾向和遗忘学习子句的冷重启结果汇总
实例集合 遗忘子句 #SAT PAR2 (SAT) #UNS PAR2 (UNS) #ALL PAR2 (ALL)
LBD > 0 158 2 278.36 109 3 421.98 267 3 879.05
LBD > 1 155 2 385.65 115 3 082.32 270 2 689.80
SAT比赛2020年标准 LBD > 2 153 2 428.49 120 2 622.74 273 2 513.30
测试实例集合 (400个实例) LBD > 3 154 2 405.37 120 2 578.99 274 2 481.17
LBD > 4 153 2 447.50 122 2 494.85 275 2 668.17
LBD > 5 153 2 495.89 121 2 542.93 274 2 516.38
LBD > 0 143 1 677.60 137 3 339.01 280 3 573.68
LBD > 1 144 1 626.29 141 3 072.62 285 2 403.80
SAT比赛2021年标准 LBD > 2 142 1 708.98 142 2 924.58 284 2 362.45
测试实例集合 (400个实例) LBD > 3 143 1 742.83 151 2 636.28 293 2 223.13
LBD > 4 140 1 748.33 149 2 669.04 289 2 243.28
LBD > 5 138 1 840.09 150 2 643.33 288 2 271.89
3.3.2 学习子句的使用效率研究
为了回答我们的猜测, 我们对学习子句的使用情况进行了研究. CDCL 算法中子句一般只有推理和参与冲突两
种用途. 单元子句一般会直接用于固定一个变元, 不会加入子句管理数据库, 因此, 本节选择 LBD 介于 2–7 的所有
学习子句, 并追踪它们参与推理和冲突的次数. 当一条子句在 BCP 中参与推出了一个变元的赋值, 则它被认为参与
了一次推理; 当一条子句参与到一次冲突和新学习子句的产生, 则它被认为参与了一次冲突. 搜索过程中一条学习
子句的 LBD 会经常发生变动, 为了方便数据统计, 一条学习子句的 LBD 被算作是该子句产生时的 LBD 数值.
本文统计了不同 LBD 的学习子句参与冲突和推理的次数, 并根据 LBD = 2 的数据进行标准化, 然后将数据汇
总于表 4. 由表中的数据可知, 算法中学习子句的使用效率在“LBD = 2”和“LBD = 3”之间发生了巨大的衰退, 其他
相邻列之间的衰退则明显较小.
表 4 不同 LBD 学习子句使用次数的标准化数据
类型 LBD = 2 LBD = 3 LBD = 4 LBD = 5 LBD = 6 LBD = 7
参与冲突 1.0 0.264 1 0.188 7 0.138 1 0.100 4 0.067 0
参与推理 1.0 0.189 9 0.128 9 0.083 3 0.044 7 0.021 5
观察 4. 遗忘学习子句的冷重启技术总是会使得不可满足实例求解性能变差, 但通常会 (不全是) 使得可满足
实例求解性能提高. 另一方面, 尽可能多地保留学习子句有利于不可满足的证明, 但不利于可满足实例的证明, 这
是由于低质量学习子句虽然可以用于剪枝搜索空间, 但其利用率较差.
3.4 遗忘多种类型信息的冷重启技术
第 3.1–3.3 节分别对 3 种单独的冷重启技术进行了讨论, 本节则进一步对复合冷重启开展研究, 即在重启时遗
忘多种搜索信息的冷重启技术. 混合冷重启策略有如下的 4 种复合形式.
● FO+FP: 重启时, 求解器会随机打乱变元序, 并随机重置相位.
● FO+FC: 重启时, 求解器会随机打乱变元序, 并清空学习子句数据库.
● FP+FC: 重启时, 求解器会随机重置相位, 并清空学习子句数据库.
● FO+FP+FC: 重启时, 求解器会随机打乱变元序, 随机重置相位, 并清空学习子句数据库.
表 5 汇报了复合冷重启的实验结果, 给出了每一个求解器的最优复合配置和对应的求解数目变化情况. 在
SC20 和 SC21 实例集合上, 对于每一个求解器, 本文分别在 ∆ SAT 、 ∆ UNS 和 ∆ ALL 这 3 列中报告了其在 SAT、UNS
和 ALL 上最优的求解效果变化情况, 和对应的最优复合配置 (C 列). 表格中仅汇报求解数量最多的一种策略, 若
有多种策略取得最优求解数目, 则汇报 PAR2 最小的复合配置.
