# Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?

arXiv: https://arxiv.org/abs/1909.11830 · HTML: https://mlsanity.com/paper/1909.11830/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Sep 2019.

## Built on by (most cited first, 10 of 10)

- [The Threat of Offensive AI to Organizations](https://mlsanity.com/paper/2106.15764/) (2021)
- [Generalization of Neural Combinatorial Solvers Through the Lens of Adversarial Robustness](https://mlsanity.com/paper/2110.10942/) (2021)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [Augment with Care: Contrastive Learning for Combinatorial Problems](https://mlsanity.com/paper/2202.08396/) (2022)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [Reinforcement Learning Based Query Vertex Ordering Model for Subgraph Matching](https://mlsanity.com/paper/2201.11251/) (2022)
- [General Method for Solving Four Types of SAT Problems](https://mlsanity.com/paper/2312.16423/) (2023)
- [Zero Training Overhead Portfolios for Learning to Solve Combinatorial Problems](https://mlsanity.com/paper/2102.03002/) (2021)
- [A Reinforcement Learning based Reset Policy for CDCL SAT Solvers](https://mlsanity.com/paper/2404.03753/) (2024)
- [Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)](https://mlsanity.com/paper/2411.15194/) (2024)

## Abstract (arXiv)

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.