决策变元选择_决策分支策略——文献学习Exponential Recency Weighted Average Branching Heuristic for SAT Solvers
作者：互联网
Exponential Recency Weighted Average Branching Heuristic for SAT Solvers
Jia Hui Liang, Vijay Ganesh, Pascal Poupart,等. Exponential Recency Weighted Average Branching Heuristic for SAT Solvers[C]// Thirtieth Aaai Conference on Artificial Intelligence. AAAI Press, 2016.
conflict history-based branching heuristic (CHB)
Abstract
|
Modern conflict-driven clause-learning SAT solvers routinely solve large real-world instances with millions of clauses and variables in them. Their success crucially depends on effective branching heuristics. In this paper, we propose a new branching heuristic inspired by the exponential recency weighted average algorithm used to solve the bandit problem. The branching heuristic, we call CHB, learns online which variables to branch on by leveraging the feedback received from conflict analysis.译文：通过利用从冲突分析中得到的反馈，在线学习哪些变量可以进行分支。
We evaluated CHB on 1200 instances from the SAT Competition 2013 and 2014 instances, and showed that CHB solves significantly more instances than VSIDS, currently the most effective branching heuristic in widespread use.More precisely, we implemented CHB as part of the MiniSat and Glucose solvers, and performed an apple-to-apple comparison with their VSIDS-based variants. CHB-based MiniSat (resp. CHB-based Glucose) solved approximately 16.1% (resp. 5.6%) more instances than their VSIDS-based variants. Additionally, CHB-based solvers are much more efficient at constructing first preimage attacks on step-reduced SHA-1 and MD5 cryptographic hash functions, than their VSIDS-based counterparts.译文：此外，基于chb的求解器在构造针对阶减SHA-1和MD5加密哈希函数的第一次原像攻击时，比基于vsid的求解器要高效得多。
To the best of our knowledge, CHB is the first branching heuristic to solve significantly more instances than VSIDS on a large, diverse benchmark of real-world instances. |
|
Modern conflict-driven clause-learning SAT solvers routinely solve large real-world instances with millions of clauses and variables in them. Their success crucially depends on effective branching heuristics. |
remain as the most effective ones in widespread use today. Lagoudakis and Littman took 7 well-known SAT 译文： |
|
Second, until very recently, little was understood as to why the VSIDS branching heuristic and its variants are so effective.译文：其次，直到最近，人们对为什么VSIDS分支启发式及其变体如此有效还知之甚少。 |
|
Inspired by the bandit framework and reinforcement learning, we learn to choose good variables to branch based on past experience. Our goal is to leverage the theory and practice of a rich sub-field of reinforcement learning to plain and design an effective branching heuristic for solving real-world problems. 译文：受到bandit框架和强化学习的启发，我们学会根据过去的经验选择好的变量进行分支。我们的目标是利用理论和实践的丰富子领域的强化学习，以平原和设计一个有效的分支启发式解决实际问题。 分支决策变元的选择包含强化学习的思想 |
| The branching heuristic proposed in this paper, CHB, is completely online and learns which variable to branch on
dynamically as the input instance is being solved. By online we mean that the heuristic learns only during the olving 译文：本文提出的分支启发式CHB是完全在线的，并在求解输入实例时动态地学习在哪个变量上进行分支。线上是指启发式只在存活过程中学习，而不存在线下学习。 |
|
Exponential Recency Weighted Average (ERWA)
|
|
The CHB Branching Heuristic
|
 |
