节点文献
SAT问题求解器重启策略对比分析
Comparative Analysis of Restart Strategy of Satisfiability Problem Solver
【摘要】 已有研究表明,在SAT求解器中引入重启可以极大地提高求解性能,并已出现了许多不同重启策略.目前还缺少全面的对比分析研究.为了避免重启策略选择的随意性,同时启发设计更好的重启策略,本文选择了具有代表性的7种重启策略,以目前广泛采用的Minisat为基本求解器,在国际SAT2011竞赛中实际应用类基准测试集之上进行了实验对比分析.结果表明:(1)不同重启策略对SAT求解器的求解过程和求解性能影响巨大;(2)在应用类测试集上,几何序列调度策略的平均综合性能优于其他策略;(3)在限定范围内,重启频率越大,求解器综合性能越好;(4)增量变化的重启频率可以克服固定重启频率导致不完备搜索的问题.
【Abstract】 It has been proved that the introduction of restart can greatly improve solving performance in the SAT solver,and many different 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 experimental results show that( i) restart strategy can enormously impact on the solving process and performance of SAT solver;( ii) the geometric 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.
【Key words】 satisfiability problem; solver; conflict-driven clause learning; restart strategy;
- 【文献出处】 小型微型计算机系统 ,Journal of Chinese Computer Systems , 编辑部邮箱 ,2013年12期
- 【分类号】TP18
- 【被引频次】4
- 【下载频次】71