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.