Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning

Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee. Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning. In 8th International Conference on Learning Representations (ICLR), April 2020.

Download

[HTML] 

Abstract

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.

BibTeX

@inproceedings{lederman-iclr20,
  author    = {Gil Lederman and
               Markus N. Rabe and
               Sanjit Seshia and
               Edward A. Lee},
  title     = {Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning},
  booktitle = {8th International Conference on Learning Representations (ICLR)},
  year      = {2020},
  month     = {April},
  abstract  = {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. },
}