Transformers satisfy
Authors: Feng Shi
CHEN LI
Shijie Bian
Yiqiao Jin
Ziheng Xu
Tian Han
Song-Chun Zhu
Venue:  (2021)
Keywords: constraint satisfaction problem
graph attention
transformers

Abstract: The Propositional Satisfiability Problem (SAT), and more generally, the Constraint Satisfaction Problem (CSP), are mathematical questions defined as finding an assignment to a set of objects that satisfies a series of constraints. The modern approach is trending to solve CSP through neural symbolic methods. Most recent works are sequential model-based and adopt neural embedding, i.e., reinforcement learning with neural graph networks, and graph recurrent neural networks. This work proposes a one-shot model derived from the eminent Transformer architecture for factor graph structure to solve the CSP problem. We define the heterogeneous attention mechanism based on meta-paths for the self-attention between literals, the cross-attention based on the bipartite graph links from literal to clauses, or vice versa. This model takes advantage of parallelism. Our model achieves high speed and very high accuracy on the factor graph for CSPs with arbitrary size.

Under review as a conference paper at ICLR 2021
TRANSFORMERS SATISFY
Anonymous authors Paper under double-blind review
ABSTRACT
The Propositional Satisfiability Problem (SAT), and more generally, the Constraint Satisfaction Problem (CSP), are mathematical questions defined as finding an as- signment to of variables such that all the constraints are satisfied. The modern approach is trending to solve CSP through neural symbolic methods. Most recent works are sequential model-based, and adopt neural embedding. i.e., reinforce- ment learning with graph neural networks, and graph recurrent neural networks. In this work, we propose Heterogeneous Graph Transformer (HGT), a one-shot model derived from the eminent Transformer architecture for factor graph struc- ture to solve the CSP problem. We define the heterogeneous attention mechanism based meta-paths for the self-attention between literals, the cross-attentie based on the bipartite graph links between literals and clauses. Exploiting high- level parallelism, our model is able to achieve exceptional speed and accuracy on the factor graph for CSPs with arbitrary size. The experimental results have demonstrated the competitive performance and generality of HGT compared the most recent baseline approaches.
INTRODUCTION
The Constraint Satisfaction Problems (CSP) is of central importance in several aspects of computer science, including theoretical computer science, complexity theory, algorithmics, cryptography, and artificial intelligence. CSP aims at finding a consistent assignment of values to variables such that all constraints. which are typically defined over finite domain, are satisfied. In particular, there is an assortment of problems arising from artificial intelligence and circuit design that can be reduced to CSP subtypes, including map coloring, vertex cover, independent set, dominating set, and clique detection.
Solving CSP on finite domain is often an NP-complete problem with respect to the domain size. The conventional CSP-solvers rely on handcrafted heuristics that guide the search for satis- fying assignments. These algorithms are focused on solving CSP via backtracking or local search. Hence, the resulted model is bounded by the greedy strategy, which is generally sub-optimal. With the advent of Graph Neural Networks (Scarselli et al. (2009)) the geometric deep learning (Bron- stein et al. (2017)) for Non- Ean-Euulddenn data has become one of the most emerging fields of machine learning. In particular, it brought deep learning solutions to of the most dominant combinato- rial optimization problems, the Constraint Satisfaction Problem (CSP) (Khalil et al. (201)). Works including NeuroSAT (Selsam al.) (2018) and Circuit-SAY (Amizadeh et (2018) commenced the study of neural methods targeted at CSP. Later works, such as Yolcu & Póczos (2019) and You al. (2019), attempted solve CSP through different deep learning approaches. However, most pioneering works, such as neural approaches utilizing RNN or Reinforcement Learning, are still restricted to sequential algorithms, while clauses are parallelizable even though they are strongly correlated through shared variables.
In this work, we propose hybrid model of the Transformer architecture (Vaswani et al. 2017 and the Graph Neural Network for solving combinatorial problems, especially CSP. Our main con- tributions in this work are: (a) We derived meta-paths adopted from Sun et al.) (201T) to formulate the message passing mechanism between homogeneous nodes (i.e., variable to variable, or clause to clause), which enable us to perform self-attention and let message pass through either variables sharing the same clauses, or clauses that include the same variables. We apply the cross -ats-ntttntion mechanism to optimize message exchanges between heterogeneous nodes(i.e.. clause to variable, or variable to clause). (b) With the combination of homogeneous attention and heterogeneous allen-

---

Under review as a conference paper at ICLR 2021
tion mechanisms on bipartite graph structure, we then combine Transformer with Neuro- Symbolic methods to resolve combinatorial optimization on graphs. (c) We proposed Heterogeneous Graph Transformer (HGT), general framework for graphs with heterogeneous nodes. In this work, trained the HGT' framework to approximate the solutions of CSP (but not limited to CSP). Our model is able to achieve competitive accuracy, parallelism, and generality on CSP problems with arbitrary sizes
RELATED WORK
Recently, the Machine Learning community has seen an increasing interest in applications and op- timizations related to constraint satisfaction problem solving. Various frameworks utilising diverse methodologies have been proposed, offering new insights into developing CSP solvers and classi- fiers. For example, [elllo et al. (2016) adopts Reinforcement Learning in their Neural Combinatorial Optimization, with an approach based on policy gradients. On the other hand, works such as Evans et al. (2018) and/Arabshahi et al. (2018) have demonstrated the effectiveness of recursive neural net- works in modeling symbolic expressions. Meanwhile, |Prates et al. (2019) proposed an embedding- based message- passseggaainggggg algorithm for solving Traveling Salesman Problem (TSP), highly relevant CSP problem.
NeuroSAT' (Selsam et al. (2018) is graph neural network model that aims solving the Boolean Satisfiability Problem (SAT) without leveraging the greedy search paradigm. It approaches SAT as a binary classification problem during training and finds an SAT assignment from the latent represen- tations during inference. NeuroSAT is able to search for solutions to problems of various difficulties despite training for relatively small number of iterations. As an extension to this line of work, [Sel- sam & Bjømer (2019) proposes neural network that facilitates variable branching decision making within high-pertormance SAT solvers on real problems.
PDP Amizadeh et al. (2019) is a generic neural framework for learning CSP solvers based on the idea of Propagation, Decimation, and Prediction. PDP provides a completely unsupervised training mechanism for solving SAT via energy minimization, and can be seen as learning optimal message passing strategy on probabilistic graphical models.
G2SAT (You et al. (2019) is a deep generative framework that learns to generate SAT formulas from a given set of input formulas while preserving the graph statistics. Even though G2SAT lacks the ability to derive solutions, it provides synthetic formulas for hyperparameter optimization.
RLSAT (Yocuu & Póczos (0199) learns SAT solvers through deep reinforcement learning and it- erative refinement. It incorporates graph neural network into a Stochastic Local Search( al- gorithm to act as the variable selection heuristic during training. However, since SLS begins with randomly initialized parameters, and non-zero terminal reward is given only when a satisfying assignment is found, RLSAT requires a curriculum learning process for performance improvement. As result, RLSAT becomes inefficient when its learning process starts with large complex graphs, in which satisfying assignments are hard to obtain. In our HGT, each possible state of assignment corresponds to a likelihood, which can be minimized to train the model. In particular, HGT is able to achieve optimal performance in efficiency and accuracy regardless of input graph sizes.
BACKGROUND
3.1 CONSTRAINT SATISFACTION PROBLEMS
fundamental problem in logic study that constitutes the cornerstone of combinatorial optimization. It provides feasible models to real world applications and is intensively involved in the design of artificial intelligence. An instance of CSP problem, CSP(V, U), is constituted of two main components: a set of N variables V E 1...N.. defined over a discrete domain D; and set of M constraint functions or factors, U (u,(2,) : j E L...M where qj is subset of V subject to uj. For each u, E U. uy : Diasl + (0, 1) outputs 1 if the input 9; satisfies constraint uy, and otherwise. A CSP problem can be formulated in Conjunctive Normal Form (CNF) (Piahringer (2010)) with the goal of finding an assignment of variables that satisfies all constraints. For given assignment to V. the measure of
Constraint Satisfaction Problems (CSP) Kumar 1992
(v;
2

---

Under review as a conference paper at ICLR 2021
CSP problem, Φ {0, + {0, 1}. is a function that returns if all the clauses in the problem are satisfied, and otherwise. Such measure function is in CNF
1. For all U, U. Uj a disjunction of literals. Here literals refer to vs or mi, for vs E 9j
2. d(V) Aug. j = {1,....M) M).
3.2 GRAPH NEURAL NETWORKS AND GRAPHI ATTENTION NETWORKS
Graph Neural Network (GNN) (Scarselli et al. 2009 provides basic architecture to operate neural network on graphs. Suppose V is a set of nodes, where each vertex U, V carries node feature ha Rd and & C V V is a set of undirected edges, where each edge ei.j E & that connects v; to By E V carries an edge feature hajj E Rde For time step t E {1..... T), GNN on the graph G(V, 8) passes messages between direct neighbors, and iteratively updates the feature vector each
Vy E V following:
hy = =Q
1--1 U
(h h h4.5)
(1)
USEN;
where N₁; = fuj E V Ber E 8), and M, Q are the message function and the update function to be learned, respectively.
3.3 TRANSFORMER AND THE RELATION WITH GNN
Transformer (Vaswani et al. (017)) is the state-of-the-art approach for sequential data and trans- duction problems that relies on self-attention mechanism. When looking into the architecture of Transformer, the computation of similarity between queries and keys highly resembles finding correlation between two types of nodes in fully connected bipartite graphs, while the self-attention mechanism among queries or keys (or tokens in NLP terminology) can be seen as calculating the weighted contribution in a half-complete connected graph, where an output token does not depend want to extend the Transformer architecture to hetero-
on future words. With these resemblance, geneous graph structures, such as bipartite graphs
4 METHODOLOGY
4.1 FACTOR GRAPHS AND META-PATHS
The value of each constraint is binary, which makes it possible to express the measure of a CNF
d(V II (g(())
The expression can be properly presented as an undirected bipartite factor graph. We construct such factor graph G(VVU), E`) by defining the set of variables V (vi....,,n,] the set of clauses U (u,,..., um }. and edges by: Ci.; E E iff variable v2 is involved constraint uy either in positive negative relation. In Yolcu & Póezos (2019). each edge is assigned with type depending on the polarity of the variable it connects to. The positive occurrence of a variable e; in clause (or factor) új represented with the positive sign (+), whereas its negative occurrence -w; in uj is represented with the negative sign (-). Hence, pair of n x m bi-adjacency matrix A = (A4, A_) is used store two types of edges such that (i.
+ - uy. Here E uj implies that u; instead of its negation -u is directly involved in uy. Each edge ei, E then assigned value equals to for edges in A4 and -1 for edges in A_ With the factor graph representation, graph neural network can be applied as CSP-solver (Selsam al. (2018); Yolcu & Póczos ( However, due to the fact that factor graph is bipartite in which variables only connected to clauses, clauses are only connected to variables. Furthermore, traditional GNN only passes messages to local neighbors, and is thus inefficient at passing messages between variables or between clauses. Consequently, variable nodes update their state solely based on their current states and the states of the clauses they affect, vice versa. In this work, we propose to pass message through length-2 meta-paths in addition existing edges, which enables: 1) variables
< U/ E uy and A_ (i,
3

---

Under review as a conference paper at ICLR 2021
Variable
C
gräph of
Decomposition factor graph poslthve and mogntive Constraints
(a) Factor graph for the CNF with measure & (w) Vu2 Vea)AAa)( where solid lines are the positive incidences of U; in új, and dashed lines are the negative incidences of -u in uy: (b) the decomposition of the factor graph according to the positive and negative re- lations, which are used for crossing-attention; (c) meta-paths are used for the self-attention among literals or clauses.
Figure I:
to incorporate the information from variables that share the same clauses during state updates; 2) clauses to incorporate the information from clauses that share some variables when update their states. In a CSP factor graph, we define that a meta-path ma, = (V), Uk. 02)) between nodes i and 2y exists if there exists some Uk V s.t. Bee & and _es, E E. Since self-attention mechanism is not symmetric, our meta-path is directed. As a result, we get four types of meta-paths in total (-,-)) ), as illustrated in Figure The adjacent matrix of such
(i.e., {(+, +), (+, meta-path can be easily computed by matrix multiplication
A. and A_ or their transposes. Take A(+.)) A(+.-) as examples, the adjacency matrix A(+,+) A+ stores all (+, +) meta-paths, and A(+,-) = AT stores all (+:-) meta-paths. diagonal entry ((.,))(E. indicates the number of positive edges that v; has, and an off-diagonal entry Ac+,)](,,j] indicates the existence of (+, +) meta- meta-ppth from 2 to e/g-
4.2 HOMOGENEOUS AND HETEROGENEOUS GRAPH ATTENTION CONVOLUTION
In order to incorporate attention mechanism into the bipartite graph, we extend the original Graph Attention Network (GATConv) (Veličković et al. (207)) with heterogeneous graph attention, while we consider the original attention in GATConv as homogeneous graph attention. Heterogeneous attention is used for nodes of different kinds. Nodes in different partitions are normally of different features or characteristics, e.g., literals forming partition different from clauses their partition. Suppose literal and clause feature matrices are V R NxF. F. and U R Mx F., respectively; and their adjacency matrix A E R M The heterogeneous attention is define as:
Cv,,y = o(aullla, [W, W.l. Eug.u. = =[(aallaa)) [[ (W, explevs.u)))
de,,, = softmax,, (em,,,) EnCEN( exrplernie))
(3)
explenggn))
Ony.w, = softmax,, (ewy,n) softmax,,(eug..r)) = EmVEN(Y exp(Car.e))
V' RVW UWW), U' = ReLU(UW, A
where W,, E R.XF and W., E FuxF are embedding weights for variables and clauses that transform input feature into a common high-level feature of dimension F. an E IR and a, E R are shared attention mechanism on variables and clauses. Attention matrix Au-se E NxM stores edge scores from clauses to variables as An-oe(,]]] ouy, and Ap-zu M stores edge scores from variables to clauses as A,, [j. = aneay a is non- linearity function, i.c., LeakyReLU used in GATConv (Veličković et al. (017)).
4

---

Under review as a conference paper at ICLR 2021
add MOrM
add nOrM
éeader Aipe
odd & norm
add & mone
Ar
entiourst uni--siontivee
modelr
10:0
MFP
Drnke
(a) Encoder Layer
(b) Graph Transformer
(c) Decoder Layer
Figure 2: Our Heterogeneous Graph Transformer architecture consists of set of encoders and decoders connected sequentially, in (b). Its encoder and decoder architectures are shown in (a) and (c), respectively.
4.3 HETEROGENEOU'S GRAPH TRANSFORMER (HGT)
Our model HGT adopts encoder-decoder structure similar to Britz al. (2017), with four encoder-layers in the encoder, and three decoder-layers in the decoder. It is flexible to adjust the number encoder and decoder layers.
Encoder. Prior to entering the stack of encoder-layers, the input node features are embedded into high-dimensional space with MLP. Within each encoder-layer, every graph node first aggregates the message (or information) from nodes of its kind through meta-paths. Note that a node (vari- able or clause) of bipartite graph has no direct connection within homogeneous nodes. Messages can only get passed among homogeneous nodes through mela-paths. We emphasize such type of communication between nodes of the same kind as self-attention, which implemented with ho- mogeneons attention mechanism. The weighted messages passed between variables and clauses through the tross-attention mechanism, implemented with the heterogeneous attention mechanism. The two types of attention connected through the residual block and layer normalization (Ba et al. (016)), as shown in Figure (a).
Decoder. Decoder consists of several decoder- layers. Inside each decoder-layer, there is cross- attention module followed by residual connection and layer normalization, as in Figure (c). The wetention-weighheed node features then fed into the MLP for dimension reduction.
4.3.
LOss EVALUATION
For given CSP(V, U), each combination of variable assignments corresponds probability. The original measure &(V, U)) is a non-differentiable staircase function defined on a discrete domain. ((V,U) evaluates to 0 if any Uy E U is unsatisfied, which disguises all other information includ- ing the number of satisfied clauses. For training purpose, differentiable approximate function is desirable. Therefore, the proposed model generates a continuous scalar output 2; [0, for each variable, and the assignment of each U; can be acquired through:
2
Lo.5 +
(4)
where is a small value to keep the generated v in {0, 1}. With continuous xy i 1,... N, we can approximate disjunction with mar(-) function and define o(-) as
M
6(E1,.., IN)
II max (1(x)) on E()))
Here, the literal function ((x, Csa) L- + e is applied to specify the polarity of each
variable. Inspired by Amizadeh al. 2019 smoothmar(()
replace the max function with differentiable
5
-1=1 Dee
(6)
Σ
eT
5

---

Under review as a conference paper at ICLR 2021
Mathematically, S, (11,,..,, ..,,,....... EN) converges max(Xi,.... 22) - However, since the assignment of each 2; is continuous and the threshold is 0.5, HGT doesn" need a strict max function to judge if clause contains literal with value 1. We note that 5 is enough for our model in practice. By maximizing the modified ø, HGT trained to find the optimal assignment for each CSP problem. For numerical stability and computational efficiency, we train HGT by minimizing the negative log-loss
M Σ ((((()) e gi))))
Cli uN) = -log(0)
During the training process, we realize that the value for each z; is trending towards 0.5 to minimize the loss function. We then append regularizer
r( r(ui, UM Σ ReLU((u 0.5)
to punish those clauses with values near 0.5, while allowing clauses with small values to increase. In this way, the regularizer encourages the value of each æ; to approach or 1, without disturbing the maximization of the values of clauses that is connected to.
5
EXPERIMENTAL EVALUATION
5.1 DATASET
In order to learn CSP solver that can be applied to various classes of satisfiability problems, we drew our training set from four classes of problems with distinct distributions: random 3-SAT, graph coloring, vertex cover, and clique detection.
Class
Distribution
Variables (n)
Clauses (m) / Edges (p)
Random 3-SAT
randa(n n. m.)
n2 100. 150, 200
[430, 645, 860)
k-coloring
color (N, N.P)
n x for (5 10
p = 50%
k-cover cover (N,))
n=(k + 1) N for N= 10F
N for N=
p 50%
k-clique
clique; (N.
n
220%, 10%
The summary of our chosen dataset. For random k-SAT problems, n and m refer to number of variables and clauses. For graph problems, N is the number of vertices, is the problem- specific parameter, and p is the probability that an edge exists.
Table 1:
For the random 3-SAT problems, we drew a total of 1200 synthetic SAT formulas from the SATLIB benchmark library (Hoos& & Stützle (2000)). These graphs consist of variables and clauses of various sizes, and should reffect a wide range of difficulties. For the latter three graph problems, we sampled 4000 instances from each of the distributions that are generated according to the scheme proposed in Yolcu & Póczos (011).. In particular, we tuned the problem-specific parameters for each set of instances assess our model's ability to generalize to other CSP problems. All formulas in our dataset, regardless of distribution, are satisfiable, and are encoded in DIMACS Conjunctive Normal Form (CNF), the natural format for SAT problems. Models trained on these graphs generalizes to other CSP problems, datasets, and larger graphs.
5.2 BASELINES
Baseline models. To assess the validity our model, we compared our framework against three categories of basclines: (a) the classic stochastic local search algorithm for CSP solving WalkSAT (Selman et al.), (b) the reinforcement learning- based CSP solver RLSAT Yolcu & Póczos (2019). (c) the generic but innovative neural framework for learning CSP solvers PDP (Amizadeh et al. 2 Among these baselines, PDP falls into the same category as the proposed model, which utilizes the one-shot algorithm.
Baseline setting. For the RLSAT and PDP baseline models, we strictly preserved their default parameters in order reproduce the original performances. Specifically, the RLSAT model was

---

Under review as a conference paper at ICLR 2021
color' (5, 0.5)
colorg
cover2
cover'
cliques
cliques
(10,0.5)
(5,0.5) 0.5)
(7.0.5)
(5, 0.2)
(10.0.1)
99.01% %
71.49%
93.78%
92.04%
95.72%
97.96%
RLSAT
-9.93%
200.92%
+12.12%
113766%
15..0%%
+12.3%%
Our Model
87.51 %
+ 1.45%
97.77% %
0.11%%
97.35% %
0.37 %
Table Our model's performance during training, compared to that of the baseline model RLSAT. We trained both models with 500 epochs on six distributions of graph problem sets. Within each cell, we present the metric of accuracy in the format of: [average accuracy [standaddd deviation %..
trained on their self-generated datasets via curriculum learning. For the PDP framework, we tested a fully neural CSP solver with weight decay = 10-10 and dropoul rale = 0.2.
5.3 EXPERIMENTAL SETTING
Software. The PyTorch implementation of our model is open-sourced, and the code is available at https://it.i/// Jo/J Our model employs Py Torchh Geometric (Fey & Lenssen (2019)) and is able to achieve high efficiency in both training and testing by taking full advantage of GPU computation resources via parallelism.
General setup. Our model for the experiments discussed in this section configured as follows.
Structures are implemented according to the architecture presented in Figure 2 For the encoder,
we adopted four encoder-layers with the number of channels set to {16, 32, 32, 32): for the de- coder, we adopted three decoder-layers with the number of channels set to {32, 16, 16). Optimizer Adam(Kingma & Ba (017)) with 31 0.9, 83 = 0.98, 10-9 was applied to train the model. Our learning rate varies with each step taken, and follows pattern that is similar to the one adopted by Noam Vaswani et al. (2017).
learning
B
(sttsssteemmm U.S step_num warmappstee sttpppsstesssttrpp -153
Specifically, our learning rate increases linearly for the initial warm-up steps, then gradually decay rate that is inversely proportional the square root of the step number. / is the coefficient used to adjust the scale of learning rate. To ensure fairness of comparison, we adopted dropout rate of 0.2 for regularization, which is the same value as Amizadeh al. (2019).
5.4 RESULTS AND EVALUATION
Validity of training. Table summarizes the performance of our model, compared to that of RL- SAT. For the training process of each model, we strictly followed the setting as explained in Section 5.2 and 5.3. Since our model adopts semi-supervised training strategy, and is capable of processing graphs of arbitrary size, we were able to combine numerous distributions of the same problem class into single dataset during training, regardless of the cooblem-specific parameters. We observed that our model's 's average accuracy is higher than that of RLSAT in all six distributions. For further analysis, present the holistic learning curves in Figure 3 where the shaded areas visualize the standard deviations of each model's validation scores. From the figure, we noticed that for the latter 100 epochs, RL-KC and RL-KV's validation performance start to oscillate significantly. Investigat- ing the characteristies of Reinforcement Learning, we discovered that RLSAT, upon encountering graphs with new scales, performs a whole new process of exploration. Therefore, RLSAT fails to generalize its leant experience to subsequent larger graphs, which results in an unstable validation score during training. In comparison, our model adopts highly paralleled message -aassing mech- anism, which updates all nodes of all graphs simultaneously at each epoch. As result, we are able to reach a high score rapidly, while maintaining the accuracy with little fluctuation.
We understand that the graph problems generated by RLSAT may not be sufficient in size and difficulty to fully assess the capability of our model. Hence, addition to testing on a diversified distribution of graph problems, we also experimented the validity of our model on the classic random 3-SAT dataset, and compared our results with that of PDP. As seen in Table 3 our model retains the ability to achieve high accuracy with little time required for processing each graph. In comparison, PDP takes a significantly longer time for validation, while reaching an average accuracy that fails to exceed ours.
7

---

Under review as a conference paper at ICLR 2021
randy 100, 430)
rand3 150, 645)
rands (200, 860)
Time (s)
Acc (%)
Time (8)
Acc (%)
Time (s)
Acc (%)
PDP
0.0743
96.51
0.0413
0..20
0,0915
93.65-10.62
Our Model
0.00368
1..28
0.00361
96.80 +
0.0128
16.59
Table 3:
Our model's 's performance during training, compared that of the baseline model PDP. We train both models with 1000 epochs on three distributions of random 3-SAT problems. We present the validation time of each graph, as well as the validation accuracy, which is in the format of: [average accuracy%] (standard deviation%].
Validition Curve
100
Our Model
184.3
Test Speed Magnitude
RDP
117.4
80
102
WalkAAT
89.2
63.2
71:9
40.2
47.7
47.3
-28.1
60
12.9
101
40
RL-KD
GT-RC
GT-KV
KQ
10a
kcolor
kcover
kclique
Rand-100
Rand-150
Rand-200
epoch
Figure 3: The learning curve HGT (GT) and that of RLSAT (RL). The z-axis measures the number of epochs trained. The y-axis measures the valida- tion score in percentage. Both models trained on (KC: color3(10, 0.5), KV: coverg(7,0.5)) 0.5), KQ: cliques (10, 0.1)3.
Figure 4: Our model's test speeds compared to those of PDP, with the speedup of WalkSAT the baseline metric. The x-axis indicates the six data distribution, upon which we test the mod- els. The y-axis measures the speedup of the models, w.r.t. WalkSAT's performance.
Efficiency of testing. Noting the discrepancy between the validation time, we further analyzed the efficiency of our model by measuring the time taken for each trained model to test on an individual graph. To diversify our test sets, we chose 2000 instances from each of the following distributions: (color3 0.5), covery(9, 0.5), cliquez (20, 0.05) }. as well as 100 instances from each of the random 3-SAT distributions: {randg(100) 430), randa (150, 645), rand3(200) (200,860)). Summarized in Figure 4 are the results we obtained from comparing the average test speeds of our model against that of PDP, with the performance of WalkSAT as the metric. As demonstrated in the figure, our model is capable of achieving higher average test speeds regardless of the graph structure. This observation can be explained by the fact that our model allows communication within homogeneous nodes, which provide all nodes with abundant semantic information when updating their states. Therefore, our model requires fewer iterations of message passing, and achieves greater efficiency.
CONCLUSION
In this paper, we proposed Heterogeneous Graph Transformer (HGT), a one-shot model derived from the eminent Transformer architecture for factor graph structures, solve the CSP problem. We defined the homogeneous attention mechanism based on meta-paths for the self-attention between literals or clauses, as well as the heterogeneous -ross-attention based on the bipartite graph links from literals to clauses, or vice versa. Our model achieved exceptional parallelism and accuracy on the factor graph form CSPs with arbitrary sizes. The experimental results have demonstrated the competitive performance and generality of //GT in several aspects. Future efforts in this direc- tion would include the extraction of high-level embeddings from HGT as well as the application of proposed algorithm to further aid classic CSP solvers solving combinatorial optimiza- tion problems. Our work also suggests the possibility of transforming classic techniques based on Conflict-Driven Clause Learning solvers to neural frameworks.
8

---

Under review as a conference paper at ICLR 2021
REFERENCES
Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. Learning to solve circuit-sat: An un- supervised differentiable approach. In International Conference on Learning Representations, 2018.
Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. Pdp: A general neural framework for learning constraint satisfaction solvers. arXiv preprint vrXiv:/903.00 00000,9999, 2019.
Forough Arabshahi, Sameer Singh, and Animashree Anandkumar. Combining symbolic expressions and black-box function evaluations in neural programs. arXiv preprint arXiv:1801.04535 2018.
Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey Hinton. Layer normalization. arXiv preprint arXiv:1607.06450, 2016.
Irwan Bello, Hieu Pham, Quoc V Le, Mohammad Norouzi, and Samy Bengio. Neural combinatorial optimization with reinforcement learning, arXiv preprint (:Xiv:6611.09900 2016.
Denny Britz, Anna Goldie, Minh-Thang Luong, and Quoc V. Le. Massive exploration of neural machine translation architectures. CoRR, abs/1703.03306, 2017. URL URL/http::/arxiv.orrg
abs/1703, 03906
Michael M Bronstein, Joan Bruna, Yann LeCun, Arthur Szlam, and Pierre Vandergheynst. Geomet- ric deep learning: going beyond euclidean data. IEEE Signal Processing Magazine, 34(4):18-42 2017.
Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? arXiv preprint /8Xiv:/802.0000 1802.8835, 2018.
Matthias Fey and Jan Eric Lenssen. Fast graph representation learning with pytorch geometric.
arXiv preprint 1903.v9903.0244 2019.
Holger H Hoos and Thomas Stützle. Satlib: An online resource for research sat. Sat, 2000: 283-292, 2000.
Elias Khalil, Hanjun Dai, Yuyu Zhang, Bistra Dilkina, and Le Song. Learning combinatorial op- timization algorithms over graphs. Advances Neural Information Processing Systems, pp. 3348-6358, 2017.
Diederik Kingma and Jimmy Ba. Adam: A method for stochastic optimization, 2017.
Vipin Kumar. Algorithms for constraint-satissactii problems: A survey, Al magazine, 13(1):32-32, 1992.
Bernhard Pfahringer. Conjunctive Normal Form, pp. 209-210. Springer US, Boston, MA, 2010. doi: 00007/978-00387-3116666 158. /RLp:ttss:///ot //t./////oo/o/////////oooooo 10. 10.1007/990 00000/978-10 -8711/9988-------888 301 30036-1648888 64-8
ISBN 978-0-387-30164-8,
Marcelo Prates, Pedro HC Avelar, Henrique Lemos, Luis C Lamb, and Moshe Y Vardi. Learning to solve np-complete problems: A graph neural network for decision tsp. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, pp. 4731-4738, 2019.
F. Scarselli, M. Gori, A. C. Tsoi, M. Hagenbuchner, and G. Monfardini. The graph neural network model. IEEE Transactions on Neural Networks, 20(1):61-80, 2009.
Bart Selman, Henry A Kautz, Bram Cohen, et al. Local search strategies for satisfiability testing.
Daniel Selsam and Nikolaj Bjømer. Guiding high-performance sat solvers with unsat-core pre- dictions. In International Conference on Theory and Applications of Satisfability Testing, pp- 336-353. Springer, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo Moura, and David Dill. Learning sat solver from bin supervision. arXiv preprint arXiv: 1802 032.03685, 2018.

---

Under review as a conference paper at ICLR 2021
Yizhou Sun, Jiawei Han, Xifeng Yan, Philip S Yu, and Tianyi Wu. Pathsim: Meta path- vath-based top-k similarity search in heterogeneous information networks. Proceedings of the VLDB Endowment, 4(L1):992-1003, 2011.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems, pp. 5998-6008, 2017.
Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Lio, and Yoshua Bengio. Graph attention networks. arXiv preprint vrXiv:1710. 10903, 2017.
Emre Yolcu and Barnabás Póczos. Learning local search heuristics for boolean satisfiability. In Advances in Neural Information Processing Systems, pp. 1992-8003, 2019.
Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec. G2sat: Learning to generate sat formulas. In Advances in neural information processing systems, pp. 10553- 10564, 2019.
10


Reviews:
[{"review_id": "zOLQVf2RLG", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 4, "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": "Summary: The paper \"Transformers satisfy\" presents an improved graph neural network model to solve SAT problems. Prior applications of GNNs to SAT have used convolutional GNNs instead of Graph Attention Networks (GATs), and this work suggests a modification of GATs to improve their performance on the bipartite graphs encountered in SAT.\n\nThe main part of the modification is that their GNNs consider up to two hops between nodes, such that variables can attend to other variables, and clauses can attend to other clauses. The paper then also suggests a way to allow \"cross-attention\" between clauses and variables.\n\nThe authors report moderate accuracy gains at predicting satisfiability on small synthetic SAT formulas.\n\nOn the positive side, the authors explore the use of \"meta-paths\", a way to exploit the bipartite structure to speed up the GNNs. But the authors do not contrast that with plain GATs applied to their problem so it is hard to say how much that idea contributes.\n\n\nMy concerns are as follows:\n- The paper claims to address constraint satisfaction problems (CSP), but focuses on SAT.\n- The paper claims to consider Transformers, but uses graph neural networks.\n- Evaluation done on very synthetic benchmarks. Does not necessarily carry over to other benchmarks.\n- Table 2 shows that the performance of their approach does not outperform their baseline in 2 out of 3 benchmarks. Table 3 shows moderate gains, but only on random SAT problems.\n- The motivation of the work is to improve the performance of neural networks on SAT problems, but I am not convinced that there is any perspective to beat CDCL solvers with neural networks at this problem.\n\n\nWriting style: The paper is understandable, but could be written better. Formulations in several places are unclear. For example:\n- Abstract: \"We define the heterogeneous attention mechanism based on meta-paths for the self-attention between literals, the cross-attention based on the bipartite graph links between literals and clauses.\" What does that mean? What are meta paths? What is cross-attention?\n- Introduction, first sentence: What does it help the reader to see only the claim that CSP is important. If you feel that SAT and CSP need motivation, please provide concrete applications.\n- Introduction: \"We apply the cross-attention mechanism to optimize message exchanges between heterogeneous nodes\" Most of the terms here were not yet introduced and I only understood this sentence after reading the rest of the paper.\n- The main contribution (Section 4.2) is not explained in detail, only the math is given and the reader has to reconstruct the motivation.\n\n\nMinor comment:\n- Check capitalization of references.", "extra_scores": {}, "extra_text": {}}, {"review_id": "eR39jNY49a", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 5, "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": "Summary of the paper:\nThe paper proposes a novel architecture called Heterogeneous Graph Transformers (HGT) to solve Constraint Satisfaction Problems (CSP) using unsupervised learning. Their model seems to achieve good results on classical problems encoded as CSP (3-SAT, k-coloring, k-cover, k-clique) with a few hundreds of variables and clauses, along with faster running time as compared to other contemporary methods because of a clause-parallel model architecture. The main contribution of the paper is to modify typical message-passing steps in graph neural networks to take more of the clause-variable structure into account, and accelerate message-passing in-between clauses and variables, respectively.\n\nStrengths:\n- A new approach to solving CSP using Graph Neural Networks/Transformers with some modeling improvements leading to reduced solution times and better success rate in finding satisfiable assignments.\n\nWeaknesses:\n- The experimental setup and results need significant improvements before this work can be published; see details in Questions below.\n\n- Writing: The motivating story in the introduction is not so clear-cut. There is a mention of previous work being limited to sequential algorithms, but no strong intuition is offered for why clause-parallelism is useful. Additionally, some key technical terms (e.g., \"cross-attention\", \"meta-paths\") are mentioned with little context, making it difficult for the reader to start grasping the paper's contributions early on.\n\n- Novelty: The attention mechanisms presented are very much similar to other attention mechanisms like Selsam et al. (2018). The use of transformer-type models is not uncommon, and was used prominently for TSP-type problems in this paper (which was not cited): Kool, Wouter, Herke van Hoof, and Max Welling. \"Attention, Learn to Solve Routing Problems!.\" International Conference on Learning Representations. 2018.\n\n\nRecommendation: \nThere are some positives to this work, particularly in the careful message-passing design. However, I have to recommend a Reject because the experimental results are very, very limited at this point. It is unlikely that the authors will be able to address all the issue I raise here, but I encourage them to do so in the near future and submit to future conferences.\n\n\nQuestions to the authors (in no particular order):\n1- Please show comparisons with a state-of-the-art optimization CSP solver such as IBM CPLEX's CP Optimizer or others.\n\n2- Test accuracy: Figure 4 only showcases the speedup achieved by the method compared to other approaches. Please report the test accuracy numbers (mean and standard deviation). Otherwise, the tables show only training results which does not tell the reader much.\n\n3- Homogeneous and heterogeneous graph attention: The distinctions between homogeneous and heterogenous graph attention is not clearly stated. The only distinction seems to be different sizes of the initial node (v in V) and edge (u in U) embedding sizes; v is of F_v dimension and u is of F_u dimension as opposed starting with same dimensions as in Velickovic et al 2017. Ideally, in heterogeneous attention, e_vi_uj and e_uj_vi should lead to different values. However, based on the definition in Equation (3), both of them will attain the same value. It would be nice if you can clearly state the differences.\n\n4- \"four encoder-layers in the encoder, and three decoder-layers in the decoder.\": how did you choose the numbers of layers here? Same question for all the hyperparameters described under \"General Setup\" in Section 5.3.\n\n5- Section 4.3.1 The definition of $l(x_i, e_{ia})$ after equation (5) is different from how $l(x_i)$ is used (with a single argument) in (5). What is the definition of $e_{ia}$? Also, can you clarify what you mean by \"is applied to specify the polarity of each variable\"? \n\n6- Table 3: the time difference with PDP is clearly implementation-dependent. Can you comment on the significance of these results? Also, it is impossible to guess how many learnable parameters PDP and your model have; can you add that information to the table? \n\nMinor:\n- \"The modern approach is trending to solve CSP through neural symbolic methods.\" --> \"One modern, trendy approach to solving CSP is through neural symbolic methods.\"\n- Unclear what this sentence means: \"Hence, the resulted model is bounded by the greedy strategy, which is generally sub-optimal.\"\n- \"The adjacent matrix\" --> \"The adjacency matrix\"\n- \"literals forming a partition different from\" --> \"literals forming a partition are different from\"\n- \"a highly paralleled message-passing\" --> \"a highly parallelized message-passing\"\n- Page 2 para 1, missing full stop in the last line.\n- Figure 2(b), the annotations \"Encoder\" and \"Decoder\" in the light blue boxes seem to be interchanged\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "aEk-FJxQmpZ", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 3, "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": "\n### Summary \n\nThe paper presents a model for inferring the solution of a constraint satisfaction problem over boolean variables expressed in *Conjunctive Normal Form (CNF)*. The proposed model builds on existing works which represent the factor graph of the CNF as a bipartite graph, and use a graph neural network for the learning task. It re-defines the graph to facilitate the message passing among the nodes which are in the same part of the graph (i.e. CNF variables/clauses). It also introduces a cross-attention mechanism between the nodes belonging to different parts. \n\nThe proposed model is evaluated on a set of benchmark SAT instances and is compared with an existing baseline method. \n\n### Strong points\n\n- The preliminary results are encouraging\n- The ideas seem to be novel, and there is a potential for impact\n- The paper is well-written and easy to follow\n\n### Aspects to be improved\n\n**Ablation study**: It seems that meta-paths can be applied without the attention mechanism. If this is the case, it should be clarified that to what extent the obtained results depend on the combination of both ideas. \n\n**Instance selection**: SAT instances vary significantly in terms of difficulty. It seems that the problem instances used in the experimental evaluation are all *easy* instances. I was not able to evaluate the difficulty of the instances from the dataset description. To have an estimate of the difficulty of the problems, I solved all instances in the *Random 3-SAT* class using the CDCL solver *MiniSAT* and obtained these runtimes:\n\n$$\n\\begin{array}{lrrr}\n\\textbf{problem class} & \\textbf{\\#instances} & \\textbf{total runtime} & \\textbf{average runtime} \\\\\\\\\nrand_3(100, 430) & 1000           & 0.709      & 0.00071   \\\\\\\\\nrand_3(150, 645) & 100            & 0.570      & 0.00570   \\\\\\\\\nrand_3(200, 860) & 100            & 6.171      & 0.06171   \n\\end{array}\n$$\n\nThese results indicate that the *Random 3-SAT* instances (especially the ones with 100 and 150 variables) are particularly easy SAT instances. The results of the experiments in the paper leads me to believe that the instances of other problem classes (i.e. $k$-coloring, $k$-cover, and $k$-clique) are also among the easier SAT instances. The reported accuracies in Tables 2 and 3 are quite high (both for the proposed method and the baseline). This indicates that there is room for including more challenging instances in the empirical analysis. \n\nNote that I am not suggesting that the learned models should compete with standard SAT solvers. I'm simply using standard solvers as a proxy to estimate the difficulty of the instances. The authors can use a similar approach to categorize a set of instances (e.g. a subset selected from a recent SAT competition) into different levels of difficulty (e.g. easy, medium, and hard). This will make the empirical analysis more reliable (and ideally further demonstrates the advantages of the proposed method). \n\n**Analysis and reporting**: \n\nThe space in the *experimental evaluation* section can be used more effectively. In contrast to the detailed description of the instances, baseline, and setup, the main results are aggregated into two small tables. I suggest spending this space on a more extensive empirical analysis. Moreover, the section and figure on *efficiency of testing* can be summarized in a few sentences. If the authors insist on presenting the inference speed as a merit of their proposed approach, they should identify instances where the solving time using a SAT solver is prohibitively long (certainly more than a fraction of a second). \n\n### Recommendation\n\nThe paper presents interesting ideas, which can potentially extend to domains beyond SAT solving. However, the proposed ideas need to be evaluated in a more extensive and rigorous empirical study. \n\n### Additional suggestions for improvement\n\n- An interesting question (which is for example studied by *RLSAT*) is the performance of models trained on one problem class when evaluated on another class. This is not a central question, yet would be a nice experiment to be included in an appendix. ", "extra_scores": {}, "extra_text": {}}, {"review_id": "3AGAZR5nJMW", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 4, "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 presents Heterogeneous Graph Transformer (HGT), a new architecture that combines useful properties of GNNs and Transformers to design HGT for combinatorial reasoning problems, particularly Boolean Satisfiability (SAT). The idea of combining these two powerful models is appealing. The motivation behind considering both homogenous attention (between two literals, or between two clauses) and heterogenous attention (between a literal and a clause) seems new and interesting too. However, there are several missing pieces in the paper in the present form, as outlined below.\n\nThe closest existing work, in terms of model architecture, appears to be Graph Attention Network or GATConv (2017). However, the first time this work is mentioned is quite late -- in section 4.2. I'm not sure why. I would have expected to see this relationship mentioned in the intro or related work sections. Without it, the proposal seems more novel than it actually is.\n\nI also find the title, Transformers Satisfy, too distant from the proposed technique, which is a combination of heterogeneous GNNs and attention mechanism, extending GATconv. Why the emphasis on Transformers? They are a particular way of using an all-to-all attention mechanism, which isn't quite what the proposed approach uses.\n\nSimilarly, the emphasis of the abstract and intro on solving CSPs too broad for what's supported in the paper. After the sentence \"A CSP can be formulated as a CNF formula\" on page 2, the rest of the formulation as well as all experiments are for the SAT problem. It would be better to frame the work as a new approach for *satisfiable* instances of SAT. It's ok to mention that it can be generalized to CSPs, but the focus is best left on SAT.  (I should note that even within SAT, the focus here is on 4 families of random instances, leaving out a whole universe of hand-crafted as well as application / \"industrial\" instances used to evaluate SAT solvers.)\n\nThe claim in the 2nd paragraph of the intro, that conventional CSP solvers rely on handcrafted heuristics and hence \"the resuling model is bounded by the greedy strategy, which is generally sub-optimal\" is misleading. It suggests that existing and proposed neural methods are closer to being optimal than conventional CSP solvers, which cannot be farther from the truth! The fact is, neural methods for CSP and SAT are one to two decades behind conventional solvers in terms of the scale of problems they can convincingly solve. It's an important research area, but not one that has yet even come close to conventional solvers.\n\nThe presentation is difficult to follow in places, as it leaves many important details unclear. E.g., section 3.3 tries to give an intuitive connection to Transformers, but relies on specific prior knowledge of queries, keys, similarity computation, etc., in transformers or attention mechanisms, which is left undescribed. I would suggest cutting down some standard details about CSPs or factor graphs, to instead focus on newer concepts.\n\nIn secion 4.3.1, the choice of v_i = floor(x_i / (0.5 + eps)) appears unusual and unnecessarily reliant on the parameter epsilon. Why not simply use v_i = floor(x_i + 0.5), the typical way to implement rounding?\n\nLater in that same section, I did not follow the intuition behind the regularizer term in Eqn (8). The motivation was to shift the value of each x_i away from 0.5 and towards either 0 or 1. Presumably it doesn't matter whether x_i goes towards 0 or towards 1, as long as the regularizer pushes it either way. How does the ReLU term achieve this?  (for one, it is asymmetric while the motivation was a symmetric move away from 0.5)\n\nIn the experiments, it's not clear what exactly are competing approaches trained on. Is it on the same distribution as the proposed model, or something else? Were any hyperparameters of baseline approaches tuned during training?\n\nI'm not sure what's the intended empirical support for the claim just before the start of 5.2, \"Models traind on these graphs generalize to other CSP problems, dataset, and larger graphs.\" Is there a particular experiment you are referring to?\n\nImportaintly, the experiment section is completely missing accuracy results on the Test set when comparing to RLSAT and PDP. Sure, training accuracy given some intuition, but it's impossible to judge the value of the method without comparing accuracy on unseen Test instances.", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper presents a new graph neural network (GNN) architecture with attention and with applications to Boolean satisfiability.

The reviewers expressed concerns over various aspects of the paper such as a need for better ablations and an analysis of the difficulty level of the SAT problems used in evaluation.  No rebuttal was provided.
Decision: Reject