Title: GRAPH NEURAL NETWORKS FOR REASONING 2-QUANTIFIED BOOLEAN FORMULAS

Abstract: 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.
GNN Architecture for Embedding SAT formulas. Previous success (Selsam et al., 2019) of GNN-based SAT solvers embedded SAT formulas like below. Each SAT formula is translated into a bipartite graph, where one kind of nodes represent all literals (Boolean variables and their negations, denoted as L) , and the other kind of nodes represent all clauses (sets of literals that are connected

1. INTRODUCTION:

As deep learning makes astonishing achievements in the domain of image (He et al., 2016) and audio (Hannun et al., 2014) processing, natural languages (Vaswani et al., 2017) , and discrete heuristics decisions in games (Silver et al., 2017) , there is a profound interest in applying the relevant techniques in the field of logical reasoning. Logical reasoning problems span from simple propositional logic to complex predicate logic and high-order logic, with known theoretical complexities from NP-complete (Cook, 1971) to semi-decidable and undecidable (Church, 1936) . Testing the ability and limitation of machine learning tools on logical reasoning problems leads to a fundamental understanding of the boundary of learnability and robust AI, and addresses the interesting questions in decision procedures in logic, symbolic reasoning, and program analysis and verification as defined in the programming language community.

There have been some successes in learning propositional logic reasoning (Selsam et al., 2019; Amizadeh et al., 2019) , which focus on SAT (Boolean Satisfiability) problems as defined below. A propositional logic formula is an expression composed of Boolean constants ( : true, ⊥ : false) , Boolean variables (x i ), and propositional connectives such as ∧, ∨, ¬ (for example (x 1 ∨ ¬x 2 ) ∧ (¬x 1 ∨ x 2 )). The SAT problem asks if a given formula can be satisfied (evaluated to ) by assigning proper Boolean values to the variables. A crucial feature of the logical reasoning domain (as is visible in the SAT problem) is that the inputs are often structural, where logical connections between entities (variables in SAT problems) are the key information. Accordingly, previous successes have used GNN (Graph Neural Networks) and message-passing based embeddings to solve SAT problems.

However, it should be noted that logical decision procedures is more complex that just reading the formulas correctly. It is unclear if GNN embeddings (via simple message-passing) contain all the information needed to reason about complex logical questions on top of the graph structures derived from the formulas, or whether the complex embedding schemes can be learned from backpropagation. Previous successes on SAT problems argued for the power of GNN, which can handle NP-complete problems (Selsam et al., 2019; Amizadeh et al., 2019) , but no successes have been reported for solving semi-decidable predicate logic problems via GNN. In order to find out where the limitation of GNN is and why, in learning logical reasoning problems, we decide to look at problems with complexity inbetween SAT and predicate logic problems, for which QBF (Quantified Boolean Formula) problems serve as excellent middle steps. QBF is an extension of propositional formula, which allows quantifiers (∀ and ∃) over the Boolean variables (such as ∀x 1 ∃x 2 . (x 1 ∨ ¬x 2 ) ∧ (¬x 1 ∨ x 2 )). In general, a quantified Boolean formula in prenex normal form can be expressed as such:

Q i X i Q i-1 X i-1 ...Q 0 X 0 . φ

where Q i are quantifiers that always differ from their neighboring quantifiers, X i are disjoint sets of Boolean variables, and φ is a propositional formula with all Boolean variables bounded in Q i . Complexity-wise, QBF problems are PSPACE-complete (Kleine Büning & Bubeck, 2009) , which lies in-between the NP-completeness of SAT problems and the semi-decidability of predicate logic problems. Furthermore, 2-QBF (QBF with only two alternative quantifiers) is Σ P 2 -complete (Kleine Büning & Bubeck, 2009) .

Another direction of addressing logical reasoning problems via machine learning is to learn heuristic decisions within traditional decision procedures. This direction is less appealing from a theoretical perspective, but more interesting from a practical one, since it has been shown to speed up SAT solvers in practical settings (Selsam & Bjørner, 2019) . In this direction, there is less concern about the embedding power of GNN, but more about the design of the training procedures (what is the data and label for training) and how to incorporate the trained models within the decision procedures. The embeddings captured via GNN is rather preferred to be lossy to prevent overfitting (Selsam & Bjørner, 2019) .

In this paper we explore the potential applications of GNNs to 2QBF problems. In Section 2, we illustrate our designs of GNN architectures for embedding 2QBF formulas. In Section 3, we evaluate GNN-based 2QBF solvers, and conjecture with empirical evidences that the current GNN techniques are unable to learn complete SAT solvers or 2QBF solvers. In Section 4, we demonstrate the potential of our GNN-based heuristics for selecting candidates and counter-examples in the CEGAR-based solver framework. In Section 5, we discuss the related work and conclude in Section 6. Throughout the paper we redirect details to supplementary materials.

We make the following contributions:

1. Design and test possible GNN architectures for embedding 2QBF. 2. Pinpoint the limitation of GNN in learning logical decision procedures that need reasoning about a space of Boolean assignments. 3. Learn GNN-based CEGAR solver heuristics via supervised learning and uncover interesting challenges for GNN to generalize across graph structures.

2. GNN EMBEDDING OF PROPOSITIONAL LOGICAL FORMULAS:

Preliminary: Graph Neural Networks. GNNs refer to the neural architectures devised to learn the embeddings of nodes and graphs via message-passing. Resembling the generic definition in Xu et al. (2019) , they consist of two successive operators to propagate the messages and evolve the embeddings over iterations:

m (k) v =Aggregate (k) {h (k-1) u : u ∈ N (v)} , h (k) v =Combine (k) h (k-1) v , m (k) v (1)

where h

(k) v

denotes the hidden state (embedding) of node v at the k th layer/iteration, and N (v) denotes the neighbors of node v. In each iteration, the Aggregate (k) (•) aggregates hidden states from node v's neighbors to produce the new message (i.e., m (k) v ) for node v, and Combine (k) (•, •) computes the new embedding of v with its last state and its current message. After a specific number of iterations (e.g., K), the embeddings should capture the global relational information of the nodes, which can be fed into other neural network modules for specific tasks. via ∨, denoted as C). Edges between literal and clause nodes represent the literal appearing in that clause, and all edges are represented by a sparse adjacent matrix (EdgeMatrix (E)) of dimension |C| × |L|. There is also another kind of edges connecting literals with their negations. The graph representation of (x 1 ∨ ¬x 2 ) ∧ (¬x 1 ∨ x 2 ) is given below as an example. Note that this architecture is specific for propositional formulas in Conjunctive Normal Form (CNF), which is composed of clauses connected via ∧.

C 1 C 2 x 1 x 2 ¬x 1 ¬x 2

The embeddings of literals and clauses are initialized with tiled random vectors. Then the GNN uses MLPs to compute the messages of literals and clauses from the embeddings, and LSTMs to update embeddings with the aggregated messages. The mathematical process for one iteration of message-passing is given below, where Emb L and Emb C denotes embedding matrices of literals and clauses respectively, Msg X→Y denotes messages from X to Y , MLP X denotes MLPs of X for generating messages from the embeddings, LSTM X denotes LSTMs of X for digesting incoming messages and updating the embeddings, and • T [] represent matrix multiplication, transposition, and concatenation respectively. Furthermore, Emb ¬L denotes a permutational view of Emb L such that the same row of Emb L and Emb ¬L are embeddings of a variable and its negation respectively.

EQUATION

Note that different instances of MLPs and LSTMs are used for clauses and literals (they have different subscripts). What's more, Emb ¬L is used as additional message when updating Emb L .

GNN Architectures for Embedding 2QBF. The difference between SAT formulas and 2QBF is that in 2QBF the variables are quantified by ∀ or ∃. To reflect that difference in graph representation, we separate ∀-literals and ∃-literals into different groups of nodes. For example, the graph representation of ∀x

1 ∃x 2 . (x 1 ∨ ¬x 2 ) ∧ (¬x 1 ∨ x 2 ) is shown below: C 1 C 2 x 1 ¬x 1 x 2 ¬x 2

Accordingly, in GNN architectures, the separated ∀-literals and ∃-literals are embedded via different modules. The GNN architecture design closely resembles the design philosophy of Selsam et al. (2019) in terms of permutation invariance and negation invariance, and would most likely carry over the success of GNN in solving SAT problems to 2QBF problems.

EQUATION

Note that we use ∀ and ∃ to denote all ∀-literals and all ∃-literals respectively. We use E X to denote the EdgeMatrix between X and C, and MLP C→X to denote MLPs that generate Msg C→X . We de facto have tested more GNN architectures for 2QBF (see the supplementary material A.1), yet the model above performed the best in our later evaluation, so we used it in the main paper.

3. GNN-BASED SOLVERS FAIL IN 2QBF PROBLEMS:

In the previous section, we have discussed GNN-based embeddings in propositional logical formulas.

We then test whether GNN-based 2QBF solvers can be learned, following the previous successes (Selsam et al., 2019; Amizadeh et al., 2019) .

3.1. EMPIRICAL STUDY FOR REASONING 2QBF BY GNN:

Data Preparation. In training and testing, we follow the previous work (Chen & Interian, 2005) to generate random 2QBF formulas of specs (2,3) and sizes (8,10). That is to say, each clause has 5 literals, 2 of them are randomly chosen from a set of 8 ∀-quantified variables, and 3 of them are randomly chosen from a set of 10 ∃-quantified variables. We modify the generation procedure so that it generates clauses until the formula becomes unsatisfiable. We then randomly negate an ∃-quantified literal per formula to get a very similar but satisfiable formula.

Predicting Satisfiability. We first tested whether our graph embeddings can be used to predict satisfiability of 2QBF formulas. We extended the GNN architectures with a voting MLP (MLP vote ) that takes the embeddings of the ∀-variables after the propagation, and uses the average votes as logits for satisfiability/unsatisfiability prediction:

logits sat = mean(MLP vote (Emb ∀ ))

We trained our GNNs with different amount of data (40 pairs, 80 pairs, and 160 pairs of satisfiable/unsatisfiable formulas) and different numbers of message-passing iterations (8 iters, 16 iters, and 32 iters), and then evaluated the converged models on 600 pairs of new instances. We report the accuracy rate of unsatisfiable and satisfiable formulas as tuples for both the training dataset and the testing dataset. By alternating the random seeds, the models with the best training data performance are selected and shown in Table 1 . Since pairs of satisfiable/unsatisfiable formulas are only different by one literal, it forces the GNNs to learn subtle structural differences in the formulas. The GNNs fit well to the smaller training dataset but have trouble for 160 pairs of formulas (numbers in the green color). Performances of the models on testing dataset are close to random guesses (numbers in the blue color), and running more iterations during testing does not help with their performances.

Predicting Unsatisfiability Witnesses. Previous work (Selsam et al., 2019; Amizadeh et al., 2019) also showed successes in predicting satisfiable witnesses (variable assignments that satisfy the formulas) of SAT problems. 2QBF problems have unsatisfiable witnesses (assignments to ∀ variables that render the reduced propositional formulas unsatisfiable). Next, we test if we can train GNNs to predict unsatisfiable witnesses of 2QBF formulas. Specifically, the final embeddings of ∀-variables are transformed into logits via an assignment MLP (MLP asn ) and then used to compute the cross-entropy loss with the actual unsatisfiability witnesses of the formula:

logits witness = MLP asn (Emb ∀ )

Once again we tried different amount of training data (160, 320, and 640 unsatisfiable formulas) and different numbers of iterations (8 iters, 16 iters, and 32 iters), and then tested the converged models on 600 unsatisfiable new 2QBF formulas. We report the accuracy per variable and the accuracy per formula as tuples for both the training dataset and the testing dataset in Table 2 , from which we can observe that the GNNs fit well to the training data (numbers in green color), especially with more message-passing iterations. However, the GNN performance on testing data is only slightly better than random guesses (numbers in blue color), and running more iterations during testing does not help with the performance either.

3.2. WHY GNN-BASED 2QBF SOLVER FAILED:

In contrast to our initial expectation, the results above clearly show that GNNs fail to learn a 2QBF solver, unlike the previous successes in solving SAT. To investigate what limits GNNs in 2QBF solver, we first backtrack one step and examine the performance of GNNs on SAT problems.

Difficulty in Proving Unsatisfiability for SAT problems. Interestingly, previous works showed that GNN-based SAT solvers actually had trouble in predicting unsatisfiability with high confidence (Selsam et al., 2019) , if those formulas do not have a small unsatisfiable core (minimal number of clauses that is enough to cause unsatisfiability). Another work (Amizadeh et al., 2019) even completely removed unsatisfiable formulas from the training dataset (since they slowed down the training process), and only trained for predicting solutions to satisfiable formulas. However, these defects are not a problem for SAT solvers, since predicting satisfiability with high confidence is already good enough for a binary distinction.

The difficulty in proving unsatisfiability is understandable, since constructing a proof of unsatisfiability demands a complete reasoning in the search space, which is more complex than constructing a proof of satisfiability that only requires a witness. Traditionally it relies on the recursive/iterative decision procedures that either traverse all possible assignments (implicitly or explicitly) to construct the proof (DPLL (Davis et al., 1962) ), or generate extra constraints from assignment trials that lead to conflicts, until some of the constraints contradict each other (CDCL (Silva et al., 2009) ). In comparison, the message-passing scheme in GNN doesn't seem to resemble either of those procedures, but is rather similar to a subfamily of incomplete SAT solvers (WalkSAT (Selman et al., 1993) ) that randomly assign variables and stochastically search for local witnesses. Similarly, those SAT solvers cannot prove unsatisfiability.

GNN-based 2QBF Solver is Conjecturally Infeasible For 2QBF problems, constructions of both proofs (of satisfiability and unsatisfiability) need complete reasoning about a search space. Proof of satisfiability needs to show that for all possible assignments of ∀ variables, there exist satisfying assignments of ∃ variables, while proof of unsatisfiability needs to show that given a witness (assignment of ∀ variables), the reduced propositional formula is proven unsatisfiable. Given this, it's reasonable to conjecture that GNNs are probably incapable of constructing either proofs, thus being unable to learn a 2QBF solver. Traditional decision procedures (such as CEGAR-based solvers (Rabe et al., 2018) ) has a way to incrementally construct such proof, but it is unlikely that the message-passing scheme in GNNs is capable of such task. Here, we conjecture that learning complete SAT solvers and 2QBF solvers are infeasible with the current GNN architectures and message-passing schemes.

4. LEARN GNN-BASED HEURISTICS FOR 2QBF:

In Section 3, we conjecture (with empirical support) that GNN-based 2QBF solvers are infeasible.

Thus the successes of learning GNN-based SAT solvers (Selsam et al., 2019; Amizadeh et al., 2019) cannot be simply extended to more complex logical reasoning problems. Therefore we pivot our attention to learning GNN-based heuristics that work with traditional decision procedures. Considerable QBF decision procedures have been proposed due to the importance of QBF solvers in fields such as conditional planning (Rintanen, 1999) and symbolic model checking (Plaisted et al., 2003) . In this section, we will just focus on the CEGAR (Counter Example Guided Abstraction Refinement) based solving algorithm.

4.1. CEGAR-BASED 2QBF ALGORITHM:

We first present the CEGAR-based solving procedure (Janota & Silva, 2011) in Algorithm 1. Iteratively, the CEGAR algorithm proposes an assignment of all ∀ variables as a candidate, which reduces the 2QBF formula to a SAT formula. If the SAT formula is proven unsatisfiable, the candidate becomes a witness and the algorithm returns (unsat, witness). Otherwise, a satisfying assignment of ∃ variables can be found as a counter-example. Each counter-example disables a set of potential candidates, and this constraints on candidates can be expressed via accumulated clauses in the constraint SAT formula ω (details in supplementary material A.2). New candidates must be proposed from the satisfying solutions of ω, to avoid proposing candidates that are already countered (thus abstract refinement). As counter-examples add clauses to ω, ω may become unsatisfiable, meaning that no more candidates can be proposed. In that case, the algorithm returns (sat, -). The algorithm is clearly exponential, since both of the search spaces (of the candidates and the counter-examples) are exponential. It is also intuitive that the quality of candidates and counterexamples affects the runtime of the algorithm. The traditional decision procedures have proposed a MaxSAT-based heuristics, which states that the good candidates should maximize the number of unsatisfied clauses in the formula (thus making the reduced SAT problem difficult), and the good counter-examples should maximize the number of satisfied clauses in the formula (thus providing a strong constraint on the candidates) (Janota & Silva, 2011) . However, MaxSAT-based heuristics are not practical, due to the heavy overhead of MaxSAT procedures. Furthermore, the number of clauses only relates to the difficulty of the SAT problems and the strength of the constraints, but does not directly decide it. This motivates us to test whether GNN-based heuristics can be used instead.

4.2. BASIC SETUPS FOR GNN-BASED HEURISTICS:

There are challenges in integrating neural-based heuristics into CEGAR-based solvers, since each proposed assignment (candidate or counter-example) must fit some logical constraints (i.e. they must satisfy a SAT formula). It is rather difficult to add logical constraints to neural-based proposals, but relatively easy to employ neural-based ranking on proposals that already satisfy the logical constraints. In fact, it is rather easy to ask for multiple satisfying assignments from SAT solvers, if there exist. Therefore we choose to use the GNN-based embeddings to rank multiple assignments, instead of directly predicting the best assignments. We also benefit from more training data and less risk of overfitting with the ranking methodology.

To get rankings from the GNN-based embeddings, we first transform the embeddings (of all ∀ variables or all ∃ variables) into scoring matrix (Sm) via a scoring MLP (MLP score ). Then a batch of assignments (A) are ranked by passing through a two-layer perceptron (using the Sm and a learnable weighting vector Wv as weights without biases).

Sm = MLPscore(Emb) RankingScoresLogits = ReLU(A • Sm) • Wv

During training, we make use of the TensorFlow ranking library (Pasumarthi et al., 2019) to compute the pairwise-logistic-loss with NDCG-lambda-weight. We then incorporate the trained models into the CEGAR cycles by replacing the SAT-solver subroutine with a procedure that returns the highest ranked solution from multiple solutions to a given SAT formula. Note that when used in CEGARbased solvers, the GNN models only need to embed each formula once to get the scoring matrix (Sm), which is then used in all the following iterations to solve that formula. This is a significant improvement compared with previous work (Lederman et al., 2018) .

The evaluations are done on 4 separate datasets:

• TrainU: 1000 unsatisfiable formulas used for training • TrainS: 1000 satisfiable formulas used for training • TestU: 600 unsatisfiable formulas used for testing • TestS: 600 satisfiable formulas used for testing .198 25.198 with 2 baselines:

• -: vanilla CEGAR without ranking • MaxSAT: ranking by the number of satisfied clauses via on-the-fly formula simplification (Note that although MaxSAT performs the best in our evaluations, it is too expensive to use in practice. See asymptotic analysis in supplementary material A.2) via measuring the average number of iterations needed to solve the 2QBF problems. Here we choose to measure the number of iterations rather than the wall clock time, because the former only measures the quality of our heuristics, while the latter is subject to various optimizations and implementation details that involve lots of engineering effort (out of the scope of this paper). From multiple random seeds, we report the results of the models that perform best on the training datasets.

4.3. RANKING THE CANDIDATES:

Since the size of 2QBF formulas for training are quite small (the same dataset as in Section 3), we can basically enumerate all assignments in the search space to generate the training data. The interesting question left is how we assign ranking scores to all the possible candidates. One way is to follow the MaxSAT-style and rank them based on the number of clauses they satisfy (the less the better, shown as "GNN1" in Table 3 ). Another way is to rank them based on the number of solutions to the reduced SAT formula (the less the better, shown as "GNN2" in Table 3 ), since having less solutions relates to more difficult SAT problems, thus stronger candidates (see details of ranking scores in supplementary material A.2).

As shown in Table 3 , all 3 ranking heuristics (including the GNN-based and the MaxSAT-baseline) improved the solving performances of all 4 datasets. The improvement on unsatisfiable problems is more significant, since we are ranking the candidates. GNN2 seems slightly better than GNN1, implying that the training data by hardness (number of solutions to the reduced SAT formula) is probably better.

4.4. RANKING THE COUNTEREXAMPLES:

We generate the training dataset for counter-examples in a similar fashion. Once again we propose two ways to generate the ranking scores. One way is to follow the MaxSAT-style and rank them based on the number of clauses they satisfy (the more the better, shown as "GNN3" in Table 4 ). Another way is to adjust the ranking score of "GNN3" based on whether the counter-examples associate with the unsatisfiable cores in ω, the constraint SAT formula (shown as "GNN4" in Table 4 , see details of ranking scores in supplementary material A.2).

As shown in Table 4 , all 3 ranking heuristics improved the solving performances of all 4 datasets. The improvement on satisfiable problems is more significant this time, since we are ranking the counterexamples. However, GNN4 performs slightly worse than GNN3. The result implies that the additional information regarding the unsatisfiable cores in 2QBF, beyond our expectation, actually damages the GNN-based heuristic. The likely explanation is that information associated with unsatisfiable cores in 2QBF may be too complicated for GNN, which goes back to the limitation of GNN in reasoning about the whole solution space and unsatisfiability.

4.5. COMBINATION OF THE HEURISTICS:

It is reasonable to assume that ranking both the candidates and the counter-examples will further improve the solver performance. We retrained GNN models using the ranking datasets for both candidates and counter-examples, so that we still just do one GNN embedding per formula. We evaluated GNN1-3 (combining the training data of GNN1 and GNN3), GNN2-3 (combining the training data of GNN2 and GNN3), and GNN2-4 (combining the training data of GNN2 and GNN4).

As shown in Table 5 , GNN2-3 is arguably our best GNN-based model via this ranking method. We further compute relative improvement of GNN2-3, which is the ratio of improvement via GNN2-3 from "-" over the improvement via MaxSAT from "-", represented by percentages. That is shown in the last row of Table 5 as GNN2-3R. We then tested the performance of our best GNN-based heuristics (GNN2-3) on larger 2QBF problems that are extended in two different ways. On one hand, we fixed the specs (number of ∀ and ∃ literals per clause) but increased the sizes (the total number of ∀ variables or ∃ variables per formula). This essentially generated larger graphs with similar connectivity (as in the upper half of Table 6 ). On the other hand, we fixed the sizes but increased the specs (as in the lower half of Table 6 ), which essentially generated graphs with different vertex degrees. We changed the number of clauses per formula such that about half of the randomly generated 2QBF formulas are satisfiable.

We list the evaluation results in Table 6 . The DataSet column shows the specs (the first tuple), the sizes (the second tuple), and the satisfiability status with the number of clauses per formula (the letter/number after the second tuple). As shown in Table 6 , the GNN-based heuristics generalizes well to larger sizes (the upper half of Table 6 ). The relative improvement via GNN2-3 is about 70% compared with that of the MaxSAT baseline (modulo the (2,3)(8,40)S521 dataset which is hard to improve with either heuristics for some reasons), which is similar to its performance on smaller instances in Table 5 . On the other hand, the GNN-based heuristics cannot generalize so well to instances with larger specs. For the dataset with either one more ∀-literal per clause, or one more ∃-literal per clause, the relative improvement via GNN2-3 is about 50%. For the dataset with both one more ∀-literal and one more ∃-literal per clause, the GNN2-3 failed completely in generalization.

This reveals an interesting challenge in GNN-based embedding or structural data embedding in general. It is natural for GNN-based embedding to generalize to larger graphs if the vertex degrees remain unchanged. In that case, it is almost like embedding a larger batch of data. However, it is not intuitive to claim that the GNN-based embedding generalizes to graphs with different vertex degrees. This caveat should promote more researches on message-passing schemes and structural data embedding in general.

Without using the existing decision procedures, several reasoning methods purely based on neural networks are proposed for SAT solvers. Selsam et al. (2019) presented a GNN architecture that embedded the propositional formulas. From single bit supervision (the formula is satisfiable or not), the GNN learned a procedure to find satisfying assignments before issuing predictions. Also, the GNN embeddings converge given more embedding iterations, indicating that the learned procedure is stable. Amizadeh et al. (2019) further improved this line of work by adapting a RL-style explore-exploit mechanism but considering circuit-SAT problems and DAG embeddings. They trained their DAG architectures via guided gradient descent and showed that their DAG embeddings found solutions faster than the previous GNN-embeddings, but didn't even try to tackle unsatisfiable formulas.

Our paper tries to extend them to 2QBF problems, and we show that the inability to reason about unsatisfiability prevent GNNs to be a 2QBF solver. Recent work of Xu et al. ( 2019) discussed GNN's expressivity power, but not in the logical reasoning context. Samulowitz & Memisevic (2007) applied classification to predict optimal choices of heuristics inside a portfolio-based and a dynamic QBF solver . Similar to our work, (Lederman et al., 2018) targeted the 2QBF problem and used GNN-based embeddings to learn branching heuristics in CADET solver in a reinforcement learning setting. However, they have to embed an updated 2QBF formula for each branching step, thus incurring high embedding overhead. To reduce the overhead, the authors used very simple GNN architectures. They also used a small number of message-passing iterations (in fact, one iteration performed best), which defeats the purpose of GNN, because 1-iteration GNN reduces to a neighbor-counting model. On the contrary, we design our solver/heuristics such that only one GNN embedding is needed per formula, which significantly reduces the GNN inference overhead.

As a result, we can use more sophisticated GNN architectures with more message-passing iterations.

Belief propagation (BP) is a Bayesian message-passing method first proposed by Pearl (1982) , which is a useful approximation algorithm and has been applied to the SAT problems (specifically in 3-SAT (Mézard et al., 2002) ) and 2QBF problems (Zhang et al., 2012) . BP can find the witnesses of unsatisfiability of 2QBF by adopting a bias estimation strategy. Each round of BP allows the user to select the most biased ∀-variable and assign the biased value to the variable. After all the ∀-variables are assigned, the formula is simplified by the assignment and sent to SAT solvers. The procedure returns the assignment as a witness of unsatisfiability if the simplified formula is unsatisfiable, or UNKNOWN otherwise. However, the fact that BP is used for each ∀-variable assignment leads to high overhead, similar to the RL approach given by (Lederman et al., 2018) . It is interesting, however, to see that with the added overhead, BP can find witnesses of unsatisfiability, which is what one-shot GNN-based embeddings cannot achieve.

QBF problems attracted lots of research attentions due to its theoretical interests and practical applications in artificial intelligence (Rintanen, 1999) , automated theorem proving (Ranjan et al., 2004) , and sequential circuit verification (Sheeran et al., 2000) . The subclass of 2QBF is worthy of studying in its own rights, due to applications in AI planning generalized to non-deterministic domains (Rabe et al., 2018) , and planning with exponentially long plans (PSPACE-complete) (Castellini et al., 2001) .

6. CONCLUSION:

In this paper we investigated GNN-based 2QBF solvers and GNN-based 2QBF heuristics. We revealed the previously unrecognized limitation of GNN in reasoning about unsatisfiability of SAT problems, and conjectured that this limitation prevents GNN from learning solvers for more complex logical reasoning problems such as 2QBF satisfiability problem. This limitation is probably rooted in the simpility of message-passing scheme, which is good enough for embedding graph structures, but not for conducting complex reasoning on top of the graph structures. We then demonstrated that learning GNN-based 2QBF heuristics is potentially successful, though still faces interesting challenges in terms of generalization across graph structures. Our work extends previous progress in this field, and offers insights in applying machine learning tools to symbolic reasoning in general.

:



Figures and Tables:

GNN Performance to Predict SAT/UNSAT

Table content: <table><tr><td>DATASET</td><td>40 PAIRS</td><td>80 PAIRS</td><td>160 PAIRS</td></tr><tr><td>8 ITERS</td><td colspan="3">(0.98, 0.94) (1.00, 0.92) (0.84, 0.76)</td></tr><tr><td>TESTING</td><td colspan="3">(0.40, 0.64) (0.50, 0.48) (0.50, 0.50)</td></tr><tr><td colspan="4">16 ITERS (1.00, 1.00) (0.96, 0.96) (0.88, 0.70)</td></tr><tr><td>TESTING</td><td colspan="3">(0.54, 0.46) (0.52, 0.52) (0.54, 0.48)</td></tr><tr><td colspan="4">32 ITERS (1.00, 1.00) (0.98, 0.98) (0.84, 0.80)</td></tr><tr><td>TESTING</td><td colspan="3">(0.32, 0.68) (0.52, 0.50) (0.52, 0.50)</td></tr></table>

GNN Performance to Predict Witnesses of UNSAT

Table content: <table><tr><td>DATASET</td><td>160 UNSAT</td><td>320 UNSAT</td><td>640 UNSAT</td></tr><tr><td>8 ITERS</td><td colspan="3">(1.00, 0.99) (0.95, 0.72) (0.82, 0.28)</td></tr><tr><td>TESTING</td><td colspan="3">(0.64, 0.06) (0.67, 0.05) (0.69, 0.05)</td></tr><tr><td colspan="4">16 ITERS (1.00, 1.00) (0.98, 0.87) (0.95, 0.69)</td></tr><tr><td>TESTING</td><td colspan="3">(0.64, 0.05) (0.65, 0.05) (0.65, 0.06)</td></tr><tr><td colspan="4">32 ITERS (1.00, 1.00) (0.99, 0.96) (0.91, 0.57)</td></tr><tr><td>TESTING</td><td colspan="3">(0.63, 0.05) (0.64, 0.05) (0.63, 0.05)</td></tr></table>

Performance of CEGAR Candidate-Ranking

Table content: <table><tr><td/><td/><td/><td/><td/><td colspan="4">Table 4: Performance of CEGAR CounterExample-Ranking</td></tr><tr><td colspan="4">DATASET TRAINU TRAINS TESTU</td><td>TESTS</td><td colspan="4">DATASET TRAINU TRAINS TESTU</td><td>TESTS</td></tr><tr><td>-</td><td>21.976</td><td>34.783</td><td colspan="2">21.945 33.885</td><td>-</td><td>21.976</td><td>34.783</td><td>21.945 33.885</td></tr><tr><td>MAXSAT</td><td>13.144</td><td>30.057</td><td colspan="2">12.453 28.863</td><td>MAXSAT</td><td>14.754</td><td>22.265</td><td>14.748 21.638</td></tr><tr><td>GNN1</td><td>14.387</td><td>31.800</td><td colspan="2">14.273 30.588</td><td>GNN3</td><td>16.95</td><td>26.717</td><td>16.743 24.325</td></tr><tr><td>GNN2</td><td>13.843</td><td>31.404</td><td colspan="2">13.787 30.273</td><td>GNN4</td><td>17.492</td><td>26.962</td><td>17</td></tr></table>



Table content: <table><tr><td/><td colspan="4">: Performance of CEGAR Both-Ranking</td></tr><tr><td>DATASET</td><td colspan="3">TRAINU TRAINS TESTU</td><td>TESTS</td></tr><tr><td>-</td><td>21.976</td><td>34.783</td><td colspan="2">21.945 33.885</td></tr><tr><td>MAXSAT</td><td>9.671</td><td>20.777</td><td>9.425</td><td>19.883</td></tr><tr><td>GNN1-3</td><td>12.505</td><td>25.505</td><td>12.22</td><td>24.638</td></tr><tr><td>GNN2-3</td><td>11.25</td><td>24.76</td><td colspan="2">12.008 24.295</td></tr><tr><td>GNN2-4</td><td>11.686</td><td>25.021</td><td colspan="2">11.605 24.318</td></tr><tr><td>GNN2-3R</td><td>87.1%</td><td>71.6%</td><td>79.4%</td><td>68.5%</td></tr><tr><td colspan="3">4.6 EVALUATION OF LARGER 2QBF PROBLEMS</td><td/><td/></tr></table>



Table content: <table><tr><td/><td colspan="3">: Performance on Larger 2QBF</td><td/></tr><tr><td>DATASET</td><td>-</td><td>MAXSAT</td><td colspan="2">GNN2-3 GNN2-3R</td></tr><tr><td colspan="2">(2,3)(16,20)U188 289.84</td><td>110.19</td><td>157.80</td><td>73.4%</td></tr><tr><td>(2,3)(16,20)S188</td><td>569.39</td><td>218.14</td><td>335.78</td><td>66.5%</td></tr><tr><td>(2,3)(8,40)U521</td><td>74.125</td><td>28.388</td><td>42.875</td><td>68.3%</td></tr><tr><td>(2,3)(8,40)S521</td><td>238.30</td><td>223.93</td><td>232.20</td><td>42.4%</td></tr><tr><td>(3,3)(8,10)U200</td><td>26.625</td><td>9.857</td><td>18.027</td><td>51.2%</td></tr><tr><td>(3,3)(8,10)S200</td><td>49.838</td><td>31.863</td><td>42.639</td><td>40.1%</td></tr><tr><td>(2,4)(8,10)U262</td><td>26.723</td><td>10.538</td><td>17.369</td><td>57.8%</td></tr><tr><td>(2,4)(8,10)S262</td><td>45.817</td><td>28.023</td><td>37.163</td><td>48.6%</td></tr><tr><td>(3,4)(8,10)U510</td><td>36.6</td><td>14.196</td><td>35.265</td><td>6.0%</td></tr><tr><td>(3,4)(8,10)S510</td><td>71.846</td><td>48.088</td><td>71.992</td><td>-0.6%</td></tr></table>

Peer review (iclr2020):
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?