February 1, 2019
There has been progress in applying machine learning techniques to symbolic reasoning (such as SAT, QBF, and SMT solving), showing various approaches to combine the power of stochastic op- timization with symbolic decision procedures. In this paper, we investigate the feasibility of learn- ing GNN (Graph Neural Network) based solvers and GNN-based heuristics for 2QBF (Quantified Boolean Formula) problems. We design and evaluate several GNN architectures for 2QBF formu- lae, and conjecture with empirical support that GNN has certain limitations in learning 2QBF solvers, primarily due to the inability to reason about ∀ quantifiers or to prove unsatisfiability of SAT problems. We then show success in learning heuristics for a CEGAR-based 2QBF solver, and compare our learned heuristics with known MaxSAT based heuristics. We further explore generalizing GNN-based heuristics to larger unseen instances, and uncover interesting challenges in generalization across graph structures. In summary, this paper provides a comprehensive sur- veying view of applying GNN-embeddings to 2QBF solvers, and aims to offer guidance in apply- ing ML to more complicated symbolic reasoning problems.