Future Work
|
The connection between branching heuristics and reinforcement learning opens many new opportunities for future improvements to branching heuristics and SAT solving in general.译文：分支启发式和强化学习之间的联系为分支启发式和SAT解决的未来改进打开了许多新的机会。
Modern CDCL SAT solvers maintain lots of state features such as the partial assignment, trail, learnt clause database, saved phases, etc. 译文：现代CDCL SAT求解器维护了许多状态特性，如部分赋值、跟踪、学习子句数据库、保存阶段等。 The technique proposed in this paper is based on the multi-armed bandit setting, and it can be extended to a full Markov decision process by conditioning the choice of variables on some of the solvers’ state features. More research is needed to find a stateful model that works well in practice by balancing the trade-off between the gain in information due to states and the cost of increased model complexity. |
| We modeled our branching heuristic on ERWA, a technique used to solve the bandit problem. However, perhaps a more powerful model will capture both the branching heuristic and clause learning. It is evident that the branching heuristic and clause learning drive each other, so a model capturing both aspects can lead to algorithms that not only choose better branching variables, but also learn higher quality clauses. It is clear that such a model is outside the bandit framework, due to the additional feedback from clause learning to the branching heuristic in the form of learnt clauses. More work is needed to construct new models that include more aspects of CDCL such as clause learning. |
References
1. The community structure of SAT formulas By: Ansotegui, Carlos; Giraldez-Cru, Jesus; Levy, Jordi. LNCS Pages: 410-423 Published: 2012 Times Cited: 28 2. Refining Restarts Strategies for SAT and UNSAT By: Audemard, G.; Simon, L. Principles and Practice of Constraint Programming. Proceedings 18th International Conference, CP 2012 Pages: 118-26 Published: 2012 Times Cited: 27 3. Glucose 2.3 in the SAT 2013 Competition By: Audemard, G.; Simon, L. DEP COMPUTER SCI S B Pages: 42-43 Published: 2013 Times Cited: 15 4. Predicting Learnt Clauses Quality in Modern SAT Solvers By: Audemard, Gilles; Simon, Laurent 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS Pages: 399-404 Published: 2009 Times Cited: 165 5. Solver and benchmark descriptions By: Balint, A.; Belov, A.; Heule, M. J. H.; et al. P SAT COMP 2013 Volume: B-2013-1 Published: 2013 Publisher: University of Helsinki [Show additional data] Times Cited: 2 6. Solver and benchmark descriptions. By: Belov, A.; Diepold, D.; Heule, M. J. H.; et al. P SAT COMP 2014 Volume: B-2014-2 Published: 2014 [Show additional data] Times Cited: 2 7. Bounded Model Checking By: Biere, A; Cimatti, A; Clarke, EM; et al. ADVANCES IN COMPUTERS, VOL 58: HIGHLY DEPENDABLE SOFTWARE Book Series: Advances in Computers Volume: 58 Pages: 117-148 Published: 2003 Times Cited: 208 8. Lingeling, plingeling, picosat and precosat at SAT race 2010 By: Biere, A. FMV Report Series Technical Report Volume: 10 Issue: 1 Published: 2010 Times Cited: 8 9. Evaluating CDCL Variable Scoring Schemes By: Biere, Armin; Froehlich, Andreas THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015 Book Series: Lecture Notes in Computer Science Volume: 9340 Pages: 405-422 Published: 2015 Times Cited: 16 10 EXE: Automatically Generating Inputs of Death By: Cadar, Cristian; Ganesh, Vijay; Pawlowski, Peter M.; et al. ACM TRANSACTIONS ON INFORMATION AND SYSTEM SECURITY Volume: 12 Issue: 2 Article Number: 10 Published: DEC 2008 Times Cited: 118 11. Minisat blbd. By: Chen, J. P SAT COMP 2014 Volume: B-2014-2 Pages: 45 Published: 2014 Times Cited: 1 12. BerkMin: A fast and robust sat-solver By: Goldberg, Eugene; Novikov, Yakov DISCRETE APPLIED MATHEMATICS Volume: 155 Issue: 12 Special Issue: SI Pages: 1549-1561 Published: JUN 15 2007 Times Cited: 39 13 Solving propositional satisfiability problems By: Jeroslow, R.; Wang, J. Ann. of Mathematics and Artificial Intelligence Volume: 1 Pages: 167-187 Published: 1990 Times Cited: 113 14. Empirical Study of the Anatomy of Modern Sat Solvers By: Katebi, Hadi; Sakallah, Karem A.; Marques-Silva, Joao P. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2011 Book Series: Lecture Notes in Computer Science Volume: 6695 Pages: 343-356 Published: 2011 Times Cited: 19 15. Learning to select branching rules in the DPLL procedure for satisfiability By: Lagoudakis, M.G.; Littman, M.L. Electron. Notes Discrete Math Volume: 9 Pages: 344-359 Published: 2001 Times Cited: 16 16. Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers By: Liang, Jia Hui; Ganesh, Vijay; Zulkoski, Ed; et al. LNCS Volume: 9434 Pages: 225-241 Published: 2015 Publisher: Springer [Show additional data] Times Cited: 11 17. The impact of branching heuristics in propositional satisfiability algorithms By: Marques-Silva, J. Progress in Artificial Intelligence. 9th Portuguese Conference on Artificial Intelligence, EPIA'99. Proceedings (Lecture Notes in Artificial Intelligence Vol.1695) Pages: 62-74 Published: 1999 Times Cited: 36 18. GRASP: A search algorithm for propositional satisfiability By: Marques-Silva, JP; Sakallah, KA IEEE TRANSACTIONS ON COMPUTERS Volume: 48 Issue: 5 Pages: 506-521 Published: MAY 1999 Times Cited: 583 19. Applications of SAT solvers to cryptanalysis of hash functions By: Mironov, Ilya; Zhang, Lintao THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS Book Series: LECTURE NOTES IN COMPUTER SCIENCE Volume: 4121 Pages: 102-115 Published: 2006 Times Cited: 54 20. Chaff: Engineering an efficient SAT solver By: Moskewicz, MW; Madigan, CF; Zhao, Y; et al. 38TH DESIGN AUTOMATION CONFERENCE PROCEEDINGS 2001 Book Series: DESIGN AUTOMATION CONFERENCE Pages: 530-535 Published: 2001 Times Cited: 1,151 21. Planning and SAT By: Rintanen, Jussi HANDBOOK OF SATISFIABILITY Book Series: Frontiers in Artificial Intelligence and Applications Volume: 185 Pages: 483-504 Published: 2009 Times Cited: 16 22. Glucose: a solver that predicts learnt clauses quality By: Simon, L.; Audemard, G. SAT Competition Pages: 7-8 Published: 2009 Times Cited: 3 23. Title: [not available] By: Soos, M. Cryptominisat 2.5.0. SAT Race competitive event booklet Published: 2010 Times Cited: 6 24. Minisat v1.13-A SAT solver with con-flict-clause minimization By: Sorensson, N.; Een, N. P SYST DESCR SAT COM Volume: 2005 Pages: 53 Published: 2005 Times Cited: 24 25. StarExec: A Cross-Community Infrastructure for Logic Solving By: Stump, Aaron; Sutcliffe, Geoff; Tinelli, Cesare AUTOMATED REASONING, IJCAR 2014 Book Series: Lecture Notes in Artificial Intelligence Volume: 8562 Pages: 367-373 Published: 2014 Times Cited: 43 26. Title: [not available] By: Sutton, R.S.; Barto, A.G. Reinforcement Learning: an Introduction Volume: 1 Issue: 1 Published: 1998 Publisher: MIT press, Cambridge Times Cited: 1,003
标签：Heuristic,Weighted,branching,Cited,决策,Times,Published,Pages,SAT 来源： https://www.cnblogs.com/yuweng1689/p/13201415.html