基于动态奖惩的CDCL SAT求解器分支启发式算法
|
摘要
分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响。为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法。每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分。用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例。实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能。
Branching heuristic algorithms play an important role in CDCL SAT solvers, and the conventional branching heuristic algorithms are more concerned with the number of conflicts when calculating the activity scores of variables and do not consider the influence of the decision level or conflict decision level. In order to improve the efficiency of solving SAT problem, we propose a dynamic reward and punishment based branching method(DRPB), which is inspired by the EVSIDS and ACIDS. Whenever a conflict occurs, the DRPB updates the activity score of variables by integrating the numbers of conflicts, decision-making level, conflict decision level, and conflict frequency of variables. We improve the Glucose version 3.0 by replacing the VSIDS algorithm with the DRPB, and conduct an empirical evaluation not only on instances of SATLIB benchmarks, but also on 2015 and 2016 SAT competitions. Experimental results show that compared with the traditional and single variable branching heuristic algorithms, the proposed strategy can reduce the size of the search tree and improve the performance of the SAT solvers by reducing the branches of the search tree and the number of Boolean constraint propagation.
Branching heuristic algorithms play an important role in CDCL SAT solvers, and the conventional branching heuristic algorithms are more concerned with the number of conflicts when calculating the activity scores of variables and do not consider the influence of the decision level or conflict decision level. In order to improve the efficiency of solving SAT problem, we propose a dynamic reward and punishment based branching method(DRPB), which is inspired by the EVSIDS and ACIDS. Whenever a conflict occurs, the DRPB updates the activity score of variables by integrating the numbers of conflicts, decision-making level, conflict decision level, and conflict frequency of variables. We improve the Glucose version 3.0 by replacing the VSIDS algorithm with the DRPB, and conduct an empirical evaluation not only on instances of SATLIB benchmarks, but also on 2015 and 2016 SAT competitions. Experimental results show that compared with the traditional and single variable branching heuristic algorithms, the proposed strategy can reduce the size of the search tree and improve the performance of the SAT solvers by reducing the branches of the search tree and the number of Boolean constraint propagation.
引文
[1] Cook S A. The complexity of theorem-proving procedures [C]//Proc of the 3rd ACM Symposium on Theory of Computing,1971:151-158.
[2] Marques-Silva J P,Sakallah K A.GRASP:A new search algorithm for satisfiability [C]//Proc of the 1996 IEEE/ACM International Conference on Computer-aided Design,1996:220-227.
[3] Bayardo R, Schrag R.Using CSP look-back techniques to solve real-world SAT instances [C]//Proc of the 14th National Conference on Artificial Intelligence,1997:203-208.
[4] Zhang H.SATO:An efficient propositional prover [C]//Proc of International Conference on Automated Deduction,1997:272-275.
[5] Moskewicz M W,Zhao Y,Madigan C F.Chaff:Engineering an efficient SAT solver [C]//Proc of the 38th Annual Design Automation Conference,2001:530-535.
[6] Goldberg E,Novikov Y.BerkMin:A fast and robust sat-solver [C]//Proc of Design,Automation and Test in Europe,2002:142-149.
[7] Eén N,S?rensson N.An extensible SAT solver [C]//Proc of International Conference on Theory and Applications of Satisfiability Testing(SAT 2003),2003:502-518.
[8] Audemard G, Simon L.Predicting learnt clauses quality in modern SAT solvers [C]//Proc of the 21st International Joint Conference on Artificial Intelligence,2009:399-404.
[9] Davis M,Logemann G,Loveland D.A machine program for theorem proving [J].Communications of the ACM,1962,5(7):394-397.
[10] Marques-Silva J P, Lynce I,Malik S.Conflict-driven clause learning SAT solvers[M]//Handbook of Satisfiability.Amsterdam:IOS Press,2009.
[11] Jeroslow R G,Wang J.Solving propositional satisfiability problems [J].Annals of Mathematics and Artificial Intelligence,1990,1(1-4):167-187.
[12] Freeman J W. Improvements to propositional satisfiability search algorithms [D].Philadelphia:University of Pennsylvania,1995.
[13] Biere A.Adaptive restart strategies for conflict driven SAT solvers [C]//Proc of International Conference on Theory and Applications of Satisfiability Testing(SAT 2008),2008:28-33.
[14] Biere A,Fr?hlich A.Evaluating CDCL variable scoring schemes [C]//Proc of Theory and Applications of Satisfiability Testing(SAT 2015),2015:405-422.
[15] Liang J H,Ganesh V,Poupart P,et al.Exponential recency weighted average branching heuristic for SAT solvers [C]//Proc of the 13th AAAI Conference on Artificial Intelligence,2016:3434-3440.
[16] Liang J H,Ganesh V,Poupart P,et al.Learning rate based branching heuristic for SAT solvers [C]//Proc of International Conference on Theory and Applications of Satisfiability Testing(SAT 2006),2016:123-140.
[17] Zhang L T,Madigan C F,Moskewicz M H,et al.Efficient conflict driven learning in a boolean satisfiability solver [C]//Proc of the 2001 IEEE/ACM International Conference on Computer-Aided Design,2001:279-285.
[2] Marques-Silva J P,Sakallah K A.GRASP:A new search algorithm for satisfiability [C]//Proc of the 1996 IEEE/ACM International Conference on Computer-aided Design,1996:220-227.
[3] Bayardo R, Schrag R.Using CSP look-back techniques to solve real-world SAT instances [C]//Proc of the 14th National Conference on Artificial Intelligence,1997:203-208.
[4] Zhang H.SATO:An efficient propositional prover [C]//Proc of International Conference on Automated Deduction,1997:272-275.
[5] Moskewicz M W,Zhao Y,Madigan C F.Chaff:Engineering an efficient SAT solver [C]//Proc of the 38th Annual Design Automation Conference,2001:530-535.
[6] Goldberg E,Novikov Y.BerkMin:A fast and robust sat-solver [C]//Proc of Design,Automation and Test in Europe,2002:142-149.
[7] Eén N,S?rensson N.An extensible SAT solver [C]//Proc of International Conference on Theory and Applications of Satisfiability Testing(SAT 2003),2003:502-518.
[8] Audemard G, Simon L.Predicting learnt clauses quality in modern SAT solvers [C]//Proc of the 21st International Joint Conference on Artificial Intelligence,2009:399-404.
[9] Davis M,Logemann G,Loveland D.A machine program for theorem proving [J].Communications of the ACM,1962,5(7):394-397.
[10] Marques-Silva J P, Lynce I,Malik S.Conflict-driven clause learning SAT solvers[M]//Handbook of Satisfiability.Amsterdam:IOS Press,2009.
[11] Jeroslow R G,Wang J.Solving propositional satisfiability problems [J].Annals of Mathematics and Artificial Intelligence,1990,1(1-4):167-187.
[12] Freeman J W. Improvements to propositional satisfiability search algorithms [D].Philadelphia:University of Pennsylvania,1995.
[13] Biere A.Adaptive restart strategies for conflict driven SAT solvers [C]//Proc of International Conference on Theory and Applications of Satisfiability Testing(SAT 2008),2008:28-33.
[14] Biere A,Fr?hlich A.Evaluating CDCL variable scoring schemes [C]//Proc of Theory and Applications of Satisfiability Testing(SAT 2015),2015:405-422.
[15] Liang J H,Ganesh V,Poupart P,et al.Exponential recency weighted average branching heuristic for SAT solvers [C]//Proc of the 13th AAAI Conference on Artificial Intelligence,2016:3434-3440.
[16] Liang J H,Ganesh V,Poupart P,et al.Learning rate based branching heuristic for SAT solvers [C]//Proc of International Conference on Theory and Applications of Satisfiability Testing(SAT 2006),2016:123-140.
[17] Zhang L T,Madigan C F,Moskewicz M H,et al.Efficient conflict driven learning in a boolean satisfiability solver [C]//Proc of the 2001 IEEE/ACM International Conference on Computer-Aided Design,2001:279-285.