  We present Graph-$Q$-SAT, a branching heuristic for a Boolean SAT solver
trained with value-based reinforcement learning (RL) using Graph Neural
Networks for function approximation. Solvers using Graph-$Q$-SAT are complete
SAT solvers that either provide a satisfying assignment or proof of
unsatisfiability, which is required for many SAT applications. The branching
heuristics commonly used in SAT solvers make poor decisions during their
warm-up period, whereas Graph-$Q$-SAT is trained to examine the structure of
the particular problem instance to make better decisions early in the search.
Training Graph-$Q$-SAT is data efficient and does not require elaborate dataset
preparation or feature engineering. We train Graph-$Q$-SAT using RL interfacing
with MiniSat solver and show that Graph-$Q$-SAT can reduce the number of
iterations required to solve SAT problems by 2-3X. Furthermore, it generalizes
to unsatisfiable SAT instances, as well as to problems with 5X more variables
than it was trained on. We show that for larger problems, reductions in the
number of iterations lead to wall clock time reductions, the ultimate goal when
designing heuristics. We also show positive zero-shot transfer behavior when
testing Graph-$Q$-SAT on a task family different from that used for training.
While more work is needed to apply Graph-$Q$-SAT to reduce wall clock time in
modern SAT solving settings, it is a compelling proof-of-concept showing that
RL equipped with Graph Neural Networks can learn a generalizable branching
heuristic for SAT search.
