Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning

Edward A. Lee
Gil Lederman
Markus Rabe
Sanjit A. Seshia
Proceedings of ICLR(2020) (to appear)
Google Scholar

Abstract

We demonstrate how to learn efficient heuristics for automated reasoning algorithms
through deep reinforcement learning. We consider search algorithms for
quantified Boolean logics, that already can solve formulas of impressive size - up
to 100s of thousands of variables. The main challenge is to find a representation
which lends to making predictions in a scalable way. The heuristics learned
through our approach significantly improve over the handwritten heuristics for
several sets of formulas.