Abstract

We demonstrate how to learn efficient heuristics for automated reasoningalgorithms through deep reinforcement learning. We focus on a backtrackingsearch algorithm for quantified Boolean logics, which can already solveformulas of impressive size - up to hundreds of thousands of variables. Themain challenge is to find a representation of these formulas that lends itselfto making predictions in a scalable way. For a family of challenging problems,we learned a heuristic that solves significantly more formulas compared to theexisting handwritten heuristics.

 

Quick Read (beta)