CDCLSAT求解器的重启策略分析  

Comprehensive Analysis of Restart Strategies of CDCL SAT Solver

作　　者：程睿 周彩兰[1] 徐宁[1] 周强[2] Cheng Rui;Zhou Cailan;Xu Ning;Zhou Qiang(School of Computer Science and Technology, Wuhan University of Technology, Wuhan 430070;School of Computer Science and Technology, Tsinghua University, Beijing 100084)

机构地区：[1]武汉理工大学计算机科学与技术学院,武汉430070 [2]清华大学计算机科学与技术系,北京100084

出　　处：《计算机辅助设计与图形学学报》2018年第6期1136-1144,共9页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(61774091)

摘　　要：CDCL SAT求解器在形式验证等领域应用广泛,但重启策略众多且参数控制复杂,导致通常选择默认参数下的策略,从而降低求解器的效率和易用性.为了提高CDCL SAT求解器的实用性,通过实验分析重启序列、重启间隔、间隔增长系数等因素对实例求解效率的影响,以及求解初期的决策变量数等行为特征数据集与重启策略集之间的关系.实验结果表明,通过改变重启策略可以提高求解效率,所得到的最优解比缺省解的效率可提高6 959%,平均提高411%;重启策略在求解过程中表现出较大的个体差异性和一定的群体差异性;相比重启频率,重启序列对求解效率影响更大.进一步用7种重启策略集合覆盖97%案列的最优重启策略,通过求解初期的特征值变化频率与相应的重启策略关联,为后期选择最优重启策略提供技术支持.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 order to improve the practicability of CDCL algorithms, this paper analyzes how restart strategies effect solving performance, and relationship between the initial feature sets and the restart strategy sets. Results demonstrate that the gap between the optimal solution and default solving performance reaches 6959%, on average, 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; Changing 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算法 SAT求解器 重启策略 重启序列 重启策略选择 

分 类 号：TP391.41[自动化与计算机技术—计算机应用技术]