SAT问题求解器重启策略对比分析  

Comparative Analysis of Restart Strategy of Satisfiability Problem Solver

作　　者：郭莹[1,2] 张斌[1] 张长胜[1] 

机构地区：[1]东北大学信息科学与工程学院,沈阳110819 [2]宁夏理工学院电气信息工程学院,宁夏石嘴山753000

出　　处：《小型微型计算机系统》2013年第12期2729-2733,共5页Journal of Chinese Computer Systems

基　　金：国家教育部少数民族高级骨干人才培养基金项目(教民[2008-8])资助;国家自然科学基金项目(61073062;61100090)资助;东北大学中央高校基本科研业务费项目(N11024006)资助

摘　　要：已有研究表明,在SAT求解器中引入重启可以极大地提高求解性能,并已出现了许多不同重启策略.目前还缺少全面的对比分析研究.为了避免重启策略选择的随意性,同时启发设计更好的重启策略,本文选择了具有代表性的7种重启策略,以目前广泛采用的Minisat为基本求解器,在国际SAT2011竞赛中实际应用类基准测试集之上进行了实验对比分析.结果表明:(1)不同重启策略对SAT求解器的求解过程和求解性能影响巨大;(2)在应用类测试集上,几何序列调度策略的平均综合性能优于其他策略;(3)在限定范围内,重启频率越大,求解器综合性能越好;(4)增量变化的重启频率可以克服固定重启频率导致不完备搜索的问题.It has been proved that the introduction of restart can greatly improve solving performance in the SAT solver, and many dif- ferent restart strategies appear accordingly. However, no comprehensive comparative analysis has been made for them currently. To avoid the arbitrariness of the restart strategy selection and inspire the designing of better restart strategy, seven representative restart strategies are selected to make a series of experimental comparative analysis. We take Minisat which is currently widely used as the basic solver, and take some application benchmarks from the international SAT 2011 competition as our testing cases. The experimen- tal results show that { i} restart strategy can enormously impact on the solving process and performance of SAT solver; （ ii ） the geo- metric sequence scheduling strategy is superior to other strategies at average comprehensive performance with respect to application benchmarks; （ iii ） within limits, the solving performance may be better if the restart frequency is greater; （ iv ）the restart frequency with incremental changes can avoid leading to incomplete search.

关 键 词：可满足性问题 求解器 冲突驱动子句学习 重启策略 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]