NSNet: A General Neural Probabilistic Framework for Satisfiability Problems
Authors: Zhaoyu Li
Xujie Si
Venue: NeurIPS 2022 Accept (2022)
Keywords: satisfiability problems
model counting
graphical model
Belief Propagation
graph neural network
marginal inference
partition function estimation

Abstract: We present the Neural Satisfiability Network (NSNet), a general neural framework that models satisfiability problems as probabilistic inference and meanwhile exhibits proper explainability. Inspired by the Belief Propagation (BP), NSNet uses a novel graph neural network (GNN) to parameterize BP in the latent space, where its hidden representations maintain the same probabilistic interpretation as BP.  NSNet can be flexibly configured to solve both SAT and #SAT problems by applying different learning objectives. For SAT, instead of directly predicting a satisfying assignment, NSNet performs marginal inference among all satisfying solutions, which we empirically find is more feasible for neural networks to learn. With the estimated marginals, a satisfying assignment can be efficiently generated by rounding and executing a stochastic local search. For #SAT, NSNet performs approximate model counting by learning the Bethe approximation of the partition function. Our evaluations show that NSNet achieves competitive results in terms of inference accuracy and time efficiency on multiple SAT and #SAT datasets.

NSNet: A General Neural Probabilistic Framework for Satisfiability Problems
Zhaoyu Li Xujie Si
McGill University, MMila - Quebec Al Institute, *CIFAR Al Research Chair {zli199, xsi] mogill.ca
Abstract
We present the Neural Satisfiability Network (NSNet), a general neural frame- work that models satisfiability problems probabilistic inference and meanwhile exhibits proper explainability. Inspired by the Belief Propagation (BP), NSNet uses a novel graph neural network (GNN) parameterize BP in the latent space, where its hidden representations maintain the same probabilistic interpretation as BP. NSNet can be flexibly configured to solve both SAT and #SAT problems by applying different learning objectives. For SAT, instead of directly predicting a satisfying assignment, NSNet performs marginal inference among all satisfying solutions, which we empirically find is more feasible for neural networks to learn With the estimated marginals, satisfying assignment by rounding and executing a stochastic local search. For #SAT, NSNet performs approximate model counting by learning the Bethe approximation of the partition function. Our evaluations show that NSNet achieves competitive results in terms of inference accuracy and time efficiency multiple SAT and #SAT datasets [
be efficiently generated
1 Introduction
The Boolean Satisfiability Problem (SAT) and the Sharp Satisfiability Problem (#SAT, or model counting) are fundamental challenges for computer science, with numerous applications including software verification [9], hardware design [28 36), and planning [5] Although modern SAT and #SAT solvers have achieved practical success in these domains, the performance of satisfiability solvers heavily relies on custom search heuristics [8) However, designing good hcuristics is highly non-trivial and time-consuming, With the superior learning ability of neural networks, recent research on satisfiability problems has migrated from hand-engineered methods toward data-driven ones.
Various neural methods have been proposed for satisfiability problems [88] A line of research aims at building standalone neural solvers, which directly predicts the satisfiability 35 [0] or a satisfying assignment 22 31 of given instance. Other approaches integrate the neural modules into classic solvers, improving the branching heuristics SAT (34 or #SAT [42) solvers. Yet, despite recent progress, the interpretation of these neural networks still remains a mystery: why and how can neural networks learn to tackle satisfiability problems? Answering this question crucial for utilizing neural networks satisfiability problems, especially for designing better neural architectures.
This paper addresses the above question by developing an explainable neural framework that can be interpreted using graphical models. Specifically, we propose Neural Satisfiability Network (NSNet), novel graph neural network (GNN) framework taking the formulation of solving satisfiability problems as probabilistic inference. Inspired by the inference algorithm Belief Propagation (BP), NSNet adopts new graph encoding for propositional formulas and employs novel message passing mechanism that subsumes the BP's updating rules in the latent space. In such a manner, NSNet serves
Code available at http:///hhhto...oo///aaaaaa///e/
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

Porform frrm marginal infonnoo
X; 0.75
X;
X; 13=1
Fiatmatt the parittin finction
X3 0.50
Reand
X1
Intiliie
SLS Solver
X1
SAT
(Xg -ggiA
Dstmmttd manginal
soiggmeer
Seidfyigg
(X: v A
NSNet
V
Semmlaa
1.39 pariition flaction
In Z
# (Salisdying ussigumentss e
#SAT
Figure I: Overview of our pipeline for solving SAT and #SAT problems. For SAT, we apply NSNet to perform marginal inference and use the estimated marginals to guide the initialization of a SLS solver. For #SAT, NSNet itself can serve as an approximate solver by estimating the partition function.
neural extension of BP and allows the inference learn from data. Like BP, NSNet can estimate both marginals and the partition function of graphical models. This key observation makes NSNet an effective unified solution both SAT and #SAT problems (Figure I
Existing neural SAT solvers formula. However, there can be multiple satisfying solutions, making it unclear which particular solution should be generated. Instead of directly predicting a solution, NSNet performs marginal inference in the solution space of SAT problem, estimating the assignment distribution of each variable among all satisfying assignments. Although NSNet not directly trained solve a SAT problem, its estimated marginals can be used to quickly generate satisfying assignment. One simple way is to round the estimated marginals to an initial assignment and then perform the stochastic local search (SLS) it. Our experimental evaluations distributions show that NSNet's initial assignments can not only solve much more instances than both BP and the neural baseline but also improve the state-of state-of-the-art SLS solver find satisfying assignment with fewer flips.
aim to predict single satisfying assignment for satisfiable
the synthetic datasets with three different
To solve #SAT, we formulate it the partition function estimation of graphical models. NSNet learns the Bethe approximation of the partition function and thus acts as an approximate #SAT solver. Experiments on the BIRD and SATLIB benchmarks illustrate that method notably surpasses both BP and the recent neural approach. Compared with the state-of-the-at approximate #SAT solvers, NSNet estimate the solutions with more than three orders of magnitude speedup, while still achieving competitive precision.
Preliminaries
Satisfiability Problems. In propositional logic, a Boolean formula consists of Boolean variables and logical operators such as negations (-), conjunctions (A), and disjunctions (V). is typical to conjunction of clauses,
represent Boolean formulas in conjunctive normal form (CNF), expressed each which is a disjunction of literals (a variable or its negation). Given a CNF formula, the SAT problem asks whether there exists assignment to its variables that satisfy the formula, whereas the goal for #SAT is to count the number of all satisfying solutions.
Factor Graphs. A factor graph is bipartite graph with set of variable nodes connected to set factor nodes, where each factor node expresses the dependencies among the variables is connected. Let p denote distribution defined over discrete random variables and be possible assignment of the i-th variable X,. Then we may define the joint probability p(x) of an assignment {I1, T2, 2n.) using factors {f1. f2, ..... fm as:
II (a.)) Z 2 Σ m
m
[I
p(x) a
where each factor fa takes an assignment of its associated variables H, C x as input, Z is the normalization constant, which is also known the partition function.
In the case of satisfiability problems, each Boolean variable and clause in a CNF formula correspond to variable and factor node in a factor graph respectively. Given factor fo with its associated

---

clause a, the input 2a represents a possible assignment for the variables appears in clause and (x,) takes value I if z satisfies the clause and otherwise. By taking all factors into account, we derive that p(æ) ) = 1/2 if and only if the assignment satisfies the entire CNF formula, where the partition function Z indicates the number of all satisfying assignments. In other words, we can consider p(æ) as a probability measure on the space of all assignments that have a uniform distribution for all satisfying assignments and zero probability for unsatisfying ones.
Belief Propagation. BP is a variational inference algorithm to estimate the marginal distributions of variables the partition function Z in factor graph. It performs iterative message passing between neighboring variable and factor nodes. Specifically, at the k-th iteration, the variable to
factor messages m. mi+a (Iz) and the factor to variable messages m ma-s(
(A)
(R) (Ix²) are computed following:
(k) my mi-aa (1.)
II
(k-1) ma-i (x:),
(1) ((x)) E fa(w))
II JEN(a)
(k) m jzaa(())) (xz),
(EN())
where (i) and (a) denotes the neighbor nodes of node and node a respectively. BP iteratively updates these messages until convergence or reaching maximum number of iterations T. After this process, the variable beliefs (1();) and the factor beliefs (xra) ) can be computed to estimate the marginal distributions over the variables and the factors respectively:
(x:)) X II
m (T) (a:),
ba (a(a x fa(
II JEN(a)
m (z)))
(EN(()
Given the variable belief's and the factor beliefs, BP can calculate a variational approximation of the partition function Z. Such an approximation is derived as the Bethe free energy F In Z in statistical physics 77, which is defined as:
m
ba ba(ara) In bu(aa)
12
Σ C(N()) - Σ Inb(a))
(4)
Sa (x(a)
3 Methodology
In this section, we first rewrite standard BP to suit satisfiability problems with a probabilistic interpretation. Based on such a formulation, we introduce the graph encoding and message passing scheme of NSNet, which stands as a neural version of BP. By formulating SAT and #SAT as probabilistic inference tasks, we show how to utilize NSNet to solve these two problems.
3.1 Rewriting Belief Propagation for Satisfiability Problems
For numerical stability, BP can be performed in log space, and its messages can be normalized at every iteration. Note each factor fa can only take value I or 0 for satisfiability problems, thus we can remove the factor term in Equation and rewrite it as:
(z,) m ia
Σ cEN
(k-1) m m (x:),
m ( = LSE
Σ
m mjza (155) (
(5)
jEN(
LSE is the shorthand for the log-sum-exp function, and 2/ is the normalization constant for the variable to factor messages at each iteration. The subscript x; \ Iæ means to fix the value for the variable X; and enumerate other satisfying variable assignments clause a. Note the normalization
(k)
term 2i ensures that Ex,5(0.1) exp(m) (2:)) = while there is no such a normalization for (k)
m (z.). From the perspective of graphical models, there is probabilistic interpretation for the messages in Equation 5 [9: the variable to clause message (x,) can be interpreted as the log probability that X; takes value x; when clause is not considered and the clause to variable message (a-)((;,) represents as the log probability that clause a is satisfied when X; takes the value of a;- With this interpretation, BP performs message passing approximate these probabilities iteratively.
However, BP often makes inaccurate estimates or fails to converge for satisfiability problems due to complex logical structures. To improve the inference of BP on satisfiability problems, we propose Neural Satisfiability Network (NSNet), a novel GNN framework that extends BP in the latent space, allowing the inference algorithm learn from data.

---

3.2 NSNet Framework
Graph Representation. Inspired by the procedure of BP, we propose new graph representation for CNF for- mulas. As shown in Figure we represent formula as an undirected bipartite graph with one type of node for each variable assignment and another type of node for each clause. An assignment node and a clause node are connected the associated variable appears in the clause, The edges between them have two different types based on whether the clause can be satisfied using this variable assignment. Note that graph representation can exactly express each message in BP: the direct edges from an as- signment node to clause node represent the messages m4-sa (x:) and the edges from the other direction represent the messages (I,) Equation
G
x
Figure 2: Our graph representation of the CNF formula (Xi V V-X2) (X1 V Xa) (-Xi V X2 V Xa). X and X denotes variable X; takes values and respectively. The solid/dashed line indi- cates that the variable assignment satis- fies/dissatisfies the associated clause.
Message Passing Scheme. On top of our graph representation, we aim to design a learnable message passing scheme that parameterizes BP with neural modules. Formally, we define an embedding on every directed edge in the vector space Id the variable assignment to clause embeddings m;-+a (2,) and the clause to variable assignment embeddings (z;) Initially, we set all the embeddings of m; (zt,) and (x:+i to two learnable vectors h1 and h2 respectively. At the k-th iteration, these hidden representations are updated as:
(k) m i-t (x:) = Ai
Σ
m (k-1))
moii (x:)) m (x.)) = A2 (m (ma (x;): m ma x.)) (6)
m (k) (1;) = As
Σ m (K) m (x,z)
LSE an Aa
(aj
where A2, are all neural networks, which are parameterized by MLPs in our implementation. (k)
(k) mx;) the At each iteration, adopt the aggregation operators for updating m (2;) and m
same as BP in Equation 5, using summation for r ( and LSE operation for m a- (2x). (x)). The subscript x;,, \ I2 enumerates
of assignment to clause embeddings connected to clause except for the assignment v; and ensures that at least one embedding on a 'satisfying' edge is included during the enumeration. The edge embedding m (A)
1 (z:) is updated by incorporating both m (z;)
(k)
and its flip value's s m (1 - J.)) With the same aggregation strategy as BP, our framework can be viewed generalized BP algorithm that maintains the same probabilistic interpretation of BP and encodes these probabilities in the latent space.
Proposition 1. Our message passing scheme subsumes the BP algorithm, where BP is special case of our message passing.
If we set the feature dimension d to 1, and let the neural networks A₁ and As be the identity function, log(exp(a) + exp(b)) then the updating rules in Equation 6 is equivalent to Equation 5 Thus we can consider BP as oon-paramteeriee GNN and NSNet neural version of BP that generalizes in the vector space with learnable parameters.
Ag be the normalization function Az (a. b)
31,, NSNet defines latent representations on edges and performs message passing between neighboring edges rather than nodes. Such design also enables NSNet to enforce the permutation invariance and the negation cquivariance of CNF formulas [35]
In contrast to existing GNN architectures for satisfiability problems 35
22 10
Proposition 2. For any parameterization of h1, h2, Ai, A2 and As, the embeddings of NSNet is either invariant or equivariant to the following operations: (1) permute any variables. (2) permute any clauses. (3) permute any variables within clause. (4) negating every literal of a given variable.
Due to the space limit, we leave the explanation and proof of Proposition 2 in Appendix A.I

---

3.3 SAT Solving
We first show how NSNet can be used solve the SAT problem. Although any satisfying assignment is a valid solution to the SAT problem, we need to consider the following question carefully:
Question 1. If a neural network can predict satisfying assignment, how and why does the neural network produce one particular solution instead of other feasible ones?
Existing neural methods [22 10 3 employ neural networks to produce value E [0, 1] for each variable, where this value is regarded as a soft assignment and rounded to I or 0 as the actual assignment. Unfortunately, these approaches fail to answer Question I they are trained generate specific satisfying solution without considering other possible ones. As a result, neural networks are biased towards specific solutions during training and uncertain about which one to predict during testing, making their generalization ability poor.
To address this question, we leverage NSNet to perform marginal inference, i.e., computing the marginal distribution of each variable among all satisfying assignments. In other words, instead of solving SAT problem directly,
aim to estimate the fraction of each variable that takes or 0 in the entire solution space. Note the marginal for each variable takes all feasible solutions into account and is unique, which is more stable and interpretable to be reasoned by the neural networks. Similar to Equation 3 used by BP to compute variable beliefs, NSNet estimates each marginal value by (x; by aggregating the clause to variable assignment messages through a MLP and softmax function:
(x())) = MLP Σ
m (E
(T) m
[b.(1), (0) softmax ((..1),6:10))
(8)
To train NSNet to perform marginal inference accurately, we minimize the Kullback-Leibler (KL) divergence loss between the estimated marginal distributions and the ground truth. We use an efficient ALLSAT solver to enumerate all the satisfying assignments and take the average of them to compute the true marginals.
Now we consider how to generate a satisfying assignment after obtaining the estimated marginals.
Note that the marginal value b, (z;) for the variable X; represents the probability X, takes x; among all satisfying solutions, X, favors taking the value of I to satisfy a formula if (1) > 0.5 and vice versa. So one simple way is to round the marginal (;(1) for each variable to value x; [b,(1) 0.55 to produce an assignment. However, when each variable takes its favoring value independently. such an assignment may not satisfy the formula even if the estimated marginals are perfect. Therefore, we also perform the local search on this assignment until finding a satisfying one. In practice, we integrate NSNet with a SLS solver by modifying the solver's initialization under the guidance of our estimated marginals. Such a combination is easy to implement and has a modest overhead. It should be stressed that marginals are important in SAT solving as they represent the underlying distribution of individual variables. Besides using local search, one can adopt other methods such as decimation to generate a satisfying solution. We leave the discussion of other approaches in Appendix A.2
3.4 Model Counting
We also apply NSNet to the #SAT problem. Exact model counting is a well-known #P-Complete problem [%] and is almost infeasible without a search procedure. Due to its inherent complexity.
line of research focuses on studying approximate model counting [39 44 I1 37 244, where the goal is to count the number of satisfying assignments with certain tolerance at a lower computational cost. Similar to BP, we leverage NSNet to perform approximate model counting by learning the Bethe approximation of the partition function Z. Specifically, besides learning the variable beliefs by (ax)) using Equation g
we learn the factor beliefs (xx.) defined in Equation 3 by:
(xx.) = MLP
Σ m mi-sa (1zz) (aa))
(x..) ba (xx.)= - LSE (b.(2x))
(9)
jEV(a)
Then using Equation
4 the log number of all satisfying assignments can be estimated as:
In Z
ba (xx) In (2aa)
Σ ((V())) 1) Σ
(10)
5

---

NSNet subsumes the standard Bethe approximation with learnable estimations of variable and factor beliefs, making it standalone approximate #SAT solver. Unlike SAT which may have multiple satisfying assignments, the solution to a #SAT problem is unique value. We collect the ground truth value using a well-engineered #SAT solver and train NSNet by minimizing the mean square error between our approximation and the ground truth.
4 Experiments
We present the evaluation results in this section. In all experiments, we set the feature dimension d= 64 and message passing iteration T 10 for training. All MLPs have 3 hidden layers with 64 units each and use ReLU as the activation function. We ran all experiments on a server with single NVIDIA A100 GPU and 8 CPU cores. See Appendix[B.. [B. more implementation details.
4.1 SAT Solving
Experiment Setup. Following the experiment settings in recent works 231 we experiment using three synthetic SAT generators: SR [35], 3-SAT, and Community Attachment (CA) [17.. The original SR distribution is to generate a set of SAT/UNSAT pairs with only one different literal between the instances in each pair. In our setting, instances, so the unsatisfiable ones are discarded. For 3-SAT, we produce random 3-SAT satisfiable instances using CNFgen (26) at the region of the phase transition [13) CA is the pseudo-industrial generator that produces instances that mimic real-world problems with similar structures. For each distribution, we generate 50k satisfiable formulas with 10 to 40 variables and split them into training/ saanng/valinn validation/testing sets following 60%/22%%/20% proportions. To measure the generalizability of our approach, we further produce 10k larger formulas with the number of variables ranging from 40 to 200. The state-of-ther the-trterrtttr art ALLSAT solver bdd _iddimminta____ee all [4] is used to enumerate all satisfying assignments to obtain the ground truth marginals. More details are in Appendix B.2.1
perform marginal inference satisfiable
Evaluation & Baselines. We evaluate our approach for SAT solving in two metrics. The first one is the solving accuracy of the initial assignment obtained from the estimated marginals. We compare NSNet against BP and the neural baseline Ac [35]. NeuroSAT is the seminal work that designs a literal-clause graph representation for CNF formula and encodes the structure using similar gated graph neural network (GGNN) 277. Such a representation and neural network design are widely used in the following works 122
10 34 47). We train and evaluate NeuroSAT the same way as NSNet. For these two neural networks, we also examine the effectiveness of our training method against the seiiinmenttsupervviine cross-entropy loss of the predicted soft assignment and a certain satisfying solution. Glucose4 used to obtain such ground truth in this setting. Besides using T 10 message passing iterations, we further test the convergence of all methods by running for more iterations of message passing.
training strategy [47] 10, 22), which minimizes the binary
The second metric is the accuracy of a SLS solver with different initial assignments. For this metric, we experiment only on the large testing problems and choose the sfate-of-the-ae pure SLS solver Sparrow [6] as our base solver. We compare our hybrid solver against the Sparrow solver with different initialization strategies, which include the default initialization (random), BP, and NeuroS All SLS solvers are allowed to generate up to 100 assignments for each formula to ensure a fair comparison. Mean and standard deviations are calculated across 10 runs.
Main Results. Table ! shows our initial assignment results on the synthetic datasets using the number of iterations T' = 10. We can notice that NSNet with marginal supervision obtains the best performance across all distributions. Although our training objective not for predicting a single satisfying solution, simply rounding the estimated marginals makes both NeuroSAT and NSNet solve much more instances than that trained with the assignment supervision. It is consistent with our hypothesis that fitting on specific satisfying assignment without considering other possible ones would confuse the neural networks and thus lead to poor generalization. Note that NSNet is only trained on small instances, it is able to generalize to larger ones and outperform BP. Meanwhile, NSNet's performance exceeds NeuroSAT's by a large gap, which also demonstrates the advantage of graph representation and neural architecture.

---

Table 1: Solving accuracy (%) of the initial assignments on the synthetic datasets.
Same Distribution
Larger Distribution
Supervision
Method
SR
3-SAT
CA
Total
SR
3-SAT
CA
Total
N/A
BP
49.65
51.43
36.45
45.84
5.97
7.18
6.59
6.58
NeuroSAT
44.16
43.74
35.37
41.09
1.60
2.52
1,64
1.92
Assignment
NSNet
39.62
57.63
47.20
48.15
3.37
8.13
3.61
5.03
NeurOSAT
47.77
48,60
50.97
49.11
1.99
3.18
5,61
3.59
Marginal
NSNet
63.16
63.52
56.30
60.99
9.13
12.07
8.08
9.76
Tabel 2 illustrates the averaging solving accuracy with different numbers of iterations on both same- size and larger testing instances. Generally, most approaches can solve more problems with increased iterations of message passing. However, we can observe that the performance of BP hits saturation at 100 iterations and decreases a lot after then. We conjecture this because BP's belief's oscillate a lot with too many iterations, making it fail to converge. Instead, NSNet achieves higher accuracy as the iteration increases and outperforms both BP and NeuroSAT consistently.
Table 2: Solving accuracy (%) of the initial assignments with the increased number of iterations T on the synthetic datasets. Thes stands for the number of iterations achieving the best accuracy.
Number of Iterations (?')
Supervision
Method
20
100
200
500
Thes
N/A
BP
26.21
30.49
32,90
34.34
30.95
21.29
34.34
NeuroSAT
21.51
25.66
24.14
23.10
22.15
22.43
25.66
Assignment
NSNet
26.59
20.75
21.18
21.40
21.59
21.78
26.59
NcuroSAT
26.35
30.89
28.41
31.10
33.35
35.21
35.21
Marginal
NSNct
35.38
40.06
41.43
41.88
42.66
42.97
42.97
In Table 3 we present the performance of SLS solvers with different initialization methods. To reduce the extra overhead of querying models, we perform T = 10 iterations of message passing for BP, NeuroSAT, and NSNet. By rounding estimated marginals initial assignments, BP-Sparrow, NeuroSAT-Sparrov and NSNet-Sparrow significantly outperform the vanilla Sparrow on all distribu- tions. This fact suggests that marginals are helpful guide a local search procedure and enhance the SLS solver to find satisfying assignment efficiently. Among all initialization approaches, NSNet still performs the best. More experimental results for SLS solvers can be found in Appendix B.2.2 B..22
Table 3: Solving accuracy (%) for Sparrow with different initializations on the synthetic datasets.
Larger Distribution 3-SAT
Method
SR
CA
Total
Sparrow
8.77 + 0.15
11.48 + 0.26
54.25 + 0.23
24.83 0.08
BP-Sparrow
27.76 + 0.20
35.30
+ 0.31
84,89 + 0.19
49.32 - 0.11
NeuroSAT-Sparron
22.04 + 0.30
29.03
1 0.30
83.64
1 0.22
44.90 1: 0.18
NSNet-Sparrow
29.66 1 0.15
37.24
1 0.18
86.13 1 0.21
51.01 1 0.11
4.2 Model Counting
Experiment Setup. We first follow the experiment settings in recent work BPNN 24 Specifically, we run experiments using the same subset of BIRD benchmark (37]. which contains eight categories arising from DQMR networks, grid networks, bit-blasted versions of SMTLIB benchmarks, and ISCAS89 combinatorial circuits. Each category has 20 to 150 CNF formulas, which we split into training/testing with a ratio of 70%/30%. Note that the BIRD benchmark quite small and contains large-sized formulas with more than 10,000 variables and clauses, it challenges the generalization ability of our model. Besides evaluating in such a data-limited regime, we also conduct experiments on the SATLIB benchmark, an open-source dataset containing a broad range of CNF formulas collected
7

---

Rumtim
10 183
Matied
139 Solved Instances
Category
Figure 3: (Left) RMSE between estimated log countings and ground truth for each solver on the BIRD benchmark. (Right) Cactus plots of runtime for each solver on the BIRD benchmark.
from various distributions. To train our model effectively, we choose the distributions with at least 100 satisfiable instances, which include the following 5 categories: (1) uniform random 3-SAT on phase transition region (RND3SAT), (2) backbone- backbone-minimal random 3-SAT (BMS), (3) random 3-SAT with controlled backbone size (CBS), (4) "Flat" graph coloring (GCP), and (5) "Morphed" graph coloring (SW-GCP). The whole dataset has 46,200 SAT instances with the number of variables ranging from 100 to 600, and we split it into sniniig/validation/tssst BIRD and SATLIB benchmarks, we the state-of-the-art exact #SAT solver DSharp 3D) with time limit of 5,000 seconds to generate the ground truth labels. The instances where DSharp fails to finish within the time limit discarded.
sets with a ratio of 60%/220%/20%. For both
Evaluation & Baselines. Following BPNN 24 we use the (1) root mean square error (RMSE) between the estimated log countings and ground truth and (2) runtime as our evaluation metrics. We compare NSNet with BP, the neural baseline BPNN 24]. and two state-of-the art approximate model counting solvers, ACproxMC3 337 and F2 M. Akin to SAT solving, both BP and neural models are allowed to run with more iterations until the test metric converges. However, although we try to run BP more iterations to make it coverage, BP consistently fails to achieve comparable results on BIRD) and SATLIB benchmarks, and F2, we set a time limit of 5,000 seconds on each instance. See Appendix B.3. for additional setting details and results of these baselines.
only leave the other baselines for comparison later. For ApproxMC3
Main Results. As shown in Figure (Left) NSNet can estimate much tighter countings than BPNN and F2 across all categories of the BIRD benchmark. In total instances, NSNet's estimates are nearly three times preciser than F2's and BPNN's, with RMSE of 0.94. However, NSNet can not compete with ApproxMC3. whose overall RMSE is only 0.03. We also present the running time of each solver on the BIRD benchmark in Figure (Right). While ApproxMC3 can provide nearly perfect estimates, its time efficiency is undesirable: spends 123.33 seconds on average for 224 solved ones and fails to finish on the other 33 instances within 5,000 seconds. Unlike ApproxMC3 and F2 running sequentially on CPUs, BPNN and NSNet can run all 257 testing instances parallelly in batch on a GPU. NSNet is the most time- effeeefficient solver than other baselines, which takes only 4.83 seconds for all problems and 0.02 seconds for each. This demonstrates that NSNet significantly outperforms BPNN and F2 in terms of both the estimate accuracy and time efficiency, and gains more than three orders of speedups over ACproxMC3 while significantly reducing the accuracy gap between them. Additionally, the failure of BP proves that NSNet can leverage the inductive bias of neural networks to synthesize a better message passing algorithm rather than approximating BP.
Table 4 summarizes the performance of each solver on the SATLIB benchmark. We train BPNN multiple times but unsuccessfully make it converge on this dataset, so we discard its performance in the table. Compared with F2, NSNet can provide more precise estimates of the count- ings in much less time. ApproxMC3 still performs the best among all solvers by a large margin. However, it takes 13.05 seconds on average for each instance, while the number for NSNet is less than 0.01, which is more
Table 4: RMSE and average runtime for each solver on the SATLIB benchmark.
Metric
Method
RMSE
Runtime (s)
ApproxMC3
0.05
13.05
F2 NSNet
2.36
27.79
1.71
< 0.01
8

---

than three orders of magnitude faster than ApproxMC3, showing the efficiency of NSNet. More experimental results on the BIRD and SATLIB datasets can be found in Appendix
[.3.2 [33.2
Related Work
Neural Satisfiability Solvers. Using neural networks for satisfiability problems has been explored in the last few years. One common idea is to encode the input formulas using a GNN and perform downstream tasks based on the formulas' embeddings. Recent approaches mainly follow this pipeline and can be classified into two folds [8]: standalone neural solvers and neural-guided solvers.
Standalone neural solvers solve satisfiability task their own. NeuroSAT 35 and the following works [2 10] classify CNF formulas as satisfiable or unsatisfiable Simultaneously, these methods can also construct a possible assignment by decoding the literal embeddings. Several alternative approaches 2 31 focus on directly generating satisfying assignments. Such frameworks leverage different GNN architectures and apply an unsupervised loss for training. However, they all attempt to predict a single satisfying solution for each instance, which fails to consider other possible ones.
Although standalone neural solvers show some promising results, neither of these solvers is competi- tive with the ttate-of-the-al satisfiability solvers in terms of accuracy or scalability. Hence, another stream of research combines neural networks with modern satisfiability solvers, hoping improve some components of the existing solvers. These neural-guided solvers include NeuroCore (34 and #Neuro 4 which utilize neural networks guide the branching decisions of SAT and #SAT solvers. While these works successfully reduce the number branching steps, frequent invocation of neural networks is also required. By contrast, we call NSNet only once for both SAT and #S problems, which significantly diminishes the overhead of querying neural networks. For the SAT problem, AT 47 guides the initialization of SLS solvers by the soft assignments of neural networks, which is close to our work. However, they employ the neural architecture similar to NeuroSAT and train using a specific satisfying assignment, while NSNet trained estimate marginals. In addition, there are also some works 45 (55 leveraging reinforcement learning to learn the local search or branching heuristic of SAT solvers.
Neural Inference Algorithms. While BP serves as a non non-trainable inference algorithm, some recent works aim to develop learnable inference models, allowing inference to adapt from data. There are some efforts exploring the idea of enhancing BP with neural networks. In particular, (3 proposes NEBP, a hybrid inference method that augments BP by running GNN co-jointly. BPNN (4 and FE-NBP [40] focus on improving the updates of factor to variable messages by using a learned operator or a learned damping ratio respectively.
Several other methods devise end-to-end inference models beyond the procedures of BP. 46 is the seminal work apply GNN to estimate the marginals on relatively small, binary graphical models. FGNN [48] is another GNN model that parameterizes the Max-Product Belief Propagation and performs MAP (maximum posteriori) inference on factor graphs. Similar to the idea of generalizing BP. FE-GNN 40) leverages the tensor sum operator to the updates of GNNs, which combines factor potentials with message vectors in similar fashion BP. Nevertheless, these models are not designed for the case of satisfiability problems and fail to satisfy the negation equivariance of CNF formulas in Proposition 2 while NSNet identifies this property for satisfiability problems.
Discussion
Limitations. There are few limitations to NSNet. First, NSNet takes the formulation of solving satisfiability problems as probabilistic inference. However, such a formulation is defined for satisfiable instances but is not applicable unsatisfialle ones. Therefore, certificating unsatisfiability is beyond the scope of our work. Second, while NSNet can achieve good performance on both SAT and #SAT problems, it requires learning from labeled data, where the labels (especially the ground truth marginals) for hard instances can be time-consuning. Third, although NSNet serves as neural generalization of BP, it unclear whether there is guarantee of the estimated marginals and model counts provided by NSNet. We consider exploring the theoretical guarantee of NSNet as future work.

---

Conclusion. In this work, we present general neural framework for solving satisfiability problems as probabílistic inference. As learnable inference model, our framework leverages novel GNN architecture that subsumes BP in the latent space and performs marginal inference and partition function estimation solve SAT and #SAT respectively. Experimental evaluations on the synthetic datasets and existing benchmarks demonstrate that our approach significantly outperforms BP and other neural baselines and achieves competitive results compared with the state-of-the-ar solvers.
Acknowledgments and Disclosure of Funding
We thank the anonymous reviewers for their insightful comments. This work was supported, in part, by Individual Discovery Grants from the Natural Sciences and Engineering Research Council of Canada, and the Canada CIFAR Al Chair Program.
References
[1] Dimitris Achlioptas, Zayd Hammoudeh, and Panos Theodoropoulos. Fast and flexible proba- bilistic model counting. In International Conference Theory and Applications of Satisfiability Testing, pages 168-164, 2018.
[2] Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. Learning to solve circuit-sat, An unsupervised differentiable approach. In International Conference Learning Representations, 2019.
[3] Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. PDP: general neural framework for learning constraint satisfaction solvers. arXiv preprint arXiv: 999900009999 2019.
[4] Carlos Ansótegui, Jesús Giráldez-Cru, and Jordi Levy. The community structure of sat formulas. In International Conference on Theory and Applications of Satisfiability Testing, pages 410 423. Springer, 2012.
[5] Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27(01):184000,, 2018
[6] Adrian Balint and Andreas Fröhlich. Improving stochastic local search for SAT with new probability distribution. In International Conference on Theory and Applications of Satisfubility Testing, volume 6175, pages 10-15. Springer, 2010.
[7] Hans A Bethe. Statistical theory of superlattices. Proceedings the Royal Society of London. Series A-Mathematical and Physical Sciences, 150(871):552-575, 1935.
[8] Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185.
IOS press, 2009.
[9] Alfredo Braunstein, Mare Mézard, and Riccardo Zecchina. Survey propagation: An algorithm for satisfiability, Random Structures & Algorithms, 27(2):201-226, 2005.
[10] Chris Cameron, Rex Chen, Jason Hartford, and Kevin Leyton-Brown. Predicting propositional satisfiability via end-to-end learning. In Proceedings of the AAAI Conference on Artificial Intelligence, pages
2020.
[11] Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In International Conference on Principles and Practice of Constraint Programming, volume 8124 of Lecture Notes Computer Science, pages 200-216. Springer, 2013.
[12] Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in Syslem Design, 19(1):7-34, 2001.
[13] James M Crawford and Larry D Auton. Experimental results on the crossover point random 3-sat. Artificial intelligence, 81(1-2):31-57, 1996.
[14] Carmel Domshlak and Jörg Hoffmann. Fast probabilistic planning through weighted model counting. Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling, pages 243-252, 2006.
10

---

[15] Carmel Domshlak and Jörg Hoffmann. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research, 30:565-620, 2007.
[16] Matthias Fey and Jan Eric Lenssen. Fast graph representation learning with pytorch geometric. arXiv preprint 19X3::9903002228 2019.
[17] Jesús Giráldez-Cru and Jordi Levy. A modularity-based random sat instances generator. In Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015.
[18] Wenxuan Guo, Junchi Yan, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan, and Yaohui Jin. Machine learning methods in solving the boolean satisfiability problem. arXiv preprint arX7v:2203.04755, 2022.
[19] Franjo Ivančić, Zijiang Yang, Malay K Ganai, Aarti Gupta, and Pranav Ashar. Efficient sat-based bounded model checking for software verification. Theoretical Computer Science, 40563):256-274, 2008.
[20] Alexander Ivrii, Sharad Malik, Kuldeep S Meel, and Moshe Y Vardi. On computing minimal independent support and its applications to sampling and counting. Constraints, 21(1):41-5,, 2016.
[21] Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, and Moshe Y. Vardi. On computing minimal independent support and its applications to sampling and counting. Constraints, 21(1):41-58, 2016.
[22] Sehastian Jaszezur, Michal Luszezyk, and Henryk Michalewski. Neural heuristics for SAT solving. arXiv preprint arXiv:2005. /330:: 2020.
[23] Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint 14X1v:1412.6980, 2014.
[24] Jonathan Kuck, Shuvam Chakraborty, Hao Tang, Rachel Luo, Jiaming Song, Ashish Sabharwal, and Stefano Ermon. Belief propagation neural networks. Advances in Neural Information Processing Systems, 33:667-678. 2020.
[25] Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro. Can q-learning with graph networks learn a generalizable branching heuristic for a SAT solver? In Advances in Neural Information Processing Systems, pages
2020.
[26] Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. Cnfgen: A generator of crafted benchmarks. In International Conference on Theory and Applications of Satisfiability Testing, pages 464 473. Springer, 2017. 2017.
[27] Yujia Li, Daniel Tarlow, Mare Brockschmidt, and Richard S. Zemel. Gated graph sequence neural networks. Yoshua Bengio and Yann LeCun, editors, International Conference on Learning Representations, 2016.
[28] João P Marques-Silva and Karem A Sakallah. Boolean satisfiability in electronic design automation. In Proceedings of the 37th Anmual Design Automation Conference, pages 675-680, 2000.
[29] Marc Mézard, Giorgio Parisi, and Riccardo Zecchina. Analytic and algorithmic solution of random satisfiability problems. Science, 297(5582) 2002.
[30] Christian J. Muise, Sheila A. Mcllraith, J. Christopher Beck, and Eric Hsu. Dsharp: Fast d-dnnf compilation with sharpsat. In Canadian Conference Artificial Intelligence, pages 356-361, 2012.
[31] Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics. Goal-aware neural SAT solver. arXiv preprint 2rXiv:2106.07162. 2021.
11

---

[32] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward 7. Yang. Zachary Vito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems, pages 8024-8035, 2019.
[33] Victor Garcia Satorras and Max Welling, Neural enhanced belief propagation on factor graphs. In International Conference on Artificial Intelligence and Statistics, volume 130, pages 685-693. PMLR, 2021.
[34] Daniel Selsam and Nikolaj Bjørner. Guiding high-performance SAT solvers with unsat-core predictions. In International Conference on Theory and Applications of Satisfiability Testing, pages 336-353. Springer, 2019.
[35] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. In International Conference on Learning Representations, 2019.
[36] Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking safety properties using induction and a sat-solver. In International Conference on Formal Methods in Computer-Aided Design, pages 127-144. Springer, 2000.
[37] Mate Soos and Kuldeep S. Meel. BIRD: engineering efficient CNF-XOR SAT solver and its applications to approximate model counting. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 1592-1599, 2019.
[38] Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending sat solvers to cryptographic problems. In International Conference on Theory and Applications of Satisfiability Testing, pages 244-257 Springer, 2009.
[39] Larry Stockmeyer. The complexity of approximate counting. Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pages 118-126. ACM, 1983.
[40] Fan-Yo Yun Sun, Jonathan Kuck, Hao Tang, and Stefano Ermon. Equivariant neural network for factor graphs. arXiv preprint arXiv:2109.14216: 2021.
[41] Takahisa Toda and Takehide Soh. Implementing efficient all solutions sat solvers. Journal of Experimental Algorithmics (JEA), 21: 2016.
[42] Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris J. Maddison, Roger B. Grosse, Sanjit A. Seshia, and Fahiem Bacchus. Learning branching heuristics for propositional model counting. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 12427-12435 2021.
[43] Leslic Valiant. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3):410-421, 1979.
[44] Wei Wei and Bart Selman. A new approach to model counting. In International Conference Theory and Applications of Satisfibiliit Testing, pages 324-339. Springer, 2005.
[45] Emre Yolcu and Barnabás Póczos. Learning local search heuristics for boolean satisfiability. In Advances in Neural Information Processing Systems, pages 7990-8001, 2019.
[46] KiJung Yoon, Renjie Liao, Yuwen Xiong, Lisa Zhang, Ethan Fetaya, Raquel Urtasun, Richard Zemel, and Xaq Pitkow. Inference in probabilistic graphical models by graph neural networks. arXiv preprint arXiv: 1803.07710. 2018
[47] Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang Nlocalsat: Boosting local search with solution prediction. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, pages 1 1177-1183, ijcai.org, 2020.
[48] Zhen Zhang, Fan Wu, and Wee Sun Lee. Factor graph neural networks. In Advances in Neural Information Processing Systems, pages 8577-8587, 2020.
12

---

Checklist
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's
contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes] See Section 6
(c) Did you discuss any potential negative social impacts of your work? [N/A] We find potential negative impacts of work are generally indirect and hard assess.
(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
2. If you are including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? (Yes] See Section and Section 6
(b) Did you include complete proofs all theoretical results? [Yes] See Section 3.2 and Appendix A.]
3. If you ran experiments..
(a) Did you include the code, data, and instructions needed to reproduce the main experi- mental results (either in the supplemental material URL)? [Yes] Included in the supplemental material and GitHub.
(b) Did you specify all the training details (c.g., data splits, hyperparameters, how they were chosen)? [Yes] See Section 3 and Appendix [B.]
(c) Did you report error bars (e.g.. with respect to the random seed after running experi-
ments multiple times)? [Yes] See Section 4.1 and Appendix B.2.1
(d) Did you include the total amount of compute and the type of resources used (e.g., type
of GPUs, internal cluster, or cloud provider)? [Yes] See Section 4
4. If you are using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes] See Section
Section 4.2 and Appendix B.I
(b) Did you mention the license of the assets? [N/A]
(c) Did you include any assets either in the supplemental material URL? [Yes] Included in the supplemental material.
(d) Did you discuss whether and how consent was obtained from people whose data you'le 're
using/curating? [N/A]
(e) Did you discuss whether the data you are using/curating contains personally identifiable information offensive content? [N/A]
5. If you used crowdsourcing conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, applicable? [N/A]
(b) Did you describe any potential participant risks, with links to Institutional Review Board (IRB) approvals, if applicable? [N/A]
(c) Did you include the estimated hourly wage paid participants and the total amount spent on participant compensation? [N/A]
13


Reviews:
[{"review_id": "mS1reZaHCui", "reviewer": "Reviewer_n673", "summary": "The paper proposes NSNet, a novel graph neural network (GNN) framework taking the SAT solving problems as probabilistic inference problems. It proposes a new graph encoding for SAT formulas and employs a novel message passing mechanism to parameterize Belief Propagation in the latent space. Because of BP, NSNet can estimate both the marginals and the partition function of graphical models, which make it applicable to solve both SAT and #SAT problems. In particular, for solving SAT problems, NSNet can be trained in an unsupervised manner; for solving #SAT problems, NSNet is trained in a supervised manner.", "questions": "1. What is the reason to make NSNet-Sparrow less time-efficient than Sparrow?\n2. Can NSNet be scalable to large SAT problems with thousands and millions of variables, such as the ones in SAT competitions?\n3. How effective is NSNet in solving unsatisfiable problems?\n4. Is there any theoretical guarantee for the accuracy of NSNet in approximating the model count?", "limitations": "The authors point out two limitations of NSNet. One is that NSNet cannot be applicable to unsatisfiable problems. However, this limitation makes NSNet not practical for solving real-world problems. Because one of the important functionality of SAT solvers is to check the satisfiability for both SAT and UNSAT problems. The second limitation is that NSNet has to be trained with supervised learning. The authors point potential research direction for solving this limitation which is inspiring for future research.", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n1. The paper is trying to solve two important problems (i.e., SAT and #SAT) which can impact many fields in computer science such as security, verification, etc.\n2. The method of utilizing a novel GNN that parametrizes BP in the latent space to do marginal inference among all satisfying solutions is interesting.\n3. The experimental results of NSNet in approximating model counting are promising.\n\nWeaknesses:\n1. The experimental results of NSNet in solving SAT problems are not good enough for practical usage. In addition, NSNet is not applicable for unsatisfiable problems.\n2. No theoretical guarantee provided for the accuracy of NSNet in approximating the model counts.\n\nOverall the motivation of the paper is convincing. It is trying to solve two important problems that can impact various kinds of fields in computer science. The idea of utilizing GNN to do marginal inference among all satisfying solutions for solving both SAT and #SAT problems is novel. \n\nFor solving SAT problems, NSNet can be trained in an unsupervised learning fashion without requiring labels of the data samples. However, I cannot be convinced by the experimental results that NSNet can be a preferable choice comparing to classic SAT solvers. First, the benchmarks utilized in the experiment are only form SATLIB. However, the instances in SATLIB are the ones that are small and relatively easy to solve. As mentioned in the paper, the number of variables in these benchmarks range from 100 to 600. However, the benchmarks in the SAT competition and the ones produced by practical applications can easily have thousands or even millions of variables. In addition, the runtime results in the appendix show that the SLS solver Sparrow takes only 245.44 seconds for solving all 9,260 testing instances, with an average of 0.02 seconds to solve each instance. From the results, I can tell that these benchmarks are easy to solve. I would recommend to do the experiments on the SAT competition benchmarks which are the one experimented by the NeuroCore solver (Selsam, Daniel, and Nikolaj Bjørner. \"Guiding high-performance SAT solvers with unsat-core predictions.\" International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2019). \n\nBesides, the authors only show that NSNet can outperform the state-of-the-art solver Sparrow in the solving accuracy. In the real world, what users of SAT solvers really care about is the time efficiency. However, as shown in the appendix, the solving runtime of NSNet-Sparrow is less efficient than the SLS solver Sparrow. This makes the current state of NSNet not practical for real-world usage. \n\nFor approximate model counting, the experimental results show that NSNet is able to outperform the state-of-the-art approximate model counter ApprxoMC in time efficiency. This makes NSNet a promising approach to consider in approximating the model count for SAT problems. However, the drawback of NSNet is that the approximation accuracy is not as good as ApproxMC. Besides, only the average of the counting accuracy is shown in the experiment. It could provide the readers with more insights if the authors can also provide the minimum and maximum approximation accuracy. In addition, I wonder if the authors can provide any theoretical guarantees/proofs about the approximate accuracy. ", "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": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "h9Z1998LRi", "reviewer": "Reviewer_8cDU", "summary": "The paper proposes a neural model for the tasks of SAT and #SAT. For SAT solving, the paper proposes to learn marginal distributions and combine them with local search to get a feasible assignment. For #SAT, the paper learns the Bethe approximation of the partition function. Experiments verify the effectiveness of the proposed model.", "questions": "\n(1) Please give in-depth discussions on how your work is different from existing works regarding model architecture and learning losses. \n(2) Regarding learning losses, what new perspectives do we have? Simply applying existing/similar losses to learn a model is not good enough for NeurIPS. There is a similar work [1] that also uses the Bethe approximation of the partition function for #SAT.\n\n[1] https://arxiv.org/abs/2205.04423", "limitations": "N/A.", "rating": 3, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n\nThe paper proposes to learn NN models for solving SAT and #SAT with unsupervised learning.\n\nWeaknesses:\n\nThe contributions are incremental. Combing GNN with BP is not new, and the losses to learning the model are not novel.", "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": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "UNFTmXRHZYd", "reviewer": "Reviewer_bWLw", "summary": "This paper introduces NSNet, a GNN-style neural network approach to improve belief propagation (BP). GNN networks have previously been used for SAT, #SAT and QBF, but here it is paired with insights from the BP algorithm. The experimental evaluation demonstrates clear gains over the existing BPNN and F2 methods on #SAT in terms of prediction error and runtime. It also improves over NeuroSAT on plain SAT in terms of the number of solved instances. The paper also claims gains over ApproxMC3 which are not supported by the evidence.", "questions": "Please respond to/refute the concerns raise in \"strengths and weaknesses\".", "limitations": "No immediate societal impact.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Impact: This paper presents significant progress in cheap estimates of #SAT instances with belief propagation supported by GNNs, which is a strong result! The progress on plain SAT is probably irrelevant in practical terms, as there are much better exact SAT solvers. I also highly appreciate the clear statement on limitations of the approach.\n\nUnfortunately the paper includes some claims with respect to ApproxMC3 that I do not find convincing. I kindly ask the authors to carefully inspect these issues and either explain how I am wrong or revise the claims. The score I gave the paper reflect my current perception of the paper and I'd be happy to be proven wrong and will increase my score accordingly.\n\nQuestionable claim: \"This demonstrates that NSNet [...] gains more than three orders of speedups over ApproxMC3 at an acceptable cost of precision.\" This paper does not contain any evaluation about the impact of the precision loss on downstream applications, so calling them \"acceptable\" is not appropriate. Instead the authors should emphasize that they significantly reduce the accuracy gap between ApproxMC3 an the competing methods.\n\nBenchmarks: There are established #SAT benchmarks that are used for the evaluation of ApproxMC3. This paper does not even mention them, which is a serious omission, given the claims of gains over ApproxMC. Instead, the benchmarks chosen here are purely synthetic formulas. These synthetic formulas have no direct relation to #SAT as far as I can see, so I am even somewhat cautious about the comparison between BPNN, F2, and NSNet.\n\nComparison to ApproxMC: As far as I know, the ApproxMC solvers can be configured to achieve different trade-offs between speed and accuracy. The paper here appears to not consider that and instead claims gains in speed while trailing in accuracy. In other words, ApproxMC might be much faster if it is not forced to produce very exact results. I acknowledge that it might be hard to find an apples-to-apples comparison. But I believe that a better evaluation is necessary to support the claims made in the paper.\n\n=========\nUpdate after the rebuttal and discussion phase: The authors were able to address my concerns and I have to revise my view of the paper. The results on #SAT are pretty impressive. This is a method to quickly estimate the solution count of complicated formulas. Unfortunately the approach does not provide any guarantees on the accuracy, but this may still be very helpful in the field.\n\nI do not share the concerns about novelty raised by some other reviewers. While the method differs only in details from other published approaches, these details appear to be pretty important as the experiments suggest.", "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": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "TjSC86Nxmkz", "reviewer": "Reviewer_Tesa", "summary": "This paper provides a neural framework for SAT solving based on Belief Propagation. The authors propose a GNN architecture that captures BP in the latent space and they perform marginal inference using the trained model to obtain satisfying assignments for SAT. They also use the partition function estimation to approximately solve the model counting version of SAT, #SAT. The task for SAT is to find a satisfying assignment to problems that are known to be satisfiable. Equipped with this fact they manage to train the model in an unsupervised way by maximizing the log-likelihood of the model's prediction of being 1 (i.e., SAT). For #SAT they minimize the RMSE of model’s prediction and the true model count of a given formula.\n\nThey experimentally show that their approach outperforms vanilla BP and other neural approaches on SATLIB and BIRD benchmarks. For SAT they further experiment with initializing an SLS solver to obtain a true satisfying assignment.", "questions": "Given the close similarities between the proposed approach and some of the baselines used in the paper, it is interesting to have an intuitive explanation as to why NSNet achieves better results relative to other neural solvers, such as NeuroSAT and BPNN? Specifically a more thorough ablation and architectural comparison to BPNN is very welcome! Some example metrics to compare the models are number of parameters, number of inference time message passing iterations used for NeuroSAT and BPNN, etc.", "limitations": "See above", "rating": 5, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n========\nThe paper is well-written and well-motivated and has a principled way of deriving the GNN architecture from BP. The \n\nWeaknesses:\n===========\n\n[Novelty:] \nThe main issue with the paper is with the novelty of the proposed approach:\n- The use of BP in the context of SAT has been extensively explored in the past but in a neural and non-neural fashion. \n- The Neural SAT solvers although not directly designing their model architecture from BP, implicitly perform similar type of computation as NSNet. \n- Training the model for SAT in an unsupervised way using equation (9) is somewhat novel although the label of the instance still needs to be known a priori since the model is trained on only satisfiable instances. \n- Obtaining a satisfying assignment from variable biases is not novel as NeuroSAT also extracts satisfying assignments by training on a single bit of supervision. \n- Lastly initializing an SLS solver with neural predictions is also not novel and has been done by Li et al. [1] and others in the past.\n\nOn the #SAT front the use of variable biases and factor beliefs to predict the log of the model count of the given formula was also done by Kuck et al. in BPNN. \n\n[Results:]\nThe results are interesting and the proposed approach does indeed better on the chosen baselines in terms of solving accuracy of the initial assignments for SAT. When it comes to initializing the SLS solvers however, the results are more or less on par with vanilla BP (BP-Sparrow vs. NSNet-Sparrow). For #SAT, the authors use BPNN and ApproxMC3 (among others) as baselines and show superior RMSE wrt. BPNN and better runtime wrt. ApproxMC3 on BIRD benchmark. A criticism to approximate neural #SAT solvers, which also applies to BPNN, is that unlike ApproxMC3 and other probably approximately correct (or PAC) counters, they do not provide any guarantees that the results fall within a confidence interval of the true model count. This makes runtime comparison to ApproxMC3 unfair and limits the use case of these types of solvers, unlike [2] which improved the heuristic of an exact solver. Having said that NSNet clearly beats the BPNN on these benchmarks which is an interesting result.\n\n\n[1]: Li et al., “Combinatorial optimization with graph convolutional networks and guided tree search”\n\n[2]: Vaezipoor et al. “Learning Branching Heuristic for Propositional Model Counting” \n", "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": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept