We demonstrate how to learn efficient heuristics for automated reasoning algorithms through deep reinforcement learning. We focus on backtracking search algorithms for quantified Boolean logics, which already can solve formulas of impressive size - up to 100s 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 challenging problems, the heuristic learned through our approach reduces execution time by a factor of 10 compared to the existing handwritten heuristics.
RL finds better heuristics for automated reasoning algorithms. Aims to learn a heuristic for a backtracking search algorithm utilizing Reinforcement learning and proposes a model that makes use of Graphical Neural Networks to produce literal and clauses embedding, and use them to predict the quality of each literal to decide the probability of each action. The paper proposes an approach to automatically learning variable selection heuristics for QBF using deep learning