# Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning

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

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Jul 2018.

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

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Augment with Care: Contrastive Learning for Combinatorial Problems](https://mlsanity.com/paper/2202.08396/) (2022)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [Simplifying Polylogarithms with Machine Learning](https://mlsanity.com/paper/2206.04115/) (2022)
- [Train on Small, Play the Large: Scaling Up Board Games with AlphaZero and GNN](https://mlsanity.com/paper/2107.08387/) (2021)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Can Graph Neural Networks Learn to Solve MaxSAT Problem?](https://mlsanity.com/paper/2111.07568/) (2021)
- [UNSAT Solver Synthesis via Monte Carlo Forest Search](https://mlsanity.com/paper/2211.12581/) (2022)
- [Pretrained Cost Model for Distributed Constraint Optimization Problems](https://mlsanity.com/paper/2112.04187/) (2021)
- [Unveiling the Limits of Learned Local Search Heuristics: Are You the Mightiest of the Meek?](https://mlsanity.com/paper/2310.19990/) (2023)
- [Learning Better Representations From Less Data For Propositional Satisfiability](https://mlsanity.com/paper/2402.08365/) (2024)
- [Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning](https://mlsanity.com/paper/2107.09766/) (2021)

## Abstract (arXiv)

We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking search algorithm, which can already solve formulas of impressive size - up to hundreds 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 a family of challenging problems, we learned a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.