In this talk we propose a framework for viewing solver branching heuristics as optimization algorithms where the objective is to maximize the learning rate, defined as the propensity for variables to generate learnt clauses. By viewing online variable selection in SAT solvers as an optimization problem, we can leverage a wide variety of optimization algorithms, especially from machine learning, to design effective branching heuristics. In particular, we model the variable selection optimization problem as an online multi-armed bandit, a special-case of reinforcement learning, to learn branching variables such that the learning rate of the solver is maximized. Based on the above modeling, we develop a branching heuristic that we call learning rate branching or LRB, based on a well-known multi-armed bandit algorithm called exponential recency weighted average (a form of EMA) and implement it as part of MiniSat and CryptoMiniSat. The LRB branching heuristic is shown to be significantly faster than the VSIDS and other leading branching heuristics on 1975 application and hard combinatorial instances from 2009 to 2014 SAT Competitions. We also show that CryptoMiniSat with LRB solves more instances than the one with VSIDS. To the best of our knowledge, the VSIDS branching heuristic and its variants have been the dominant class of such heuristics for SAT solvers since 2001, until we introduced a novel class of machine-learning based branching heuristics.

Vijay Ganesh Brief Bio

Website: https://ece.uwaterloo.ca/~vganesh

Dr. Vijay Ganesh is an assistant professor at the University of Waterloo since 2012. Prior to that he was a research scientist at MIT, and completed his PhD in computer science from Stanford University in 2007.

Vijay's primary area of research is the theory and practice of automated reasoning aimed at software engineering, formal methods, security, and mathematics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, The Z3 string solver, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of theories over string equations and integers. For his research, he recently won the Early Researcher Award (ERA) in 2016, an IBM Research Faculty Award in 2015, Google Research Faculty Awards in 2013 and 2011, and 7 best paper awards/honors at conferences like CAV, IJCAI, CADE, ISSTA, SAT, SPLC, and DATE (including a Ten-Year Most Influential Award @ DATE 2008). His solvers STP and MapleSAT have won numerous awards at the highly competitive international SMT and SAT solver competitions. Recently he was invited to the first Heidelberg Laureate Forum in 2013, a gathering where young researchers from around the world were selected to meet with Turing, Fields and Abel Laureates.