Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 3: Weak Reject
review_content: The paper presents an approach, PDP, to solve Boolean satisfiability (SAT) by decomposing it into Propagation, Decimation and Prediction, where each can be learned with a neural network.  

Strength:
-	The proposed approach makes sense to me and allows modularity.
-	The paper compares the approach to several prior works including the recent NeuroSAT and Glucose, a Conflict-Driven Clause Learning (CDCL) SAT solver for industrial problems. Surprisingly, NeuroSAT cannot handle the problems studied in this work. The proposed PDP performs similar to Glucose on the studied problems.
-	The paper is clearly written and seem over all solid.

Weaknesses:
1.	Comparison to prior work
1.1.	To allow a better comparison to prior work, I am wondering why the author did not compare in a setting and dataset prior work evaluated SAT solvers.
1.2.	It would be interest to know if and how the proposed model performs on the problems evaluated in Selsam 2019.
2.	The paper could be improved by including better ablations to understand where the strength comes from, specifically w.r.t. to the design choices of Propagation, Decimation and Prediction and the relation to Selsam 2019.

An overall solid paper, which could be improved by better comparison to prior work, by using setups used previously and better analyzed by providing clear ablations which allow better understanding the individual components of the system.
I am borderline on this paper, also given my limited knowledge of the field.


review_title: Official Blind Review #1

final_score: rating: 6: Weak Accept
review_content: The authors develop an unsupervised method for solving SAT problems. The method consists of an energy-based loss function which is optimized by a three-stage architecture that performs propagation, decimation, and prediction (PDP). The authors show that on uniform random 4-SAT problems, their PDP system outperforms two classical methods, a prior neural method, and performs favorably in comparison to a heavily developed industrial solver. Further, they show that a PDP system trained on modular 4-SAT problems performs better on modular 4-SAT problems that one trained on uniform random 4-SAT problems.

This well-written paper introduces an appealing unsupervised method for learning solvers for an important class of problems. Their results seem to be much stronger than the prior neural state-of-the-art, which also has the downside of requiring labelled data. The authors argue convincingly that although their method does not outperform Glucose, it still constitutes an useful advance in the use of neural methods for solving CSPs.

Overall, this seems to me like a useful contribution. Currently my accept recommendation is weak only because I'm not familiar enough with this area to verify that there are not other prior-work comparisons that should have been included.

Comments
The modular 4-SAT experiment is a bit underwhelming. This is not necessarily the fault of the learning algorithm: it may be that modular k-SAT problems are not the best setting to showcase the potential benefits of learning domain-specific solvers.

I don't often see field names such as "Machine Learning" and "Deep Learning" capitalized as they are in this paper.

Typos
In contract -> In contrast
N discrete variable X -> N discrete variables X?
review_title: Official Blind Review #2

final_score: rating: 1: Reject
review_content: This paper investigates the well-studied problem of solving satisfiability problems using deep learning approaches. In this setting, the authors propose a neural architecture inspired by message passing operations in deep probabilistic graphical models. Namely, the architecture takes as input a CNF formula represented as a factor graph, and returns as output a set of soft assignments for the variable nodes in the graph. The internal layers of the architecture consist of propagation, decimation and prediction steps. Notably, decimation operations take an important role in learning non-greedy search strategies. Besides PDP operations, the architecture incorporates parallelization and batch replication techniques. The learning model is trained in a non-supervised way, using a cumulative (discounted) log-likelihood loss that penalizes the non-satisfying assignments returned by the algorithm.  

Overall, the paper is relatively well-written and well-positioned with respect to related work. However, it is difficult to accept the paper in its current state: as explained below, it is difficult to understand how the PDP architecture effectively solves SAT problems, and experiments are not really conclusive. 

Although the idea of using general message-passing techniques for learning to solve SAT problems is relevant, the overall architecture left me somewhat confused. In the SAT problem, we have a CNF formula, say $F$, and the goal is to predict whether $F$ is satisfiable or not. In the former case, the solver is required to additionally supply a model of $F$, that is, an assignment of variables to values satisfying $F$. However, unless I missed something, the PDP architecture returns as output a set of $T$ “soft assignments” for each input SAT instance, which leads to two major concerns: 
* There is no final decision (SAT/UNSAT), so how can we predict the satisfiability of an instance $F$ with just a set of $T$ assignments? I guess that the PDP model will predict SAT (resp. UNSAT) if the resulting loss is small (resp. large) enough, but this is very unclear.
* Furthermore, the output set consists of “soft” assignments, as defined by (4). But a solver should return a "discrete" assignment mapping variables to values in $\{0,1\}$. So, how can we convert soft assignments to discrete ones? Are the authors using a rounding method? 

The experimental results are a bit confusing too. First of all, which generator has been used for random instances ($4$-SAT) and pseudo-industrial instances? For the sake of reproducibility, this should be mentioned in the revised version of the paper. Furthermore, it seems that at first sight, PDP is competitive with Glucose, as illustrated in the left part of Figure 1. Notably, the performance of Glucose degrades as the ratio $M/N$ grows. But this is not surprising because its timeout is set to 3s. However, the right part of Figure 1 is telling another story: apparently, Glucose can solve all instances in less than 10s. So, for the sake of fairness, it would be legitimate to report curves (left part) using 10s per instance: this would highlight the behavior of PDP with respect to modern SAT solvers on random instances using reasonable timeouts for the UNSAT part. The idea of making experiments on pseudo-industrial instances is interesting, but the PDP algorithm trained on those instances (i.e. PDP-modular) is rapidly degrading as the ratio $M/N$ increases. In fact, the difference between PDP-4SAT and PDP-modular is not statistically significant for UNSAT instances. Finally, Glucose is clearly dominating PDP on pseudo-industrial instances, as it can solve all instances with just a timeout of 2s per instance. 
review_title: Official Blind Review #3

Meta-review: The authors present a neural framework for learning SAT solvers that takes the form of probabilistic inference. The whole process consists of propagation, decimation and prediction steps, so unlike other prior work like Neurosat that learns to predict sat/unsat and only through this binary signal,  this work presents a more modular approach, which is learned via energy minimization and it aims at predicting assignments (the assignments are soft which give rise to a differentiable loss). On the other hand, at test time the method returns the first soft assignment whose hard version (obtained by thresholding) satisfies the formula.  Reviewers found this to be an interesting submission, however there were some concerns regarding (among others) comparison to previous work.  

Overall, this submission has generated a lot of discussion among the reviewers (also regarding how this model actually operates)  and it is currently borderline without a strong champion. Due to the concerns raised and the limited space in the conference's program, unfortunately I cannot recommend this work for acceptance.

Decision: Reject