Learning Rate Based Branching Heuristic for SAT Solvers (Презентации лекций), страница 5

We plan to explore a mathematicalmodel where the branching heuristic is an inductive engine (machine learning), and the conflict analysis is a deductive feedback mechanism. Such amodel could enable us to prove complexity theoretic results that at long lastmight explain why CDCL SAT solvers are so efficient for industrial instances.Contribution II: We chose MAB as the optimization method in this paper,but many other optimization techniques can be applied to optimize LR.

Themost natural extension to our work here is to incorporate the internal state ofthe solver and apply stateful reinforcement learning. The state, for example,could be the current community the solver is focused on and exploiting thisinformation could improve the locality of the branching heuristic [20].Contribution III: We based LRB on one MAB algorithm, ERWA, due to itslow computational overhead. The literature of multi-armed bandits is veryrich, and provides many alternative algorithms with a wide spectrum ofcharacteristics and assumptions. It is fruitful to explore the MAB literatureto determine the best algorithm for branching in CDCL SAT solvers.Finally, as our experimental results suggest, the line of research we have juststarted exploring, namely, branching heuristics as machine learning algorithms(and branching as an optimization problem) has already shown considerableimprovement over previous state-of-the-art branching heuristics such as VSIDSand CHB, and affords a rich design space of heuristics to explore in the future.References[1] Ansótegui, C., Giráldez-Cru, J., Levy, J.: Theory and Applications of SatisfiabilityTesting – SAT 2012: 15th International Conference, Trento, Italy, June 17-20,2012.

Proceedings, chap. The Community Structure of SAT Formulas, pp. 410–423. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)[2] Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SATSolvers. In: Proceedings of the 21st International Jont Conference on Artifical Intelligence. pp. 399–404.

IJCAI’09, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2009)[3] Audemard, G., Simon, L.: Refining Restarts Strategies for SAT and UNSAT. In:Proceedings of the 18th International Conference on Principles and Practice ofConstraint Programming. pp. 118–126. CP’12, Springer-Verlag, Berlin, Heidelberg(2012)[4] Audemard, G., Simon, L.: Glucose 2.3 in the SAT 2013 Competition.

In: Proceedings of SAT Competition 2013. pp. 42–43 (2013)[5] Biere, A.: Theory and Applications of Satisfiability Testing – SAT 2008: 11thInternational Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, chap. Adaptive Restart Strategies for Conflict Driven SAT Solvers, pp.28–33. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)[6] Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMVReport Series Technical Report 10(1) (2010)[7] Biere, A., Fröhlich, A.: Theory and Applications of Satisfiability Testing – SAT2015: 18th International Conference, Austin, TX, USA, September 24-27, 2015,Proceedings, chap. Evaluating CDCL Variable Scoring Schemes, pp.

405–422.Springer International Publishing, Cham (2015)[8] Brown, R.G.: Exponential Smoothing for Predicting Demand. In: Operations Research. vol. 5, pp. 145–145 (1957)[9] Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically Generating Inputs of Death. In: Proceedings of the 13th ACM Conferenceon Computer and Communications Security. pp. 322–335. CCS ’06, ACM, NewYork, NY, USA (2006)[10] Carvalho, E., Marques-Silva, J.P.: Using Rewarding Mechanisms for ImprovingBranching Heuristics.

In: Proceedings of the Seventh International Conference onTheory and Applications of Satisfiability Testing (2004)[11] Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Form. Methods Syst. Des. 19(1), 7–34 (2001)[12] Eén, N., Sörensson, N.: Theory and Applications of Satisfiability Testing: 6thInternational Conference, SAT 2003, Santa Margherita Ligure, Italy, May 5-8,2003, Selected Revised Papers, chap. An Extensible SAT-solver, pp.

502–518.Springer Berlin Heidelberg, Berlin, Heidelberg (2004)[13] Erev, I., Roth, A.E.: Predicting How People Play Games: Reinforcement Learning in Experimental Games with Unique, Mixed Strategy Equilibria. AmericanEconomic Review 88(4), 848–881 (1998)[14] Fröhlich, A., Biere, A., Wintersteiger, C., Hamadi, Y.: Stochastic Local Searchfor Satisfiability Modulo Theories.

