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.
@article{arxiv.1807.08058,
title = {Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning},
author = {Gil Lederman and Markus N. Rabe and Edward A. Lee and Sanjit A. Seshia},
journal= {arXiv preprint arXiv:1807.08058},
year = {2019}
}