Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning
This work addresses the challenge of scalable automated reasoning for quantified Boolean formulas, which is important for applications in formal verification and AI planning, though it appears incremental as it builds on existing backtracking search algorithms.
The authors tackled the problem of learning efficient heuristics for automated reasoning algorithms for quantified Boolean formulas using deep reinforcement learning, resulting in a heuristic that solves significantly more formulas compared to existing handwritten heuristics for a family of challenging problems.
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.