Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.
review_content: 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.

They 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.
strengths_and_weaknesses: Strengths:
========
The paper is well-written and well-motivated and has a principled way of deriving the GNN architecture from BP. The 

Weaknesses:
===========

[Novelty:] 
The main issue with the paper is with the novelty of the proposed approach:
- The use of BP in the context of SAT has been extensively explored in the past but in a neural and non-neural fashion. 
- The Neural SAT solvers although not directly designing their model architecture from BP, implicitly perform similar type of computation as NSNet. 
- 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. 
- Obtaining a satisfying assignment from variable biases is not novel as NeuroSAT also extracts satisfying assignments by training on a single bit of supervision. 
- 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.

On 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. 

[Results:]
The 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.


[1]: Li et al., “Combinatorial optimization with graph convolutional networks and guided tree search”

[2]: Vaezipoor et al. “Learning Branching Heuristic for Propositional Model Counting” 

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
review_title: null

final_score: rating: 3: Reject: For instance, a paper with technical flaws, weak evaluation, inadequate reproducibility and incompletely addressed ethical considerations.
review_content: 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.
strengths_and_weaknesses: Strengths:

The paper proposes to learn NN models for solving SAT and #SAT with unsupervised learning.

Weaknesses:

The contributions are incremental. Combing GNN with BP is not new, and the losses to learning the model are not novel.
questions: 
(1) Please give in-depth discussions on how your work is different from existing works regarding model architecture and learning losses. 
(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.

[1] https://arxiv.org/abs/2205.04423
limitations: N/A.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: 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.
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.

Unfortunately 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.

Questionable 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.

Benchmarks: 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.

Comparison 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.

=========
Update 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.

I 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.
questions: Please respond to/refute the concerns raise in "strengths and weaknesses".
limitations: No immediate societal impact.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: 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.
strengths_and_weaknesses: Strengths:
1. 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.
2. The method of utilizing a novel GNN that parametrizes BP in the latent space to do marginal inference among all satisfying solutions is interesting.
3. The experimental results of NSNet in approximating model counting are promising.

Weaknesses:
1. 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.
2. No theoretical guarantee provided for the accuracy of NSNet in approximating the model counts.

Overall 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. 

For 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). 

Besides, 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. 

For 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. 
questions: 1. What is the reason to make NSNet-Sparrow less time-efficient than Sparrow?
2. Can NSNet be scalable to large SAT problems with thousands and millions of variables, such as the ones in SAT competitions?
3. How effective is NSNet in solving unsatisfiable problems?
4. 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.
review_title: null

Meta-review: metareview: This is a controversial paper. My thinking, however, is to largely agree with bWLw that the performance warrants publication even if that performance is largely due to details rather than major architectural innovation. I think that the overlap with Savari and Bortolussi is not a problem given the timing of the publication. The much smaller number of parameters compared to NeuroSAT and BPNN (see the response to Tesa) also seems significant. 
confidence: Less certain
Decision: Accept