一种求解SAT问题的动态重启策略  

An Dynamic Restart Strategy for Solving SAT Problem

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

机构地区：[1]东北大学信息科学与工程学院,辽宁沈阳110819

出　　处：《东北大学学报（自然科学版）》2014年第7期935-938,共4页Journal of Northeastern University(Natural Science)

基　　金：国家自然科学基金资助项目(61073062;61100090);中央高校基本科研业务费专项资金资助项目(N11024006);宁夏回族自治区自然科学基金资助项目(NZ13265)

摘　　要：为降低冲突驱动子句学习SAT求解器的运行计算成本,从"何时重启"和"何处重启"两个角度入手,提出一种动态启发式重启策略2WSAT.该策略将冲突决策层次和变量重启次数作为反映求解状态的重要参数,及时摆脱错误的求解分支,通过重启后选择更优的决策变量提高求解性能.采用实际应用的基准测试集,与两个流行的求解器进行了对比实验.结果表明,所提出的策略对求解速度、内存占用、冲突发生数、传播次数等关键指标有显著改善.In order to reduce the computational costs in conflict-driven clause learning solvers,an improved adaptive heuristic restart strategy named 2WSAT was proposed,which was based on two questions including＂when to restart＂and＂where to restart＂.In this strategy,the conflict decision levels and variable＇s restart times were taken as important solving state parameters,so that overall performance could be improved by escaping from wrong search branches and choosing better decision variables.Comparative experiments were conducted among 2WSAT and two modern solvers,using the practical application benchmarks.The results showed that 2WSAT has higher scores in many key indicators such as solving speed,memory usage,conflicts number,propagation number etc.

关 键 词：可满足性问题 重启策略 启发式 冲突决策层次 变量重启次数 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]