CDCL SAT求解器的重启策略分析

• 作者: 周强 周彩兰 徐宁 程睿
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: CDCLSAT算法 SAT求解器 重启策略 重启序列 重启策略选择
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: VLSI 设计与测试及电子设计自动化
• 页码范围: 1136-1144
• 页数: 9页
• 分类号: TP391.41
• 字数: 7587字
• 语种: 中文
• DOI: 10.3724/SP.J.1089.2018.16694

摘要

CDCL SAT求解器在形式验证等领域应用广泛, 但重启策略众多且参数控制复杂, 导致通常选择默认参数下的策略, 从而降低求解器的效率和易用性. 为了提高 CDCL SAT 求解器的实用性, 通过实验分析重启序列、重启间隔、间隔增长系数等因素对实例求解效率的影响, 以及求解初期的决策变量数等行为特征数据集与重启策略集之间的关系. 实验结果表明, 通过改变重启策略可以提高求解效率, 所得到的最优解比缺省解的效率可提高6959%, 平均提高411%; 重启策略在求解过程中表现出较大的个体差异性和一定的群体差异性; 相比重启频率, 重启序列对求解效率影响更大. 进一步用7种重启策略集合覆盖97%案列的最优重启策略, 通过求解初期的特征值变化频率与相应的重启策略关联, 为后期选择最优重启策略提供技术支持.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周强	清华大学计算机科学与技术系	73	599	13.0	22.0
2	徐宁	武汉理工大学计算机科学与技术学院	20	71	5.0	7.0
3	周彩兰	武汉理工大学计算机科学与技术学院	33	367	11.0	18.0
4	程睿	武汉理工大学计算机科学与技术学院	1	3	1.0	1.0