Graph Neural Networks for Reasoning 2-Quantified Boolean Formulas
Authors: Fei Wang
Zhanfu Yang
Ziliang Chen
Guannan Wei
Tiark Rompf
Venue:  (2020)
Keywords: Graph Neural Networks
2-Quantified Boolean Formula
Symbolic Reasoning

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.


GRAPH NEURAL NETWORKS FOR REASONING 2- QUANTIFIED BOOLEAN FORMULAS
Anonymous authors Paper under double-blind review
ABSTRACT
It is valuable yet remains challenging to apply neural networks in logical reasoning tasks. Despite some successes witeessed in learning SAT (Boolean Satisfiability) solvers for propositional logic via Graph Neural Networks (GNN), there haven't tt 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 learning GNN-based solvers and GNN-based heuristics for the cases with universal-existentnn quantifier alternation (so-called 2QBF problems).
We conjecture, with empirical support, that GNNs have certain limitations in learn- ing 2QBF solvers, primarily due to the inability to reason about of assignments. Then we show the potential of GNN-based heuristics in CEGAR- R-based solvers, and explore the interesting challenges generalize them larger problem instances. In summary, this paper provides comprehensive surveying view of applying GNN- embeddings 2QBF problems, and aims to offer insights applying machine learning tools to more complicated symbolic reasoning problems.
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.) (017). , and discrete heuristics decisions in games (Silver et 2017), there is a profound interest in applying the relevant techniques 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 197I) 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 (T : true, 1 : false). Boolean variables (r,), and propositional connectives such as A, V, (for example (æ] V -x2) A (- V x2)). The SAT problem asks if a given formula can be satisfied (evaluated to T) by assigning proper Boolean values to the variables. A crucial feature of the logical reasoning domain (as is visible 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-par passsingg based embeddings to solve SAT problems.
However, it should be noted that logical decision procedures is more complex that just reading the formulas correctly. is unclear if GNN embeddings (via simple uessage-passingg 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 compleee 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 where the limitation of GNN

---

is and why, in learning logical reasoning problems, decide to look at problems with complexity in- between SAT and predicate logic problems, for which QBF (Quantified Boolean Formula) problems serve as excellent middle steps. QBF is extension of propositional formula, which allows quantifiers (V and F) over the Boolean variables (such as Van 3z2. (01 V mx2) A (-01 V x2)).. In general, a quantified Boolean formula in prenex normal form be expressed such:
where Qi are quantifiers that always differ from their neighboring quantifiers, X; are disjoint sets of Boolean variables, and é is a propositional formula with all Boolean variables bounded in Qi- Cosplexity-wise. QBF problems are PSPACE-complete (Kleine Büning & (ubbeck]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 Σg -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 speed up SAT solvers in practical settings (Selsam & Bjømerr 2019). In this direction, there 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 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-basee solver framework. In Section []] we discuss the related work and conclude in Section 6 the paper we redirect details to supplementary materials.
Throughout
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 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 learn the embeddings of nodes and graphs via pnessage-passingg 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:
ma Aggregate!") (1h : N(v)))) (b) =Combine (R) (A. (M-1) mm
(K)
(1)
where (+) denotes the hidden state (embedding) node v at the 4th layer/iteration, and ((v) denotes the neighbors of node v. In each iteration, the Aggregate (*) aggregates hidden states
from node v's neighbors produce the new message (i.e., (k), for node v, and Combine (.,-) computes the new embedding of e with its last state and its current message, After 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.
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 bipartite graph, where one kind of nodes represent all literals (Boolean variables and their negations, denoted as T.). and the other kind of nodes represent all clauses (sets of literals that connected

---

via V, denoted 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)) dimension [C] x LJ. There is also another kind of edges connecting literals with their negations. The graph representation of (x1 V -x2) A (-01 22) 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 A.
3/2
C
11
C2
222
The embeddings of literals and clauses are initialized with tiled random vectors. Then the GNN uses MLPs 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 pesssage-passing given below, where Emb, and Embe denotes embedding matrices of literals and clauses respectively, Msgx-y denotes messages from X to Y. MLPx denotes MLPs of X for generating messages from the embeddings, LSTMx denotes LSTMs of X for digesting incoming messages and updating the embeddings, and represent matrix multiplication, transposition, and concatenation respectively. Furthermore, Emb-L denotes a permutational view of Emb, such that the same row of Emb,, and Emb.,,, embeddings of a variable and its negation respectively.
MsgL-C E MLP,, r. (Emb,.)
#aggregate clauses
Emba LSTMc Msg
#combine clauses
(2)
Msgc-L E² MLPc(EEbe)
#aggregate literals
Emb, L.STM,(Emb,, Msgc-.: Emb .I])
#combine literals
Note that different instances of MLPs and LSTMs used for clauses and literals (they have different subscripts). What's more, Emb-,, is used as additional message when updating Emby.
GNN Architectures for Embedding 2QBF. The difference between SAT formulas and 2QBF is that in 2QBF the variables are quantified by V or 3. To reflect that difference in graph representation, we separate Y-literals and F-literals into different groups nodes. For example, the graph representation of Vx, Rog. (I1 V -x2) A (-x1 V xr2 is shown below:
Ci
T2
C2
Accordingly, in GNN architectures, the separated V-literals and 3-literals 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.
Msgr_- BRy MLP,(Emby), Rg (EPa(E)ba)]
#aggregate clauses #combine clauses
Embe = LSTM (Embe, Msg
Msga_v = EE MLP (Embe)
#aggregate Y #combine
(3)
Emby ILLTMyMEEmb. Msg Emb-vl)
Msga-s = ET MLPc
#aggregate
Emby LSTMs (EmM,, MMg Emb-al)
#combine
Note that we use and to denote V-liteaass and all 3-literals respectively. We use Ex to denote the EdgeMatrix between X and C. and MLPc-x to denote MLPs that generate Msga-x- We de facto have tested more GNN architectures for 2QBF (see the supplementary material A.II. yet the model above performed the best in our later evaluation,
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, (8,10). That is to say, each clause has literals, of them are randomly chosen from a set V-quantified variables, and 3 of them are randomly chosen from set of 10 3-quantified variables. We modify the generation procedure that it generates clauses until the formula becomes unsatisfiable. We then randomly negate an E-quantified literal per formula to get very similar but satisfiable formula.
Predicting Satistiability. 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 that takes the embeddings of the v-variables after the propagation, and uses the average votes as logits for aatisfabliiylumssttiiubbblll prediction:
logits sat mean ML. (Embo))(Emmb))
We trained our GNNs with different amount of data (40 pairs, 80 pairs, and 160 pairs of satisfiable/un- satisfiable formulas) and different numbers of message- 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 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 Since pairs of satisfiabl/uussatiffbbble 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 Unsatisfiaiility Witnesses. Previous work (Selsam et al. 2019 Amizadeh al. 2019) also showed successes in predicting satisfiable witnesses (variable assignments that satisty the formulas) of SAT problems. 2QBF problems have unsatisfiable witnesses (assignments ' variables that render the reduced propositional formulas unsatisfiable). Next, we test we can train GNNs to predict unsatisfiable witnesses of 2QBF formulas. Specifically, the final embeddings of V-variables transformed into logits via an assignment MLP (MLPase and then used to compute the cross-entropy loss with the actual unsatisfiability witnesses of the formula:
wittsssttness = MLP asm (Emby)
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 tuples for both the training dataset and the testing dataset in Table 2 from which we observe that the GNNs fit well to the training data (numbers in green color), especially with more message-passing iterations. However, the GNN performance 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 SAT problems.
Difficulty in Proving Unsatisfibiiiity for SAT problems. Interestingly, previous works showed that GNN-based SAT solvers actually had trouble in predicting unsatisfiability with high confidence

---

Table 1: GNN Performance to Predict SATUUNSAT
Table 2: GNN Performance to Predict Winnesses of UNSAT
DATASET
40 PAIRS
80 PAIRS
160 PAIRS
DATASET
160 UnSAt
320 UNSAT
640 UNSAT
8 ITERS
(0.98, 0.94)
(1.00, 0.92) (0.50, 0.48)
(0.84, 0.76)
8 ITERS
(1.00, 0.99) (0.64, 0.06)
(0.95, 0.72)
(0.82, 0.28)
TESTING
(0.40, 0.64)
(0.50, 0.50)
TESTING
(0.67, 0.05)
(0.69, 0.05)
16 ITERS
(1.00, 1,00)
(0.96, 0.96)
(0.88, 0.70)
16 ITERS
(1.00, 1,00)
(0.98. 0.87)
(0.95,0.69)
TESTING
(0.54, 0.46)
(0.52, 0.52)
(0.54, 0.48)
TESTING
(0.64, 0.05)
(0.65, 0.05)
(0.65, 0.06)
32 ITERS
(1.00, 1.00)
(0.98, 0.98)
(0.84, 0.80)
32 ITERS
(1.00. 1.00)
(0.99, 0.96)
(0.91, 0.57)
TESTING
(0.32, 0.68)
(0.52, 0.50)
(0.52, 0.50)
TESTING
(0.63, 0.05)
(0.64, 0.05)
(0.63, 0.05)
(Selsam et al., 2019). if those formulas do not have small unsatisfiable core (minimal number of clauses that is enough to cause unsatisfiability.. Another work (Amizadeh et al. (019) 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 binary distinction.
The difficulty in proving unsatisfiability understandable. since constructing a proof of unsatisfiability demands complete reasoning in the search space, which is more complex than constructing a proof of satisfiability that only requires witness. Traditionally it relies on the recursive/ieeraive decision procedures that either traverse all possible assignments (implicitly 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- -aagggiggagnnggggg scheme in GNN doesn't seem to resemble either of those procedures, but is rather similar to subfamily of incomplete SAT solvers (WalkSAT (Selman al. (193)) 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 search space. Proof of satisfiability needs to show that for all possible assignments of A variables, there exist satisfying assignments of 3 variables, while proof of unsatisfibiility needs to show that given witness (assignment of Y 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 way to incrementally construct such proof, but it is unlikely that the message- message-passing scheme in GNNs is capable of such task. Here, we conjecture that learning complete SAT solvers and 2QBF solvers infeasible with the current GNN architectures and message-passing schemes.
4 LEARN GNN- 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 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 ALGORITIM
We first present the CEGAR- solving procedure (Janota & Silva 2011) in Algorithm [ It- eratively, the CEGAR algorithm proposes an assignment of all V variables as candidate, which reduces the 2QBF formula to a SAT formula. If the SAT formula is proven unsatisfiable, the candidate becomes witness and the algorithm returns (unsat, witness). Otherwise, satisfying assignment

---

of variables can be found as counter-example. Each counter-example disables set of potential candidates, and this constraints on candidates can be expressed via accumulated clauses in the constraint SAT formula w (details in supplementary material A.2 ) New candidates must be proposed from the satisfying solutions of w, to avoid proposing candidates that are already countered (thus abstract refinement). As counter-examples add clauses w, w may become unsatisfiable, meaning that no more candidates can be proposed. In that case, the algorithm returns (sat, -).
The algorithm clearly exponential, since both of the search spaces (of the candidates and the counter-examples) are exponential. is also in- tuitive that the quality of candidates and counter- examples affects the runtime of the algorithm. The traditional decision procedures have pro- posed 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 diffi- should
Algorithm 1 CEGAR-based 2QBF Algorithm
Input: vX
Output: (sat, -) or (unsat, witness)
Initialize constraints an empty set of clauses.
while true do
proposing candidates (has-candidate, candidate) SAT-solver(w) if not has cas-ddadddtte then
return (sat, -) end if
cult), and the good counter-exande maximize the number of satisfied clauses in the formula (thus providing a strong constraint on the candidates) (Janota & Silva, 201T). How- ever, MaxSAT-basee heuristics are not practical, due the heavy overhead of MaxSAT proce- dures. Furthermore, the number of clauses only relates to the difficulty of the SAT problems and the strength of the constraints, but does not di- rectly decide it. This motivates us to test whether GNN-based heuristies can be used instead.
proposing counter-examples
(has counter, counter) = SATTsolverr(xxx--amniii if not has- has-counter then
return (unsat, candidate)
end if
abstract refinement
details in supplementary material A.2
add counter to constraints w end while
4.2 BASIC SETUPS FOR GNN-BASER HEURISTICS
There are challenges in integrating neural- based heuristics into CEGAR-basee solvers, since each proposed assignment (candidate or counter-ext counter-example) must fit some logical constraints (i.e. they must satisfy 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 A variables or all 3 variables) into scoring matrix (Sm) via a scoring MLP (MLP.core Then a batch of assignments (A) are ranked by passing through two-layer perceptron (using the Sm and learnable weighting vector Wv as weights without biases).
Sm RankingScores.ogiiss
MI. M.Pssoore(Emb) ReLU(A Sm) Wy
During training, we make use of the TensorFlow ranking library (Pasumarthi et al.) 2019) to compute the soaniss--ogissii-llo with the CEGAR cycles by replacing the SAT-solver subroutine with procedure that returns the highest ranked solution from multiple solutions to a given SAT formula. Note that when used CEGAR- based 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 al. 2018).
We then incorporate the trained models into
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

---

Table 3: Performance of CEGAR Candidate-Raann Ranking
'Table 4: Performance of CEGAR CoumerExxamlleRRaae
DATASET
TRAINU
TRAINS
TESTU
TESTS
DATASET
TRAINU
TRAINS
TESTU
TESTS
21.976
34.783
21.945
33.885
21.976
34.783
21.945
33.885
MAXSAT
13.144
30.057
12.453
28.863
MAXSAT
14.754
22.265
14.748
21.638
GNNI
14.387
31,800
14.273
30.588
GNN3 GNN4
16.95
26.717
16.743
24.325
GNN2
13.843
31.404
13.787
30.273
17.492
26.962
17.198
25.198
with 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 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 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 the number of clauses they satisfy (the less the better, shown as "GNNI" 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-hased and the MaxSAT-bann AT-haseline) improved the solving performances of all datasets. The improvement on unsatisfiable problems more significant, since we are ranking the candidates. GNN2 seems slightly better than GNNI, 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-example in a similar fashion. Once again we propose two ways to generate the ranking scores. One way 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 to adjust the ranking score of "GNN3" based on whether the counter-examples associate with the unsatisfiable cores in w, 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 counter- examples. 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 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
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 examlees, so that we still just do one GNN embedding per formula. We evaluated GNN1-3 (combining the training data of GNNI 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 5 GNN2-3 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 Ba GNN2-3R.
Table S: Performance of CEGAR Both Bodh-Ranking
DATASET
TRAINU
TRAINS
TESTU
TESTS
21.976
34.783
21.945
33.885
MAXSAT
9.671
20.777
9.425
19.883
GNNI-3
12.505
25,505
12.22
24.638
GNN2-3
11.25
24.76
12.008
24.295
GNN2-4
11.686
25.021
11.605
24.318
GNN2-3R
87.1%
71.6%
79.4%
68.5%
4.6 EVALUATION OF LARGER 2QBF PROBLEMS
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 V and 3 literals per clause) but increased the sizes (the total number of V 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 satisñability status with the number of clauses per formula (the letter/number after the second tuple).
Table Performance Larger 2QBF
DATASET
MAXSAT
GNN2-3
GNN2-3R
(2.3)(16.20)U183
289.84
110.19
157.80
73.4%
(2.3)(16,00)S188
569.39
218.14
335.78
66 66.5%
(8.3)(8440U552)
74.125
28.388
42.875
68.3%
(2.3)(8,00)552)
238.30
223.93
232.20
42.4%
(3,3) 100JU00
26.625
9,857
18.027
51.2%
100)S2000
49.838
31.863
42.639
40.1%
(2,4) 10)U262
26.723
10.538
17.369
57.8%
(8,4) (2)5)2210))222
45.817
28.023
37.163
48.6%
10)
36.6
14.196
35.265
6.0%
10))5500
71.846
48.088
71.992
-0.6%
As shown in Table 6 the GNN-based heuristics generalizes well 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))S52 dataset which 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 instances with larger specs. For the dataset with either one more Vilitaal per clause, one more 3-literal per clause, the relative improvement via GNN2-3 about 50%. For the dataset with both one more V-literal and one more 7-literal per clause, the GNN2-3 failed completely in generalization.
This reveals an interesting challenge 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, is almost like embedding a larger batch of data. However, is not intuitive to claim that the GNN-based embedding generalizes graphs with different vertex degrees. This caveat should promote more researches on pessage-passiingg schemes and structural data embedding in general.

