其他分享
首页 > 其他分享> > 决策变元选择_决策分支策略——文献学习Exponential Recency Weighted Average Branching Heuristic for SAT Solvers

决策变元选择_决策分支策略——文献学习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.

 

 

 
  1. Marques-Silva and Sakallah invented the CDCL technique (Marques-Silva and Sakallah 1999), 
  2. designing branching heuristics such as
    • DLIS (Marques-Silva 1999),
    • BerkMin (Goldberg and Novikov 2007), and Jeroslav-Wang (Jeroslow and Wang 1990),
    • the VSIDS branching heuristic and its variants remain( 2001)

                   remain as the most effective ones in widespread use today.

Lagoudakis and Littman took 7 well-known SAT
branching heuristics (MAXO, MOMS, MAMS, Jeroslaw-
Wang, UP, GUP, SUP) and used reinforcement learning to
switch between the heuristics dynamically during the run of
the solver (Lagoudakis and Littman 2001).

译文:
Lagoudakis和Littman采用了7个著名的SAT分支启发法(MAXO, MOMS, MAMS, Jeroslaw-)Wang, UP, GUP, SUP)和使用强化学习在求解器运行期间在启发式之间动态切换(Lagoudakis和Littman 2001)。译文:他们的技术需要对类似的实例进行离线培训。

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
process, and there is no offline learning.

译文:本文提出的分支启发式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解决的未来改进打开了许多新的机会。


We detail some of our future work below that builds on the foundation laid by this paper. 译文:在本文所奠定的基础上,我们将在下面详细说明我们未来的一些工作。

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