It is valuable yet remains challenging to apply neural networks in logical reasoning tasks. Despite some successes witnessed in learning SAT (Boolean Satisfiability) solvers for propositional logic via Graph Neural Networks (GNN), there haven't been any successes in learning solvers for more complex predicate logic. In this paper, we target the QBF (Quantified Boolean Formula) satisfiability problem, the complexity of which is in-between propositional logic and predicate logic, and investigate the feasibility of learning GNN-based solvers and GNN-based heuristics for the cases with a universal-existential quantifier alternation (so-called 2QBF problems). We conjecture, with empirical support, that GNNs have certain limitations in learning 2QBF solvers, primarily due to the inability to reason about a set of assignments. Then we show the potential of GNN-based heuristics in CEGAR-based solvers, and explore the interesting challenges to generalize them to larger problem instances. In summary, this paper provides a comprehensive surveying view of applying GNN-based embeddings to 2QBF problems, and aims to offer insights in applying machine learning tools to more complicated symbolic reasoning problems.
This paper explores how graph neural networks can be applied to test satisfiability of 2QBF logical formulas. They show that a straightforward extension of a GNN-based SAT solver to 2QBF fails to outperform random chance, and argue that this is because proving either satisfiability or unsatisfiability of 2QBF requires reasoning over exponential sets of assignments. Instead, they show that GNNs can be useful as a heuristic candidate- or counterexample- ranking model which improves the efficiency of the CEGAR algorithm for solving 2QBF.
This is a clear, well-written, and well-structured paper, and I support accepting it to ICLR. That being said, I am not as familiar with the literature on neural solvers for logic problems, so I base my review on the content within the paper more than its context in the field.
I can’t find much to fault with the writing and arguments. The GNN architecture for 2QBF (Section 2) is simple, elegant, and well-motivated as a minimal extension of successful SAT solvers. The arguments in Section 3 are convincing, and make a good case for why an algorithm such as CEGAR is necessary. Finally, the metrics in Section 4 are clearly interpretable and well-justified. 
A couple questions and concerns:
In Section 3, The amount of training data (up to 160 pairs of formulas for predicting satisfiability) seems to be very small for a machine learning problem. By comparison, Selsam et al. 2019 says they train their GNN SAT solver on “millions of problems” (Section 5). Is there a good reason for using a much smaller dataset, given that 2QBF is a harder class of problem?
Section 4.2: how are the TraunU, TrainS, TestU, and TestS datasets generated?
In Section 4.6, are the models re-trained on these new distributions, or on the data described in Section 4.2? (If the latter, how does the GNN perform if re-trained on the larger-spec data?)
And minor points on clarity:
* “-” for the baseline seems a bit awkward; consider spelling out “vanilla”?
* Are all the numbers in the tables iteration counts, unless specified otherwise? It would help to restate this in the captions. Similarly, I wonder if there could be more informative names for GNN1, GNN2, GNN3, and GNN4?