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

摘要：

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

关键词：CDCLSAT算法、SAT求解器、重启策略、重启序列、重启策略选择

所属期刊栏目：30

分类号：TP391.41(计算技术、计算机技术)

资助基金：国家自然科学基金61774091

在线出版日期：2018-06-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：1136-1144