In: Proceedings of the Twenty-Ninth AAAIConference on Artificial Intelligence. pp. 1136–1143. AAAI’15, AAAI Press (2015)[15] Gershman, R., Strichman, O.: Hardware and Software, Verification and Testing:First International Haifa Verification Conference, Haifa, Israel, November 13-16,2005, Revised Selected Papers, chap. HaifaSat: A New Robust SAT Solver, pp.76–89. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)[16] Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust Sat-solver. Discrete Appl.Math. 155(12), 1549–1561 (Jun 2007)[17] Jeroslow, R.G., Wang, J.: Solving Propositional Satisfiability Problems.

Annalsof Mathematics and Artificial Intelligence 1(1-4), 167–187 (Sep 1990)[18] Lagoudakis, M.G., Littman, M.L.: Learning to Select Branching Rules in theDPLL Procedure for Satisfiability. Electronic Notes in Discrete Mathematics 9,344–359 (2001)[19] Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential RecencyWeighted Average Branching Heuristic for SAT Solvers. In: Proceedings of AAAI16 (2016)[20] Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: UnderstandingVSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers.

In:Hardware and Software: Verification and Testing, pp. 225–241. Springer (2015)[21] Loth, M., Sebag, M., Hamadi, Y., Schoenauer, M.: Principles and Practice of Constraint Programming: 19th International Conference, CP 2013, Uppsala, Sweden,September 16-20, 2013. Proceedings, chap. Bandit-Based Search for ConstraintProgramming, pp. 464–480. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)[22] Marques-Silva, J.P.: The Impact of Branching Heuristics in Propositional Satisfiability Algorithms. In: Proceedings of the 9th Portuguese Conference on ArtificialIntelligence: Progress in Artificial Intelligence. pp. 62–74.

EPIA ’99, SpringerVerlag, London, UK, UK (1999)[23] Marques-Silva, J.P., Sakallah, K.A.: GRASP-A New Search Algorithm for Satisfiability. In: Proceedings of the 1996 IEEE/ACM International Conference onComputer-aided Design. pp. 220–227. ICCAD ’96, IEEE Computer Society, Washington, DC, USA (1996)[24] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Annual Design Automation Conference. pp.

530–535. DAC ’01, ACM, New York, NY, USA (2001)[25] Newsham, Z., Ganesh, V., Fischmeister, S., Audemard, G., Simon, L.: Impact ofCommunity Structure on SAT Solver Performance. In: Theory and Applicationsof Satisfiability Testing–SAT 2014, pp. 252–268. Springer (2014)[26] Pipatsrisawat, K., Darwiche, A.: A Lightweight Component Caching Scheme forSatisfiability Solvers. In: Proceedings of the 10th International Conference onTheory and Applications of Satisfiability Testing. pp. 294–299. SAT’07, SpringerVerlag, Berlin, Heidelberg (2007)[27] Rintanen, J.: Planning and SAT.

Handbook of Satisfiability 185, 483–504 (2009)[28] Ryan, L.: Efficient Algorithms for Clause-Learning SAT Solvers. Master’s thesis,Simon Fraser University (2004)[29] Soos, M.: CryptoMiniSat v4. SAT Competition p. 23 (2014)[30] Stump, A., Sutcliffe, G., Tinelli, C.: Automated Reasoning: 7th International JointConference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL2014, Vienna, Austria, July 19-22, 2014. Proceedings, chap. StarExec: A CrossCommunity Infrastructure for Logic Solving, pp. 367–373. Springer InternationalPublishing, Cham (2014)[31] Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, vol. 1.

MITpress Cambridge (1998)[32] Yechiam, E., Busemeyer, J.R.: Comparison of basic assumptions embedded inlearning models for experience-based decision making. Psychonomic Bulletin &Review 12(3), 387–402[33] Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient ConflictDriven Learning in a Boolean Satisfiability Solver. In: Proceedings of the 2001IEEE/ACM International Conference on Computer-aided Design. pp. 279–285.ICCAD ’01, IEEE Press, Piscataway, NJ, USA (2001).