CDCLSAT求解器的重启策略分析

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

基于变量混合特征的分支启发式策略

先进的SAT求解器能够通过有效的分支启发式策略解决大型应用实例.目前VSIDS策略是最具有代表性的基于冲突分析的分支策略,它因其稳健性而被广泛使用,但在每次冲突分析中其判定变量活性的增量方式过于单一.针对此问题,本文提出了一种基于变量混合特征的分支启发式算法,目的是充分地利用参与冲突分析的变量所携带的不同信息特征来区分变量,来进一步指导变量活性增长.并将所提出的分支策略算法嵌入到Glucose4.1中形成求解器Glucose4.1+MFBS,通过对比测试,实验结果表明改进的分支算法比原本的VSIDS策略,具有一定的优势,求解明显个数增加.