Improving SAT Solver Heuristics with Graph Networks and Reinforcement Learning

A BSTRACT We present GQSA T, a branching heuristic in a Boolean SA T solver trained with value-based reinforcement learning (RL) using Graph Neural Networks for function approximation. Solvers using GQSA T are complete SA T solvers that either provide a satisfying assignment or a proof of unsatisfiability, which is required for many SA T applications. The branching heuristic commonly used in SA T solvers today suffers from bad decisions during their warm-up period, whereas GQSA T has been trained to examine the structure of the particular problem instance to make better decisions at the beginning of the search. Training GQSA T is data efficient and does not require elaborate dataset preparation or feature engineering to train. We train GQSA T on small SA T problems using RL interfacing with an existing SA T solver. We show that GQSA T is able to reduce the number of iterations required to solve SA T problems by 2-3X, and it generalizes to unsatisfiable SA T instances, as well as to problems with 5X more variables than it was trained on. We also show that, to a lesser extent, it generalizes to SA T problems from different domains by evaluating it on graph coloring. Our experiments show that augmenting SA T solvers with agents trained with RL and graph neural networks can improve performance on the SA T search problem. 1 I NTRODUCTION Boolean satisfiability (SA T) is an important problem for both industry and academia impacting various fields, including circuit design, computer security, artificial intelligence, automatic theorem proving, and combinatorial optimization. As a result, modern SA T solvers are well-crafted, sophisticated, reliable pieces of software that can scale to problems with hundreds of thousands of variables (Ohrimenko et al., 2009). SA T is known to be NPcomplete (Karp, 1972), and most state-of-the-art open-source and commercial solvers rely on multiple heuristics to speed up the exhaustive search, which is otherwise intractable. These heuristics are usually meticulously crafted using expert domain knowledge and are often iterated on using trial and error. In this paper, we investigate how we can use machine learning to improve upon an existing branching heuristic without leveraging domain expertise.