  In this paper, we investigate the feasibility of learning GNN (Graph Neural
Network) based solvers and GNN-based heuristics for specified QBF (Quantified
Boolean Formula) problems. We design and evaluate several GNN architectures for
2QBF formulae, and conjecture that GNN has limitations in learning 2QBF
solvers. Then we show how to learn a heuristic CEGAR 2QBF solver. We further
explore generalizing GNN-based heuristics to larger unseen instances, and
uncover some interesting challenges. In summary, this paper provides a
comprehensive surveying view of applying GNN-embeddings to specified QBF
solvers, and aims to offer guidance in applying ML to more complicated symbolic
reasoning problems.
