Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning
arXiv:1807.08058
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.
References in corpus (12)
- Efficient Estimation of Word Representations in Vector Space
- Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling
- Learning Combinatorial Optimization Algorithms over Graphs
- Layer Normalization
- Learning a SAT Solver from Single-Bit Supervision
- Solving QBF with Counterexample Guided Refinement
- Solving QBF by Clause Selection
- GamePad: A Learning Environment for Theorem Proving
- Can Neural Networks Understand Logical Entailment?
- Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
- Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers
- On Expansion and Resolution in CEGAR Based QBF Solving