码迷,mamicode.com
首页 > 其他好文 > 详细

决策变元选择_决策分支策略——文献学习A branching heuristic for SAT solvers based on complete implication graphs

时间:2020-06-28 22:11:49      阅读:63      评论:0      收藏:0      [点我收藏+]

标签:ast   dcl   let   not   tom   col   val   ever   orm   

A branching heuristic for SAT solvers based on complete implication graphs

Xiao, F., Li, C., Luo, M. et al. A branching heuristic for SAT solvers based on complete implication graphs. Sci. China Inf. Sci. 62, 72103 (2019). https://doi.org/10.1007/s11432-017-9467-7

 

除了VSIDS和LRB之外,新的决策变元选择(活跃度)策略——基于activity_distance[v]


Abstract

The performance of modern conflict-driven clause learning (CDCL) SAT solvers strongly depends on branching heuristics. State-of-the-art branching heuristics, such as variable state independent decaying sum (VSIDS) and learning rate branching (LRB), are computed and maintained by aggregating the occurrences of the variables in conflicts. However, these heuristics are not sufficiently accurate at the beginning of the search because they are based on very few conflicts.

 

We propose the distance branching heuristic, which, given a conflict, constructs a complete implication graph and increments the score of a variable considering the longest distance between the variable and the conflict rather than the simple presence of the variable in the graph. 译文:给定一个冲突,构造一个完整的隐含图,并考虑变量与冲突之间的最长距离,而不是简单地考虑变量在图中的存在,增加变量的得分。

 

We implemented the proposed distance branching heuristic in Maple_LCM and Glucose-3.0, two of the best CDCL SAT solvers, and used the resulting solvers to solve instances from the application and crafted tracks of the 2014 and 2016 SAT competitions and the main track of the 2017 SAT competition. The empirical results demonstrate that using the proposed distance branching heuristic in the initialization phase of Maple_LCM and Glucose-3.0 solvers improves performance. The Maple_LCM solver with the proposed distance branching heuristic in the initialization phase won the main track of the 2017 SAT competition.

 

 

References

  1. 1

    Audemard G, Simon L. Glucose 2.3 in the SAT 2013 competition. In: Proceedings of SAT Competition, 2013. 42–43

    Google Scholar 

  2. 2

    Biere A. Lingeling, Plingeling, Picosat and Precosat at SAT Race 2010. FMV Report Series, Technical Report 10/1, 2010

    Google Scholar 

  3. 3

    Eén N, Sorensson N. An extensible SAT solver. In: Proceedings of SAT, 2003. 502–518

    Google Scholar 

  4. 4

    Marques-Silva J, Sakallah K A. GRASP — a new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer-Aided Design, 1996. 220–227

    Google Scholar 

  5. 5

    Moskewicz M, Madigan C, Zhao Y, et al. Chaff: engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, 2001. 530–535

    Google Scholar 

  6. 6

    Soos M. CryptoMiniSat v4. In: Proceedings of SAT Competition, 2014. 23

    Google Scholar 

  7. 7

    Marques-Silva J, Lynce I, Malik S. Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability. Washington: IOS Press, 2009. 131–153

    Google Scholar 

  8. 8

    Liang J H, Ganesh V, Poupart P, et al. Exponential recency weighted average branching heuristic for SAT solvers. In: Proceedings of AAAI, 2016. 3434–3440

    Google Scholar 

  9. 9

    Audemard G, Simon L. Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of IJCAI, 2009. 399–404

    Google Scholar 

  10. 10

    Luo M, Li C M, Xiao F, et al. An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings of IJCAI, 2017. 703–711

    Google Scholar 

  11. 11

    Xiao F, Luo M, Li C M, et al. MapleLRB LCM, Maple_LCM, Maple_LCM_Dist, MapleLRB_LCMoccRestart and Glucose-3.0+width in SAT Competition 2017. In: Proceedings of SAT Competition, 2017. 22–23

    Google Scholar 

  12. 12

    Audemard G, Simon L. Refining restarts strategies for SAT and UNSAT. In: Proceedings of International Conference on Principles and Practice of Constraint Programming, 2012. 118–126

    Google Scholar 

  13. 13

    Biere A, Förhlich A. Evaluating CDCL variable scoring schemes. In: Proceedings of SAT, 2015. 405–422

    Google Scholar 

  14. 14

    Goldberg E, Novikov Y. BerkMin: a fast and robust Sat-solver. Discrete Appl Math, 2007, 155: 1549–1561

    MathSciNet Article MATH Google Scholar 

  15. 15

    Jeroslow R G, Wang J. Solving propositional satisfiability problems. Ann Math Artif Intell, 1990, 1: 167–187

    Article MATH Google Scholar 

  16. 16

    Marques-Silva J. The impact of branching heuristics in propositional satisfiability algorithms. In: Proceedings of EPIA, 1999. 850

    Google Scholar 

  17. 17

    Audemard G, Simon L. GLUCOSE: a solver that predicts learnt clauses quality. In: Proceedings of SAT Competition, 2009. 7–8

    Google Scholar 

  18. 18

    Audemard G, Simon L. Glucose in the SAT 2014 competition. In: Proceedings of SAT Competition, 2014. 31–32

    Google Scholar 

  19. 19

    Liang J H, Ganesh V, Poupart P, et al. Learning rate based branching heuristic for SAT solvers. In: Proceedings of SAT, 2016. 123–140

    Google Scholar 

  20. 20

    Liang J H, Oh C, Ganesh V, et al. MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB. In: Proceedings of SAT Competition, 2016. 52–53

    Google Scholar 

  21. 21

    Li C M, Manyá F, Mohamedou N O, et al. Resolution-based lower bounds in MaxSAT. Constraints, 2010, 15: 456–484

 

决策变元选择_决策分支策略——文献学习A branching heuristic for SAT solvers based on complete implication graphs

标签:ast   dcl   let   not   tom   col   val   ever   orm   

原文地址:https://www.cnblogs.com/yuweng1689/p/13205197.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!