Exponential Recency Weighted Average Branching Heuristic for SAT Solvers (1185833), страница 4

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 4)

More work is needed to construct new models thatinclude more aspects of CDCL such as clause learning.ConclusionWe introduced a new branching heuristic CHB inspired bythe multi-armed bandit problem, a special case of reinforcement learning. We evaluated the heuristic on two popular SAT solvers, MiniSat and Glucose, and demonstratedthat CHB solves more instances than VSIDS on a largeand diverse benchmark containing 1200 instances from recent SAT competitions and 60 instances of first preimageattacks on cryptographic hash functions. The results showthat CHB is more effective in CDCL SAT solvers at solving instances than the longstanding state-of-the-art VSIDSbranching heuristic.ReferencesAnsótegui, C.; Giráldez-Cru, J.; and Levy, J. 2012.

Thecommunity structure of SAT formulas. In Theory and Applications of Satisfiability Testing–SAT 2012. Springer. 410–423.Audemard, G., and Simon, L. 2009a. Glucose: a solver thatpredicts learnt clauses quality. SAT Competition 7–8.Audemard, G., and Simon, L. 2009b. Predicting learntclauses quality in modern SAT solvers. In IJCAI, volume 9,399–404.Audemard, G., and Simon, L. 2012. Refining restarts strategies for SAT and UNSAT. In Principles and Practice ofConstraint Programming, 118–126. Springer.Audemard, G., and Simon, L.

2013. Glucose 2.3 in the sat2013 competition. In Proceedings of SAT Competition 2013,42–43.Balint, A.; Belov, A.; Heule, M. J. H.; and Järvisalo, M.2013. Solver and benchmark descriptions. In Proceedingsof SAT Competition 2013, volume B-2013-1. University ofHelsinki.Belov, A.; Diepold, D.; Heule, M. J. H.; and Järvisalo, M.2014. Solver and benchmark descriptions. In Proceedingsof SAT Competition 2014, volume B-2014-2. University ofHelsinki.Biere, A., and Fröhlich, A.

2015. Evaluating CDCL variablescoring schemes. In Theory and Applications of Satisfiability Testing–SAT 2015. Springer. 405–422.Biere, A.; Cimatti, A.; Clarke, E. M.; Strichman, O.; andZhu, Y. 2003. Bounded model checking. Advances in computers 58:117–148.Biere, A. 2010. Lingeling, plingeling, picosat and precosatat SAT race 2010. FMV Report Series Technical Report10(1).Cadar, C.; Ganesh, V.; Pawlowski, P. M.; Dill, D.

L.; andEngler, D. R. 2008. EXE: automatically generating inputsof death. ACM Transactions on Information and System Security (TISSEC) 12(2):10.Chen, J. 2014. Minisat blbd. In Proceedings of SAT Competition 2014, volume B-2014-2, 45. University of Helsinki.Goldberg, E., and Novikov, Y. 2007. BerkMin: A fastand robust SAT-solver. Discrete Applied Mathematics155(12):1549–1561.Jeroslow, R.

G., and Wang, J. 1990. Solving propositionalsatisfiability problems. Annals of mathematics and ArtificialIntelligence 1(1-4):167–187.Katebi, H.; Sakallah, K. A.; and Marques-Silva, J. P. 2011.Empirical study of the anatomy of modern SAT solvers. InTheory and Applications of Satisfiability Testing-SAT 2011.Springer.

343–356.Lagoudakis, M. G., and Littman, M. L. 2001. Learning toselect branching rules in the DPLL procedure for satisfiability. Electronic Notes in Discrete Mathematics 9:344–359.Liang, J. H.; Ganesh, V.; Zulkoski, E.; Zaman, A.; and Czarnecki, K. 2015. Understanding VSIDS branching heuristicsin conflict-driven clause-learning SAT solvers. In Hardwareand Software: Verification and Testing. Springer. 225–241.Marques-Silva, J.

P., and Sakallah, K. 1999. GRASP: Asearch algorithm for propositional satisfiability. Computers,IEEE Transactions on 48(5):506–521.Marques-Silva, J. P. 1999. The impact of branching heuristics in propositional satisfiability algorithms. In Progress inArtificial Intelligence. Springer. 62–74.Mironov, I., and Zhang, L. 2006. Applications of SATsolvers to cryptanalysis of hash functions. In Theory and Applications of Satisfiability Testing-SAT 2006. Springer.

102–115.Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; andMalik, S. 2001. Chaff: Engineering an efficient SAT solver.In Proceedings of the 38th annual Design Automation Conference, 530–535. ACM.Rintanen, J. 2009. Planning and SAT. Handbook of Satisfiability 185:483–504.Soos, M. 2010. Cryptominisat 2.5.0. SAT Race.Sorensson, N., and Een, N. 2005. MiniSat v1.13-a SATsolver with conflict-clause minimization.

SAT 2005:53.Stump, A.; Sutcliffe, G.; and Tinelli, C. 2014. StarExec: across-community infrastructure for logic solving. In Automated Reasoning. Springer. 367–373.Sutton, R. S., and Barto, A. G. 1998. Reinforcement learning: An introduction, volume 1. MIT press Cambridge..

Характеристики

Список файлов лекций