There have been recent efforts for incorporating Graph Neural Network models for learning fully neural solvers for constraint satisfaction problems (CSP) and particularly Boolean satisfiability (SAT). Despite the unique representational power of these neural embedding models, it is not clear to what extent they actually learn a search strategy vs. statistical biases in the training data. On the other hand, by fixing the search strategy (e.g. greedy search), one would effectively deprive the neural models of learning better strategies than those given. In this paper, we propose a generic neural framework for learning SAT solvers (and in general any CSP solver) that can be described in terms of probabilistic inference and yet learn search strategies beyond greedy search. Our framework is based on the idea of propagation, decimation and prediction (and hence the name PDP) in graphical models, and can be trained directly toward solving SAT in a fully unsupervised manner via energy minimization, as shown in the paper. Our experimental results demonstrate the effectiveness of our framework for SAT solving compared to both neural and the industrial baselines.
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.