Abstract

We demonstrate how to learn efficient heuristics for automated reasoningalgorithms for quantified Boolean formulas through deep reinforcement learning.We focus on a backtracking search algorithm, which can already solve formulasof impressive size - up to hundreds of thousands of variables. The mainchallenge is to find a representation of these formulas that lends itself tomaking predictions in a scalable way. For a family of challenging problems, welearned a heuristic that solves significantly more formulas compared to theexisting handwritten heuristics.

 

Quick Read (beta)