---

5 RELATED WORK AND DISCUSSION
Without using the existing decision procedures, several reasoning methods purely based on neural networks are proposed for SAT solvers. [Selsam 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 RL--ttlle explore-expliit 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- MeNN-embeddings. but didn't '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 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 learn branching heuristics in CADET solver in 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-passingg iterations (in fact, one iteration performed best), which defeats the purpose of GNN, because 1-iteration GNN reduces to neighbor-counting 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 result, we can use more sophisticated GNN architectures with more message-passing iterations.
Belief propagation (BP) a Bayesian sessage-passing method first proposed by Pearl (1982), which is usefuul approximation algorithm and has been applied to the SAT problems (specifically in 3-SAT (Mézard et al. ) 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 v-varialle and assign the biased value to the variable. After all the V-variables 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 V-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 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 Al planning generalized to non-etteriiiistic domains (Rabe et al., 2018), and planning with exponentially long plans (PSPACF-ccomplete) (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 symbolic reasoning in general.

---

REFERENCES
Saced Amizadch, Sergiy Matusevych, and Markus Weimer. Learning solve cireuit-SAT: unsupervised differentiable approach. In International Conference on Learning Representations, 2019. URL tt
//openreview.net/ htt.://wewntoooommm///ox22gg222
Claudio Castellini. Enrico Giunchiglia, and Armando Tacchella. Improvements to sat-based conformant planning. 01 2001. doi: 10.131402...16911.666
Hubie Chen and Yannet Interian. model for generating random quantified boolean formulas. IJCAI, pp. 66-71. Professional Book Center, 2005.
Alonzo Church. A note on the entscheidumnssrrobem.. J. Symb. Log,, 1(1):40-41, 1936.
Stephen A. Cook. The complexity of eecorem-proving procedures. In Proceedings of the Third Annual ACM Symposium Theory Computing, STOC '71. pp. 151-158. New York. NY, USA. 1971. ACM. doi:
1..114450011578005444 Ittp:://d/ acm wtt.://..cc.rrg/o.//g.///o org/10. 1145/11115/.1.../ 885847
Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving proving. Commun. ACM, 5(7):394 397, 1962.
Awni Y. Hannun, Carl Case, Jared Casper, Bryan Catanzaro, Greg Diamos, Erich Elsen, Ryan Prenger, Sanjeev Satheesh, Shubho Sengupta, Adam Coates, and Andrew Y. Ng. Deep speech: Scaling up end-to-end speech recognition. CoRR, abs/1412.5567, 2014.
Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Deep residual learning for image recognition. In CVPR. pp. 770-778. IEEE Computer Society, 2016.
Mikolás Janota and João P. Marques Silva. Abstraction bassee algorithm for 2qbf. In SAT, volume 6695 of Lecture Notes Computer Science, pp. 230 244. Springer, 2011.
Hans Kleine Büning and Uwe Bubeck. Theory of quantified boolean formulas. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 735-760. IOS Press, 2009.
Gil Lederman, Markus N. Rabe, and Sanjit A. Seshia. Learning heuristics for automated reasoning through deep reinforcement learning. CoRR, abs/l807 .08058, 2018
M. Mézard, G. Parisi, and R. Zecchina. Analytic and algorithmic solution of random satisfiability problems. Science, 297(5582):812 815, 2002. ISSN 0036-8075.
Alexander Nadel, Vadim Ryvchin, and Ofer Strichman. Efficient MUS extraction with resolution. In FMCAD, pp. 197-200. IEEE, 2013.
Rama Kumar Pasumarthi, Sebastian Bruch, Xuanhui Wang. Cheng Li, Michael Bendersky, Mare Najork, Jan Pfeifer, Nadav Golbandi, Rohan Anil, and Stephan Wolf. Tf-ranking: Scalable tensorflow library for learning-to-rank In KDD, pp. 2970-2978. ACM, 2019.
Judea Pearl, Reverend bayes on inference engines: A distributed hierarchical approach. In AAAI pp. 133-136.
AAAI Press, 1982.
David A. Plaisted, Armin Biere, and Yunshan Zhu. A satisfiability procedure for quantified boolcan formulac. Discrete Applied Mathematics, 13002):291-328, 2003.
Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, and Sanjit A. Seshia. Understanding and extending incremental determinization for 2qbf. In Hana Chockler and Georg Weissenbacher (eds.), Computer Aided Verification, pp. 254, Cham, 2018. Springer International Publishing.
Darsh Ranjan. Daijue Tang, and Sharad Malik. A comparative study of 2qbf algorithms, In IN PROCEEDINGS OF THE 7TH INTERNATIONAL. CONFERENCE ON THEORY AND APPLICATIONS OF SATISPIABILITY TESTING (S4 ACM, 2004.
Jussi Rintanen. Constructing conditional plans by theorem-proves J. Artif. Intell. Res., 15:323-352, 1999.
Horst Samulowitz and Roland Memisevic, Learning to solve QBF. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22-26. 2007, Voncouver, British Columbia, Canada, pp. 255-260.
AAAI Press, 2007. URL http:h//t///w awai. ww..orgg////// http:////..bbarr/aa//////////aaa
009. php
Bart Selman, Henry A. Kautz, and Bram Cohen. Local search strategies for satisfiability testing. In Cliques. Coloring, and Satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pp. 521-531. DIMACS/AMS, 1993.

---

Daniel Selsam and Nikolaj Bjørner. Guiding high-performance SAT solvers with unsat-core predictions. In SAT, volume 11628 of Lecture Notes in Computer Science, pp. 336-353. Springer, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz. Percy Liang. Leonardo de Moura, and David L. Dill. Learning SAT solver from single-bit supervision. ICLR (Puster). OpenReview.net, 2019.
Mary Sheeran, Satwinder Singh, and Gunnar Stålmarck. Checking safety properties using induction and sat-solver. FMCAD, 2000.
João P. Marques Silva, Inés Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiabllity volume 185 of Frontiers Artificial Intelligence and Applications, pp. 131-153, IOS Press. 2009.
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou. Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap. Karen Simonyan, and Demis Hassabis. Mastering chess and shogi by self- play with general reinforcement learning algorithm. CoRR, abs/1712.01815, 2017.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention all you need. In NIPS, pp. 5998 6008, 2017.
Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In ICLR. OpenReview.net, 2019.
Pan Zhang, Abolfazl Ramezanpour, Lenka Zdeborová, and Riccardo Zecchina. Message passing for quantified boolean formulas. CoRR, abs/1202.2536 2012. URL htt////t///rrr....o//////2/22/3

---

A APPENDIX
A.I ALL EEN-EMBEDDING ARCHITECTURES
We use subscript symbols A to denote all Y q-qunntified literals, to denote all 3-quantificd literals, L to denote all literals, and C' to denote all clauses. We use notations Emby to denote embeddings of X, where X can be subscript V. 3, L, or C. We use notations Emb-x to denote embeddings of the negations of X (4, 3, L). which permutational views of Embx such that the variable and its negation respectively.
of Embx and Emb-x use notations Msgx_. to denote messages from X to We also use notations MLPx to denote MLPs that generate messages from the embeddings of X. notations MLPx - to denote MLPs that generate messages from the embeddings of X for Y. notations LSTMx to denote LSTMs that update embeddings of X given incoming messages, and notations LSTMx e-Y Y to denote LSTMs that update embeddings given incoming messages from Y. also use notations 15xx denote sparse adjacency matrix (A, 7, or L.) and clauses, notations X to denote matrix multiplication
embeddings of
and Y, notations [X, Y] to denote matrix concatenation of X and Y, and notations X" to denote matrix transposition of X.
Our first form of GNN peessage-passingg of 2QBF (Model 1) is given below.
Model
Msge: = Ey (Emby + Eg MLP2(Emba))
Embe LSTMcc Msga)
Msgc-v E? MLP (Embe)
Emby LSTM,(Emb,, M Emb-v))
Msgc-3 E.¹- (LPCc
Embg LSTMy(Embb, Emb-a))
In Model 2. we update the clause embedding with 2 LSTMs, each of them take the messages from V and literals respectively.
Model 2:
Msgv Ey (Lmb(
Msga+cC Es MLP (Emba)
Embc LSTM -M (Embc, Msgv..c
Embe = M (Embe, Msga
Msgc-v Σ MLPc((Ebbe)
Emb, = LSTMy (Emby, [ Emb-+])
Msgo- = E MLPc(Embe)
Emby = LSTb, [Mgo Emb-a])
We switch the order these LSTMs in Model 3.
Model 3:
Msga4c MLP: (Emba)
Msg.,JC Ev MLP, (Emby)
Embc = LST LST - [Embe, Msgg
Embe = LSTM
Msg._c)
Msga-v = R3 (l.bc(Embe))
Emby LSTM, MMgo--v: Emb-v])
Msgo = ET (LPc<
Emb: LSTM= [Msgo=,,Emb.

---

In Model concatenate the messages from and 3 literals.
Model 4:
Msgc [B MLPy(Emb,))........mm Ba (LP=(Emba)]
Embe (ETMe Msgc)
- E MLPc(Embc)
Emb, (.mb,, [Msgo-y: Emb x])
Msgc-3 FŞJ Ml.Pc(Embb))
Emby (Emb,, [ Emb-a])
The performance of our GNN architectures improve greatly after we realize that (in Model 5) may also need different ML.P modules generate messages from clauses and E literals. Note that this also the model we reported the main paper, and model we decided to use for results reported the main paper.
Model 5:
Msge: [By (Emb( Rg MLPs(Emb))]
Emby (Embe,
Msga E MLP (Embe)
Emb, = LSTM,(Emby, [Msgo-v: Emb-v])
Msga-+ E3 (LLPc-a<EEme)
Emby = LSTMMg(Emb,, [Msga_.. Emb..))
We also explore the possibility Model 6) of having two embeddings each clause, one serving the Y literals one serving the literals. We need extra notations: Embx-y denotes embeddings X serves Y. LSTMX-y denotes LSTMs that updates embedding of X that serves Y.
Model 6:
Msga = [Ev MLPy(Emby), Eg MLP3(Emba))
Emba = LLSMc-+v (Embc-w.. Msg..)
Embe-s (Embc=s Msge:
Msga-v = ET MLPc-wwEmmbea...
Emby LSTM, [Mg Emb-v))
Msga-1 T (Fmbcc-)(mmcc+a)
Emb: LSTM; [Ms Emb-a))
We further explore possibility (in Model 7) that our embedding scheme should reflect CEGAR cycle, which starts from A variables (proposing candidates), to clauses, to 7 variables (finding counterexamples), back to clauses, then back y variables.

---

Model 7:
Msgv-c = By MLP+(Emb.)
Embc-1 1 Msgv
Msgc = Tİ -M-Pc-a(Fmmc--a)
Emb; (Emb,, Msgc Emb.s.))
Msg= = E3 (LPaa
Embe-v = (SSTMc--V(EEbee Msga
M = Ey MLP (Embec
Emby = LSTM, (Bmby, M Emb-v])
A.2 CEGAR ALGORITHM AND RANKING SCORES
Steps of Abstract-Refinemeet in CEGAR-based 2QBF sovlers This paragraph explains in detail about how abstract refinement CEGAR- based 2QBF sovlers works (Janota & Silva 2011) for our 2QBF formulas in CNF (conjunction normal form). Basically, abstract refinement is about maintaining and augmenting the constraint SAT formula w, the solutions of which are the candidates in the next round of iteration.
In the main paper, we said that initialize initialize w with many variables and clauses. The variables include all the V variables in the 2QBF formula, and a fresh variable z. for each clause in 2QBF formula. Intuitively, the variable 2, represents that the clause e is not satisfied by the candidates. The w is also initialized with many 2-sized clauses as below: for each clause c in the 2QBF formula, we add clause (-2e V -)) for each y literal in c. It should be clear that this initialization poses no constraints to all Y variables, since
empty set of clauses. That was simplification. Actually, we
set all to false to satisfy all clauses in trivially.
For each counter example (assignment all E variables), compute the of 2QBF clauses that not satisfied by counter example (call them residual clauses). Intuitively, the constraint should say: at least one of the residual clauses should not be satisfied by the next proposed candidate, so that the current counter example cannot counter it. That constraint is realized by adding to w one clause (V2c for all in the residual clauses). This clause guarantees that at least one of the residual clauses is not satisfied by the next candidates, and transfers the constraints related A variables the corresponding (-2e V -l) clauses w.
Asymptotic analysis GNN-based heuristics v.s. MaxSAT-baseling overhead of GNN-based heuristics with the MaxSAT-baseline let us assume a 2QBF instance with Ny V- variables, Ng 3 variables, and M clauses. We also assume that on average, each clause has ny V-literals and mg 3-literals. Now need to rank K candidates
rigorously compare the
coutte--xxapples
The time complexity of MasSee--asee (on-the-fly formula simplification) is O ((MM.w). which is for each candidate and each clause, check the candidate satisfies clause in ny steps.
We also assume that the second dimension of scoring matrix (Sm) d. The time complexity of GNN-based heuristics is equivalent to the 2 matrix multiplications of dimensions (K, Nv) x (Ny, d) and (K, d) (d, 1), which is O(K Nyd).
To compare the complexity, variables the formula) is often much smaller than M (number clauses in formula), Moreover, in practice, matrix multiplications can be easily parallelized and accelerated on many kinds of hardware with BLAS libraries. Of course, GNN-base based heuristics needs the GNN-embeddings via pessaag--passing but that is computed only once per formula, with the cost amortized.
safely assume that both d and my small constants. However, Ny (number
GNN1 Candidate Ranking Score: i.e. based list of the numbeer of satisfied clauses.
def n. his.ussslistt2..rnnnngsosooo n_clauses_mit lali_clllaus__ssst
return [max(1, n. clauses clauses. _min)
for n clauses in n. clauses. list]
GNN2 Candidate Ranking Score: i.c. hased on list of the numbers of solutions to the simplified SAT formula.

---

if n_solutions < 3: return 10.0
n_solutions
if n_solutions <= 5: return 6.0
if nolouutoons 8: return 5.0
n.solutions 12: return
n_solutions 16: return 3.0
n_solutions <= 21: return 2.0
else: return 1.0
n_solutions_ www.eaannnnnoosssnnnonoo return
list): for n_solutions in n_solutions_ list]
GNN3 Counter-example Ranking Score: i.e. based on a list of the numbers of satisfied clauses.
def n_clauses_liste 2_stte___ist____eee 2ar.listt22rnnnnn_ssoorrree scriinnssccoreescunteteereeee cnuuteer__clauss___isttt
n. clauses max = max(n. clauses _ist)
return [max(1, 10 n. n__clauss__m max clauses)
for clauses in c_alauses list]
GNN4 Counter-example ranking Score: ie. adjusted from GNN3 ranking scores based on unsatisfiable cores.
def unsat core 2 ranking scores. counter(core index, n. clauses list): scores. # core index marks the index of scores that are in the unsatisfiable cores.
n_clauses_max max(n_clauses.list)
[max(1, n=clauses_max n_clauses)
for clauuse in n_clauses_
scores numpy. hmpp.array(scoress
scores[core_inddsl index] = 10
return tolist
Procedure determine which counter-examples associate with the unsatisfiable cores: Since each counter-example will add a clause to the constraint SAT formula w, determining the unsatisfiable cores (the smallest subset of clauses that constraints the formula to be unsatisfiable) of w will give us the sets of counter-examples that directly associate with the unsatisfiable cores.
For satisfiable 2QBF formulas in the training dataset, generate all clauses of from all counter-examples. then solve w with hmueSAT (Nadel el al.) (013) for unsatisfiable cores. For unsatisfiable 2QBF formulas, we again collect all clauses of w from all counter-examples In this case w is satisfiable, and the solutions to it are actually witnesses of unsatisfiability. To obtain unsatisfiable cores, we add the solutions back to w as additional constraints, until w is unsatisfiable with the cores returned.


Reviews:
[{"review_id": "HJgGOTcDtS", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper first presents GNN architectures to solve 2-QBFs. They show that similar GNN architectures which work for propositional logic do not transfer to 2-QBFs, and provide some explanation for the result. Finally, they show how GNN modules can be used to speed up existing 2-QBF solvers instead. I mostly like the paper. The claims of the paper are well presented and empirically validated. Here are some suggestions / complaints:\n\n1. It will be good to have more overview of 2-QBFs and existing solvers. How popular is CEGAR and why the improvements to its performance is important ?\n2. Dataset sizes are tiny compared to current standards. Is there a reason to use such small datasets ? From the results, I don't think any of the conclusions will change significantly from the dataset size, but still its better to use larger datasets.\n3. I think all tables should be self-explanatory. There are too many dataset splits and captions of tables do not provide any information. ", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly."}, "extra_text": {}}, {"review_id": "ByefKW4V5r", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper investigated the GNN-based solvers for the 2-Quantified Boolean Formula satisfiability problem. This paper points out that GNN has limitations in reasoning about unsatisfiability of SAT problems possibly due to the simple message-passing scheme. To extend the GNN-based SAT solvers to 2-QBF solvers, this paper then turns to learn GNN-based heuristics that work with traditional decision procedure, and proposes a CEGAR-based 2QBF algorithm.\n\nOverall, the topic of combining logic reasoning and graph neural networks is interesting. But it is not clear how important is the targeted 2-QBF problem, except for testing and finding the limitations of GNN. In other words, this paper picks up a specific class of model for a very specific class of problem, which lacks sufficient and convincing motivations. Although GNN achieves success in solving SAT problems, it is not necessary that GNN is a must for solving the 2-QBF problems. Also, when analyzing the limitations of GNN, the paper makes conjecture only based on empirical results. It would be much more insightful to provide some theoretical analysis so that the paper can inspire other researchers working on different problems. Based on the above reasons, I would like to recommend a weak reject for this paper.", "extra_scores": {"experience_assessment": "I have published one or two papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "B1xdwB9TKr", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "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.\n\nThis 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.\n\nI 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. \n\nA couple questions and concerns:\nIn 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?\nSection 4.2: how are the TraunU, TrainS, TestU, and TestS datasets generated?\nIn 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?)\n\nAnd minor points on clarity:\n* “-” for the baseline seems a bit awkward; consider spelling out “vanilla”?\n* 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?\n", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: This work investigates the use of graph NNs for solving 2QBF . The authors provide empirical evidence that for this type of satisfiability decision problem, GNNs are not able to provide solutions and claim this is due to the message passing mechanism that cannot afford for complex reasoning. Finally, the authors propose a number of heuristics that extend GNNs and show that these improve their performance.

2-QBF problem is used as a playground since, as the authors also point, their complexity is in between  that of predicate and propositional logic. This on its own is not bad,  as it can be used as a minimal environment for the type of investigation the authors are interested. That being said, I find a number a number of flaws in the current form of the paper (some of them pointed by R3 as well), with the main issue being that of lack experimental rigor. Given the restricted set of problems the authors consider, I think the experiments on identifying pathologies of GNNs on this setup could have gone more in depth. Let me be specific. 

1) The bad performance is attributed to message-passing. However, this feels anecdotal at the moment and authors do not provide firm conclusions about that. The only evidence they provide is that performance becomes better with more message-passing iterations they allow. This is a hint though to dive deeper rather than a firm conclusion. For example do we know if the finding about sensitivity to  message-passing  is due to the small size of the network or the training procedure? 
2) To add on that, there is virtually no information on the paper about the specifics of the experimental setup, so the reader cannot be convinced that the negative results do not arise from a bad experimental configuration (e.g., small size of network).
3) Moreover, the negative results here, as the authors point, seem to contradict previous work, providing negative results against GNNs.  Again, this is a valuable contribution if that is indeed the case, but again the paper does not provide enough evidence. In lieu of a convincing set of experiments, the paper could provide a proof (as also asked by R3). However with no proof and not strong empirical evidence that this result does not feel ready to get published at ICLR.

Overall, I think this paper with a bit more rigor could be a very good submission for a later conference. However, as it stands I cannot recommend acceptance. 

Decision: Reject