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