SAT solver based on CDCL has been widely used in formal verification. As the numerous restart strategies and complex parameters, choosing the default strategy reduces the efficiency and usability. In or-der to improve the practicability of CDCL algorithms, this paper analyzes how restart strategies effect solv-ing performance, and relationship between the initial feature sets and the restart strategy sets. Results dem-onstrate that the gap between the optimal solution and default solving performance reaches 6959%, on av-erage, 441%; Great individual differences and certain group differences on choosing restart strategies are shown; Compared to restart frequency, restart schedule plays a greater role in solving performance; Chang-ing the restart strategy can improve the solving performance. In addition, seven restart strategies can cover 97% of the optimal strategies. The correlation between the change frequency of the features and the seven strategies provides technical support for choosing the optimal restart strategy.%CDCL SAT求解器在形式验证等领域应用广泛, 但重启策略众多且参数控制复杂, 导致通常选择默认参数下的策略, 从而降低求解器的效率和易用性. 为了提高 CDCL SAT 求解器的实用性, 通过实验分析重启序列、重启间隔、间隔增长系数等因素对实例求解效率的影响, 以及求解初期的决策变量数等行为特征数据集与重启策略集之间的关系. 实验结果表明, 通过改变重启策略可以提高求解效率, 所得到的最优解比缺省解的效率可提高6959%, 平均提高411%; 重启策略在求解过程中表现出较大的个体差异性和一定的群体差异性; 相比重启频率, 重启序列对求解效率影响更大. 进一步用7种重启策略集合覆盖97%案列的最优重启策略, 通过求解初期的特征值变化频率与相应的重启策略关联, 为后期选择最优重启策略提供技术支持.
展开▼
