We demonstrate how to learn efficient heuristics for automated reasoning algorithms through deep reinforcement learning. We focus on backtracking search algorithms for quantified Boolean logics, which already can solve formulas of impressive size - up to 100s of thousands of variables. The main challenge is to find a representation of these formulas that lends itself to making predictions in a scalable way. For challenging problems, the heuristic learned through our approach reduces execution time by a factor of 10 compared to the existing handwritten heuristics. Automated reasoning and machine learning have both made tremendous progress over the last decades. Automated reasoning algorithms are now able to solve challenging logical problems that once seemed intractable, and today are used in industry for the verification of hardware and software systems. At the core of this progress are logic solvers for Boolean Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and recently also Quantified Boolean Formulas (QBF). These solvers rely on advanced backtracking search algorithms, such as conflict-driven clause learning (CDCL) BID30 , to solve formulas with thousands or even millions of variables. Many automated reasoning algorithms are not only able to answer challenging queries, but also to explain their answer by providing detailed mathematical proofs. However, when problems lack a formal semantics automated reasoning algorithms are hard to apply, and they tend to scale poorly for problems involving uncertainty (e.g. in form of probabilities).Machine learning, on the other hand, recently experienced several breakthroughs in object recognition, machine translation, board games, and language understanding. At the heart of the recent progress in machine learning lie optimization algorithms that train deep and overparameterized models on large amounts of data. The resulting models generalize to unseen inputs and can generally deal well with uncertainty. However, the predictions made by learned models are often hard to explain and hard to restrict to safe behaviors.The complementary strengths of machine learning and automated reasoning raise the question how the methods of the two fields can be combined. In this paper we study how neural networks can be employed within automated reasoning algorithms. We discuss the unique challenges that arise in applying neural networks to vast logical formulas and how reinforcement learning can be used to learn better heuristics for backtracking search algorithms.Backtracking search algorithms in automated reasoning are highly nondeterministic: at many points in their execution there are multiple options for how to proceed. These choices have a big impact on performance; in fact we often see that some problems cannot be solved within hours of computation that under different heuristics are solved within milliseconds. The most prominent heuristic choice in CDCL-style search algorithms is the variable selection heuristic, which is to select a variable (and which value to assign to that variable). Until today, Variable State Independent Decaying Sum (VSIDS) BID33 and its variants are used as the variable selection heuristic in some of the most competitive SAT solvers BID4 Soos, 2014; BID2 and QBF solvers BID28 BID36 . Even small improvements over VSIDS, such as the recent introduction of learning rate branching BID27 , are highly interesting for the automated reasoning community.Designing heuristics for backtracking search algorithms is often counter-intuitive: For example, it is well-known that heuristics that aim to find a correct solution perform worse than heuristics that aim to quickly cause a conflict (i.e. reach a dead-end in the search tree). This is because running into a conflict allows us to apply clause learning, a process that (deductively) derives a new constraint that prevents running into the similar conflicts again. This can cut off an exponential number of branches and can therefore save a lot of computation time in the future. Heuristics for search algorithms are an interesting target for machine learning with immediate impact in verification.The Problem We want to learn a heuristic for a backtracking search algorithm such that it solves more formulas in less time. We view this as a reinforcement learning problem where we are given a formula from some distribution of formulas, and we run the backtracking search algorithm until it reaches a decision point and then query the neural network to predict an action. We iterate this process until termination (at which point the formula is proven or refuted) or a time limit is reached. The input to the neural network is thus the current state of the algorithm, including the formula, and we reward it for reaching termination quickly.In this work, we focus on learning heuristics for the solver CADET BID36 BID38 . CADET is a competitive solver for QBF formulas with the quantifier prefix ∀X ∃Y , which covers most of the known applications of QBF. For all purposes of this work, we can assume the algorithm works exactly like a SAT solver. The heuristic we address in this work is the variable selection heuristic.Challenges The setting comes with several unique challenges:Size: While typical reinforcement learning settings have a small, fixed-size input (a Go board or an Atari screen), the formulas that we consider have hundreds of variables and thousands of clauses, each with several data points. All variables appear both as part of the state and as actions in the reinforcement learning environment. At the same time, the size of the formulas varies dramatically (from tens of variables up to 700k variables) and is hardly correlated with their 'difficulty' -while some of the largest formulas can be solved with little effort, some of the formulas with only 100 variables cannot be solved by any modern QBF solver. We presented an approach to improve the heuristics of a backtracking search algorithm for Boolean logic through deep reinforcement learning. The setting is new and challenging to reinforcement learning, featuring an unbounded input-size and action space, a connection between the length of episodes and rewards. We demonstrate that these problems can be overcome, and learn a heuristic that reduces the overall execution time of a competitive QBF solver by a factor of 10 after training on similar formulas.We believe that this work motivates more aggressive research efforts in the area and will lead to a significant improvement in the performance of logic solvers. Our experiments uncover particu-lar challenges to be addressed in the future. The transfer of the learned insights between different sets of formulas is still limited, learning from long episodes seems to be challenging, andcounterintuitively-it does not seem to help to consider multiple iterations of the GNN.14. Number of successful propagation steps indicates whether the variable is universally quantified, DISPLAYFORM0 indicates whether the variable is existentially quantified, y 2 ∈ {0, 1}indicates whether the variable has a Skolem function already, y 3 ∈ {0, 1} indicates whether the variable was assigned constant True, y 4 ∈ {0, 1} indicates whether the variable was assigned constant False, DISPLAYFORM1 indicates whether the variable was decided positive, y 6 ∈ {0, 1} indicates whether the variable was decided negative, and DISPLAYFORM2 indicates the activity level of the variable. There is no way to assign variables strings as names. The reasoning behind this decision is that this format is only meant to be used for the computational backend.
RL finds better heuristics for automated reasoning algorithms. Aims to learn a heuristic for a backtracking search algorithm utilizing Reinforcement learning and proposes a model that makes use of Graphical Neural Networks to produce literal and clauses embedding, and use them to predict the quality of each literal to decide the probability of each action. The paper proposes an approach to automatically learning variable selection heuristics for QBF using deep learning