PDP: A General Neural Framework for Learning SAT Solvers
Authors: Saeed Amizadeh
Sergiy Matusevych
Markus Weimer
Venue:  (2020)
Keywords: Neural SAT solvers
Graph Neural Networks
Neural Message Passing
Unsupervised Learning
Neural Decimation

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

Under review as a conference paper at ICLR 2020
PDP: A GENERAL NEURAL FRAMEWORK FOR LEARN- ING SAT SOLVERS
Anonymous authors Paper under double-blind review
ABSTRACT
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. 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 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.
INTRODUCTION
Constraint satisfaction problems (CSP) (Kumar 1992) and Boolean Satisfiability (SAT), in partic-
ular, are the most fundamental NP-complete problems in Computer Science with a wide range of applications from verification to planning and scheduling. There have been huge efforts in Computer
Science (Biere et al., 2209aa Knuth 2015; Nudelman et al.) 2004: AAsóótguui et al.) 2008 2012
Newsham et al.) 2014) as well as Physics and Information Theory (Mezard Montanari, 2009
Krzakala et al. 2007) to both understand the theoretical aspects of SAT and develop efficient search algorithms to solve it. Furthermore, since in many real applications, the problem instances are often drawn from narrow distribution, using Machine Learning to build data-driven solvers which can learn domain-specific search strategies is a natural choice. In that vein, Machine Learning has been used for different aspects of CSP and SAT solving, from branch prediction (Liang et al. 2016) to algorithm and models rely on carefully- craffted features, more recent methods have incorporated techniques from Representation Learning and particularly Geometric Deep Learning (Bronstein et al., 2017 2019) to capture the underlying discrete structure of the CSP (and SAT) problems.
selection (Xu et al., 2008 Hutter et al., 2011). While most these
Wu et al.
Along the latter direction, Graph Neural Networks (Li al. 2015 Defferrard et al. 2016) have been
the cornerstone of many recent deep learning approaches to CSP e.g., the NeuroSAT framework (Selsam et al. 2019), the Circuit-SAr AT framework (Amizadeh et al. 2019). and Recurrent Relational Networks for Sudoku (Palm et 2018). These frameworks have been quite successful in capturing the inherent structure of the problem instances and embedding it into traditional vector spaces that are suitable for Machine Learning models. Nevertheless, a major issue with these pure embedding frameworks is that it is not clear how the learned model works, which in turn begs the question whether the model actually learns to search for a solution or simply adapts to statistical biases in the training data. As alternative, researchers have used deep neural networks within classical search frameworks for tackling combinatorial optimization problems e.g. Khalil et al. (017)). In these hybrid, neuro-symbolic frameworks, deep learning is typically used to learn optimal search heuristics for generic search algorithm e.g. greedy search. Despite the clear search strategy, the performance of the resulted models is bounded by the effectiveness of the imposed strategy which is not learned.

---

Under review as a conference paper at ICLR 2020
In this paper, take middle way and propose neural framework for learning SAT solvers which enjoys the benefits of both of the methodologies above. In particular, we take the formulation of solving CSPs probabilistic inference (Montanari et al., 2007; Mezard & Montanari] 2009 Braunstein et al., 2005] Grover et al., 20188 Gableske et al. 2013) and propose a neural version of that is capable of learning efficient inference strategy (i.e. the search strategy in this context) for specific problem domains. Our general framework is design pattern which consists of three main operations: Propagation, Decimation and Prediction, and hence referred as the PDP framework. In general, these operations can be implemented either as fixed algorithms or as trainable neural networks. In this light, PDP can be seen as probabilistic inference in the latent space, and as a result, is somewhat straightforward to establish how the search strategy in the neural PDP works, unlike pure embedding methods. On the other hand, due to the distributed nature of its decimation component, PDP is nol restricted by the greedy strategy of the classical decimation process, meaning that it can potentially learn search strategies which are not greedy. And this would distinguishes it from the neuro-symbolic methods that are defined within the greedy strategy. Furthermore, we propose an unsupervised, fully differentiable training mechanism based on energy minimization which trains PDP directly toward solving SAT via end-to-end backpropagation. The unsupervised nature of our proposed training mechanism enables PDP to train on (infinite) stream of unlabeled data.
Our experimental results show the superiority of the PDP framework compared both oftte-f--the-rtt neural and inference-based solvers. We further demonstrate our model's capability in adapting to problem distributions with distinct structure which is common in industrial settings. Lastly, we take an ambitious step further and compare our neural framework against the well-known class of Conffict-Driven Clause Learning (CDCL) industrial solvers. Despite the fact that neural solvers (including ours) are still in their infancy and not really comparable to industrial SAT solvers, we were pleasantly surprised to see that our trained models could come close to the performance of the CDCL solver. This is significant in the sense that it shows that even though our neural model at this point lacks some powerful classical search techniques such as backtracking and clause learning, its adaptive neural constraint propagation strategy is nevertheless very effective.
2 RELATED WORK
Classical Machine Learning has been incorporated in solving combinatorial optimization problems
(Bengio et al.] 20188) and SAT in particular: from SAT classification (Xu et al. (2012), and solver
selection (Xu et al. 2008) to configuration tuning (Haim & Walsh, 2009 | Hutter et al. 2011 [iingh
al. 2009) and branching prediction (Liang et al. 2016]] Grozea& & Popescul 2014 | & Blaschko 2012). However, more recently, researchers have used Deep Learning to train full-stack solvers.
There are two main categories of Deep Learning methodologies proposed recently. In the first category, neural networks are used to embed the input CSP instances into a latent vector space where a predictive model can be trained. Palm et al. (2018) used Recurrent Relational Networks to train Sudoku solvers. Their framework relies on provided solutions at the training time opposed to framework, which is completely unsupervised. Selsam et al. (2019) proposed to use Graph Neural Networks (Li et al., 2015) to embed CNF instances for the SAT classification problem. They also proposed to use a post post-processing clustering approach to decode SAT solutions. In contrast, our method is fully unsupervised and is directly trained toward solving SAT. Amizadeh al. (2019) proposed a DAG Neural Network to embed logical circuits for solving the Circuit-SAT problem. Their framework is also unsupervised but it is mainly for circuit inputs with DAG structure, Prates et al. (018)) proposed a convolutional embedding based method for solving TSP.
In the second category, neural networks are used to learn useful search heuristies within an algorithmic search framework- typically the greedy search /Vinyals et al.] 2015) Bello et al.) 2016 Khalil et al., 2017), branch-and-boum search (He et al., 2014)) or tree search (Li et al.] 2018). While these methods enjoy a strong inductive bias in learning the optimization algorithm well some proof of correctness, their effectiveness is essentially bounded by sub-optimality of the imposed search strategy. Our proposed framework effectively belongs to this category but at the same time, its performance is not bounded by any search strategy.
Our framework can also be seen as learning optimal message passing strategy on probabilistic graphical models. There have been some efforts in this direction (Ross et al. 2011 Lin et al.) (013) Heess et al. 2013 Johnson et al. 2016 Yoon et al. 2018), but most are focused merely message
2

---

Under review as a conference paper at ICLR 2020
passing, whereas our framework learns both optimal message passing and decimation strategies, concurrently.
3 BACKGROUND
Constraint Satisfaction Problem, denoted by CSP C), aims finding an assignment to a set of N discrete variables X = {z, E I..N] each defined on a set of discrete values X' such that it satisfies all constraints C = (ca (a a E 1..M). Here, da is subset of variable indices that constraint depends on; similarly, by 0i, we denote the subset of constraint indices that variable i participates in. Each constraint Ca x210aa + {0, 1) is Boolean function that takes value 1 iff aa satisfies the constraint Ca. In this paper, we focus on Boolean Satisfiability problem (SAT) where the variables take values from X' {) and each constraint (or clause) is disjunction of subset of variables or their negations.
Furthermore, any CSP instance CSP(X. C) can be represented a factor graph probabilistic graphical model (X,(X, C. (Kollr et al. 2009). A factor graph IF X, C) is a bipartite graph where each variable z; corresponds to a variable node in IFG and each constraint Ca corresponds to factor node in IGG. There is an edge between the i-th variable node and the a-th factor node if i E da. Then, one may define a measure on FG as:
1 Z
P(X)
II da (x.a))
(1)
where da are the factor functions such that dha = max(ca (3 for some very small, eo e. Z is the normalization constant. In the special case of SAT, we extend the FG representation by assigning a binary &ia E {-1, 1} attribute to each edge such that 6sa = -1 if variable x; appears negated in the clause ca. and eio otherwise. This way the factor functions take the same functional form (i.e. conjunction) independent of the factor index a; that is, Qa (Daaa) = ox eau). where eaa all the edges connected to the a-th factor.
Using this formalism, the solutions of the original CS, C*) correspond to the modes of P(X). Given FG C), one can compute the marginal distribution of each variable node by probabilistic inference on the factor graph using the Belief Propagation (BP) algorithm (aka the Sum-Product algorithm) (Koller al. 2009). But the actual optimization problem be solved by computing the max-marginals of P(X) via algorithms such as Max-Product, Min-Sum (Koller et al. 2009) and Warning- [Braunstein al. 2005).
All of the above algorithms including BP can be seen as special cases of the General Message Passing (GMP) algorithm on factor graphs (Mezard & Montanari, 2009). where the outgoing messages from the graph nodes are computed as deterministic function of the incoming messages in an iterative fashion. If GMP converges, at the fixed-point, the messages often contain valuable information regarding variable assignments that maximizes the marginal distributions and eventually solve the CSP. In particular, the basic procedure to solve CSPs via probabilistic inference is (1) run a specific GMP algorithm the factor graph until convergence, (2) based on the incoming fixed-point messages to each variable node, pick the variable with the highest certainty regarding a satisfying assignment, (3) set the most certain variable to the corresponding value, simplify the factor graph if possible and repeat the entire process over and over until all variables are set. We refer to this process as GMP- GMP-guided sequential decimation or decimation for short. The most famous algorithms in this class are BP-guided decimation (Montanari et al. (007)) and SP-guided decimation, based on Survey Propagation (SP) (Aurell al. WW05Chhavas et al. 2005).
4 THE PDP FRAMEWORK
In order to develop neural framework for learning to solve SAT, first we need a suitable design pattern that would allow solving SAT via neural networks. To achieve this, we introduce the Propagation- Piopagation-Decimaatin.
(PDP) framework. The PDP framework can be as the generalization of the GMP-guided sequential decimation procedure described in previous section, where certain restrictions relaxed. In particular:
3

---

Under review as a conference paper at ICLR 2020
(A) In the GMP-ggiddd sequential decimation, decimation step is executed only after GMP is converged. We relax this requirement in PDP by interleaving propagation and decimation steps.
(B) In sequential decimation, at each step, only one variable is fixed (i.e. the one with the highest certainty). But as it is shown in Chavas et al. (2005), this is not necessary and multiple variables can be set concurrently in a fully distributed fashion. We follow this pattern and let the decimation step occur concurrently across the factor graph without any centralized selection procedure.
(C) In the classical decimation procedure, decimation refers to "fixing" variable node to a certain value. In PDP, we relax this requirement in two ways: (1) we let the decimation step happen at the message-level (i.e. on the edges) rather than at the variable-level (i.e. on the nodes), and (2) instead of fixing the message on an edge to certain value, the PDP's decimation step simply intercepts the propagator messages and transform them in a stateful manner. Note that almost all GMP-guided decimation algorithms can be expressed in terms of the PDP design pattern but not the other way around. For example, in the classical case, the decimation process is greedy by definition; whereas in PDP, that restriction has been lifted. Even though our proposed framework is versatile enough to tackle any type of CSP, in this paper, we focus on the SAT problem.
Messages: In the PDP framework, at each time step I, there are four messages defined on each edge (t) (i, a): the propagator messages in each direction, Pi-a and p(") Pa-ii and the decimator messages in each direction: i- and d a->s These messages are real vectors in latent space R
This step defines how the propagator messages on the edges get updated given the incoming decimator messages from the previous step. In particular for each edge (i, a), we have:
Propagation Step:
P. L ((((d) es.) : b E di (i\)a) at) -.-.. L
2 (((d) Eag) : E da (i))
(2)
where V and Nr, are general (neural network) sel functions parametrized by the parameter vectors and y, respectively. Similar to Amizadeh et al. (2019). in our implementation, we have used Deep Set functions (Zaheer et al. 2017) to model L and L y. It should be emphasized that both L and I, are stateless functions that compute the outgoing propagator messages merely based on incoming decimator messages and the corresponding edge attributes.
As mentioned before, in PDP, the decimation step simply consists of transforming the messages generated by the propagation step on each individual edge. Moreover, in principle, the effect of decimation usually goes beyond one iteration, which means that the decimator needs to keep a memory of how transformed the same message in the previous iterations. In other words, the decimation step is inherently stateful. Therefore, we define the decimation step as a stateful function that calculates the decimator message on each edge based on the propagator message on the same edge as well as the decimator message at the previous iteration:
Decimation Step:
d (p!" Cia ) di2,, T (p Gia e- Here 4, and a are recurrent neural network units (e.g. LSTM or GRU (Chung et al. 2014)) parametrized by parameter vectors V and w, respectively.
(3)
Prediction Step: At any point during the ieneaattoo-decimatto process, the model can be queried to produce the most likely (soft) assignments for the variable nodes in the factor graph. This is done via the prediction step which produces variable assignments based on the incoming decimator messages to each variable node as well as the corresponding edge attributes; that is,
(4) where I c is another deep set function neural network parametrized by the parameter vector Ç. In the SAT problem, we use the Sigmoid function as the last activation layer of I to generate soft assignments for Boolean variables.
T- ([((( exx) : be Oit)
The tuple M = (Ls. V Φ Pw, T&) fully specifies the PDP model. Algorithm illlsstraees the interplay of the PDP's three steps in the forward path. Note that the train time, the forward computation returns back one set of assignments per each iteration step - i.e. total of Tmax sets of soft assignments. This is mainly done for the loss computation purposes, as shown in the next section. At the test time, however, the iteration loop terminates as soon satisfying assignment is found (Line 13 in Algorithm T]. In order to check whether a soft assignment is SAT, we first
> 0.5) on soft assignments to get the hard Boolean apply the thresholding function 5 (z: = [zx (t) assignment for each variable.
4

---

Under review as a conference paper at ICLR 2020
Finally note that, at first sight, the PDP frame- work bears a resemblance to the NeuroSAT model in (Selsam al. (2199) in the sense that both methods produce latent representations on bipartite graph via some notion of "message passing". Nevertheless, we would like to em- phasize that these methods different. In NeuroSAT,, the latent representa- tions are defined per each node and represent the node embeddings of the bipartite representa- tion of CNF, whereas in PDP, latent vectors represent messages per each directed edge. Also, the message passing in NeuroSAT refers to the process proposed in Li et al. (2015) for graph embedding, whereas in our framework, message passing refers to belief propagation the factor graph graphical model.
Algorithm 1: The PDP Forward Computation
input: Factor graph IG(X, C)) and Tmaz
Randomly initialize p pi-.a Pa- d da for t = to Tmar do // Propagation ion step
(0) (0)
foreach (i,a) E (G C* do
fundamentally
L Compute Pi Pa using Eq.
(4) (t)
// Decimation step foreach (i,a) E (G C*) do
L Compute d o-ه using Eq.
(3
// Prediction step
10
for i 1 to N do L Compute using Eq. (4)
X + {z, : 1..N Testing and 8 (xx(1) SAT then return (1)
13
Parallelization and Batch Replication: Our implementation of PDP in PyTorch is embarrass- ingly parallel: every inner loop in Algorithm runs concurrently on all the edges/nodes of the input factor graph. Furthermore, parallel pro- cessing of multiple input factor graphs in single batch is straightforward in PDP: we simply concatenate all the instances batch into one large factor graph and treat the result as one CNF for- mula with multiple independent clauses. Using this powerful trick allows us to solve many examples simultaneously on GPU.
14
15 return (x(1) : :LEL 1..T Maaz
Furthermore, batch parallelization can be also used to expedite the search in single problem scenarios. Note that a CSP may have many solutions and which one of them is found by PDP depends on the random initialization in Line 1 of Algorithm I Therefore, at the test time, single example in the batch multiple times knowing that each replica will be initialized by different random values; then, the iteration loop terminates one of the replicas. This process, referred as batch replication, enables the solver to simultaneously search different parts of the solution space for single problem.
replicate each
as the solver finds solution for least
TRAINING PDP SAT SOLVER
In order to train PDP model M to solve SAT problems, would ideally like to reward the model outputs that have high probability regarding the measure in Eq. (T). As a result, one can train M by maximizing the probability of the model output w.r.. the model parameters. Instead, more numerically stable method aims at minimizing the negative log-likelihood aka the energy function:
E(X) log P(X) log Z
Σ log (x Caa)
(5)
Nevertheless, ob-) is not differentiable function soft assignments which cannot directly fed into Φ(-). To resolve these issues, for training purposes only, define differentiable proxy to the original Φ(-). In particular, in the SAT problem, Φ(-) should encode the logical disjunction on soft assignments. One possible differentiable formulation is the smooth max function proposed by Amizadeh et al. (2019)
defined it in Section Moreover, M produces
Eisdo (l (aeee//((x,,,,,, ((x,,
if eio Ij - otherwise
Smaz (F Cdu)
where ((1,, Psa)
(6)
Eieon e((x,e1a)/7
is the literal function, and is the temperature parameter. Similar to Amizadeh et al. (2019)
start the training at high temperature and gradually anneal toward 0. By doing so, we effectively let Smaz() (-) start off as the arithmetic mean function and gradually turn into the max(.) (-) function, which is the equivalent of logical disjunction on soft assignments. order to mimic the behavior of disjunction even further, we use the smooth Step function to enhance the contrast of the Smax
5

---

Under review as a conference paper at ICLR 2020
output by pushing the soft assignment values to the extremes depending whether they are below 0.5 or above
Gx(z) x
x)
where K. > 1 is constant. Using Eqs. (6) finally we can define our smooth proxy for Φ(-)
((Daa, eda) Gx (Smaz (Daaa Eaa)) Given this proxy, we define the loss function for the example [G C) as the discounted accumulated energy over Tmax iterations:
(x(FG(X,)) = t=1
(l E(X(1)
(8)
where [x(()) :t 1..Tmax] } is the output of model M according to Algorithm I and 0 < A < 1 the discounting factor. The idea here is the model is penalized more if produces non-SAT assignments further down the iteration loop. Finally, we note that using this loss function, our training methodology is completely unsupervised; that is, it does not need SAT solutions the training time nor does it need SAT/UNSAT binary labels. And yet, the proposed mechanism directly trains the PDP model toward solving SAT. In that respect, our framework is very different from the NeuroSAT framework (Selsam al. 2019) where solver is built indirectly via training binary SAT classifier.
EXPERIMENTAL RESULTS
We have compared our PDP framework against three different categories of baselines: (a) the classical probabilistic inference based techniques for SAT solving, (b) the state-of-the the-art neural embedding SAT solver and (c) a CDCL industrial SAT solver, as follows
SP: Survey-propp propagation guided decimation (Mezard & Montanani 2009) is one of the most effective inference- based algorithms to approach random uniform k-SAT problems in the hard SAT region.
Reinforce: Unlike PDP, the decimation process in SP is sequential. Not only can this slow down the search but also it restricts the search the greedy strategy. To address these issues, Aesues,(Caavas [Chavas al.) (2005) have proposed fully distributed version of SP called the Reinforce Algorithm.
NeuroSAT: Ae (Selsam et al. 2019) is the state-of-the-art neural method based on learning a SAT classifier.
Glucose (Audemard Simon 2018 a popular Conflict- Clause Learning (CDCL) SAT solver for industrial problems (Biere et al. 2009b whose basic techniques have become common practice for many modern SAT solvers.
Glucose:
Of these baselines, SP and Reinforce are implemented using the same PDP platform. All the PDP- based methods as well as NeuroSAT take a maximum iteration number (i.c. Tmaz) which controls the timeout budget; in our experiments, explicit timeout policy since it does not support controllable iteration number.
have set Tmax 1000. For Glucose. have incorporated
In experiments, the dimension of the message space (h) is set 150. The deep functions a. y, and Iç are implemented according to the formulation in Theorem 2 in Zaheer et al. (207)) where p and are each 2-layer Perceptrons. The decimator functions 4g and Φ, are implemented as GRU cells. The LogSigmoid function is used for all internal non-linearities. We have used the Adam optimizer with learning rate of 10-4 and gradient clipping with norm 0.65 to train our model. We have also enforced weight decay of 10 as well as dropout with rate 0.2 for regularization. These are picked using grid-search on training dataset with smaller variable sizes (up to 20) over 5 epochs. For NeuroSAT, we have used the default settings proposed in /Selsa et al. (2019).
6.1 UNIFORM RANDOM S-SAT
Uniform random k-SAT problems (where each clause in the input CNF has exactly k literals and is selected uniformly from a set of variables) have been studied in depth in Combinatorial Optimization,
We have provided our PyTorch implementation accompanied by detailed documentation and the config files for the neural PDP as well the PDP-hased SP and Reinforce baselines in the supplemental materials.

---

Under review as a conference paper at ICLR 2020
100
1.00
SP
Reintorce
Guease
7.5
8.5
8.5
PDP
NeveSAT
10'
PSB Ce--ar
ren-a
20
10-3
7.0
7.5 8.0
8.5
5.0
0.5
10.0
7.5
0.5
9.5
1.
M.N
MIN
Figure 1: (Left) The ratio of the uniform 4-SAT problems solved versus a. The green vertical lines indicate the theoretical phase transition thresholds for uniform 4-SAT as N + oc. (Right) The accuracy and time for Glucose vs. PDP (parallel), PDP (serial) and PDP (serial with batch replication) on uniform 4-SAT. All PDP methods were run up to 1000 iterations, whereas Glucose was let to solve all the problems without time restriction.
Statistical Physics and Coding Theory (Mezard & Montanari 2009). In particular, researchers have rigorously identified four different phases of complexity most random k-SAT problems go through as the ratio of clauses variables (known as a M/N) grows: the eplica-symmetti (RS) phase (aka the easy SAT phase), the dynamical phase, the condensation phase and finally the UNSAT phase (Krzakata et al., 2007).
Since the training strategy in Section 5 is fully unsupervised, at the training time, we simply generate a stream of unlabeled examples in memory to train a PDP SAT solver. For the training examples, we let the size of each clause in CNF varies randomly between 2 and 10. Also the a value for each CNF varies between 2 and 10, while the number of variables N is chosen uniformly between 4 and 100. This guarantees that training stream will contain all ranges of problems in terms of complexity. Training of NeuroSAT, on the other hand, is based on training of a supervised SAT/UNSAT classifier which not only does need binary labels, but also imposes striet training regime to avoid learning superfluous features, as described in Selsam et al. (2019). As a result, we have adopted the same regime to generate offline training data for NeuroSAT. Nevertheless. we were not able to train a NcuroSAT classifier for problems with more than 20 variables, even when we increased the model capacity. Therefore, the NeuroSAT model only trained with instances of 4 to 20 variables instead.
Training:
Results: We have generated test datasets of uniformly random satisfiable 4-SAT problems (each with 100 variables) with various a values according to the process described in Mezard & Montanari (2009) chapter 10. In particular, for any given value of a., a dataset of 500 SAT examples has been generated where all examples in the dataset have roughly the same a value. This process was then repeated for different values of a to cover all the aforementioned phases. Figure [[ett) shows the results of rumning the models on the 4-SAT test datasets. All the PDP-based models well as NeuroSAT are run for Tmax = 1000 iterations. This would translate to 3s per example timeout threshold for Glucose. As the plot shows, NeuroSAT model could not solve any of the problems even though its underlying SAT/UNSTT classifier reached a small training error. We suspect this might be due to the fact that were not able to train NeuroSAT on larger problems and the fact that it is not directly trained to solve SAT to begin with. Our neural PDP method, on the other hand, significantly outperformed the SP and Reinforce algorithms signifying the importance of learning compared to classical (fixed) inference methods. Moreover, within the 3s timcout budget for Glucose. our framework performs as par with Glucose This may not seem fair because unlike Glucose, PDP processes multiple examples in a batch each time. To further investigate this, we have let Glucose to go beyond 3s timeout limit and compared it against the original parallel PDP, its serial version and its serial version augmented by batch replication (each run for 1000 iterations). Figure Right shows the accuracy and time comparison results. From this plot, we can see that: (1) the serial versions of PDP cannot beat Glucose, (2) Glucose can eventually solve all the problems in the datasets if given opportunity to go beyond 3s budget, and (3) batch replication significantly improves the accuracy of neural PDP while time overhead is roughly similar that of serial PDP. The latter observation is
7

---

Under review as a conference paper at ICLR 2020
82-
62-
20
5.0
5.5
6.0
5.5
7.0
7.5
0.0
8.5
M/N
Figure 2:
The ratio of the modular 4-SAT problems solved versus a for Glucose and the two PDP solvers trained on uniform and modular random 4-SAT.
crucial because shows combined with batch replication, PDP can achieve even higher accuracy within limited time budget. This further shows the potential of combining pure neural framework with classical restart mechanism, which is introduced to PDP via batch replication.
6.2 PSEUDO-INDUSTRIAN RANDOM k-SAT
As mentioned earlier, one of the main goals of incorporating Machine Learning in combinatorial optimization is to arrive at generic, data-driven solvers that adapt to different problem domains. Nevertheless, the neural SAT solvers proposed in the literature so far are mainly trained on uniform random k-SAT problems. This begs the question whether neural solvers domain-specific information inherent in a narrow problem distribution. To this end, in this section, go beyond uniform k-SAT and focus problems that exhibit distinct structures. In particular, consider pseudo-industrial random SAT problems with highly modular structures (Newman) (2006). This is mainly motivated by the fact that real industrial SAT problems highly modular (Ansótegui et al. 2012). To generate such problems. we have incorporated the Community Attachment (CA) model proposed in Giráldez- Cru & Levy (2016).
capable of picking up
Training: We have trained two neural PDP models with the same exact architecture and capacity as the one in the previous section. The first model has been trained on a stream of uniformly generated 4-SAT problems with the number of variables ranging from 5 to 100. The second model, however, trained on a stream of pseudo-industrial industrial random 4-SAT problems generated according to the CA model. Each random example in the CA stream has between 10 to 20 communities with modularity factor Q between 0.8 and 0.9. note that the Q value does not typically go beyond 0.3 for uniform k-SAT problems (Ansótegui et al. 2012).
We have tested both the trained PDP models as well as Glucose on the datasets of modular 4-SAT problems generated with the same setting the modular training data for different values of a the CA model in Giráldez-Cri & Levy 2016). Figure 2 shows the performance these models grows. Each point in the plot represents dataset of 200 modular examples with the corresponding a value. The PDP models are run for Tmaz 1000 iterations which translates to 2s per example timeout budget for Glucose. As the plot shows, Glucose beats the PDP volv by solving all the problems for all a values within the time budget. This is somewhat expected as CDCL solvers have been shown to exploit the modular structure (Newsham al.) [014 Giräldez-Cri & Levy 2016) and as a result perform very well on real-world industrial problems. However, among the neural PDP models, the one that has been trained on modular A-SAT problems perform significantly better than the one trained on uniform 4-SAT problems. This is an important result because classical message passing inference algorithms (like SP) work reasonably well the underlying graph is locally tree-like (Mezard & Montanari 2009), which holds for uniform random k-SAT problems as + 2c, but does not generally hold for non- non-unine uniform random graphs. Nevertheless, the neural PDP still learn efficient. domain-specifi specific inference strategies. This indicates that the neural PDP framework has the potential to adapt to domains beyond uniform random AAS and be used as a generic yet adaptive solver.
Results:
8

---

Under review as a conference paper at ICLR 2020
We also note that the gap between the two models shrinks for high a values. This phenomenon can be explained as follows: intuitively, in modular formulas, solving each module (which is roughly a uniform k-SAT) is a necessary (not sufficient) condition for solving the entire formula; this means that the hardness of individual modules puts lower bound on the hardness of the formula. This is not problematic for medium-range a and the gap between the PDP trained modular problems and the uniform PDP is significant (~ 20%). But, for high a's, since the lower bound is already pretty high, it would effectively make modular problem as hard uniform problem of same a for message- passiin decimation algorithms and as result the gap between the two models shrinks.
7 CONCLUSIONS AND FUTURE DIRECTIONS
In this paper, proposed the neural PDP framework for learning neural SAT solvers. Unlike recent methods in the literature which are based on learning efficient embeddings, our framework can be interpreted as a non-trivial neural extension of probabilistic message passing and inference techniques on graphical models and as such its search strategy can be viewed in the probabilistic terms. Furthermore, proposed fully unsupervised training procedure based the idea of energy minimization on graphical models to train PDP toward solving SAT. Due to its unsupervised nature, this training mechanism enables us to train PDP on an (infinite) stream of unlabeled problem instances generated in real-time. This is in stark contrast with strict supervised training mechanism taken by some recent frameworks such as NeuroSAT. This also opens the door the further question of how to generate unlabeled training streams for efficient training in specific domains.
We also note that PDP as a general design pattern is powerful idea on its own as it allows many classical message passing algorithms such as SP, BP and Reinforce to be reformulated in terms of fully parallel framework which can be run on GPUs. Moreover, the general PDP framework does not require its components to be necessarily neural. This gives rise to hybrid neuro-symbolic solvers where some components of the model are learned while others are fixed (e.g. using a SP propagator with neural decimator). We leave the exploration this aspect of PDP to the future work.
Since neural PDP actually learns an inference algorithm, it can find multiple solutions for an input problem depending on its messages' initial values. This further gives rise to the idea of batch replication which in turn introduces the classical notion of restarts in the PDP framework. In this direction, important future work is to investigate ways of introducing other classical search techniques used in CSP solvers, specifically backtracking and clause learning.
Our experimental results on k-SAT problems showed the effectiveness of the PDP framework compared to neural and industrial baselines. In particular, we saw that not only did PDP outperform classical baselines but it also came close to the well-known Glucose solver. Moreover, we showed that PDP can go beyond uniform problems and adapt to pscudo-industrial problem domains with prominent modular structures. Finally, we would like to emphasize that neural PDP is still far from claiming victory over the industrial solvers. However, the fact that our PyTorch prototype could outperform other classical and neural solvers and come close an industrial solver reveals the huge potential in pursuing this direction, especially regarding translating other classical search techniques used CDCL and other industrial solvers into neural frameworks such as PDP.
REFERENCES
Saced Amizadeh, Sergiy Matusevych. and Markus Weimer. Learning to solve circuit-SAT: An unsupervised differentiable approach. In International Conference on Learning Representations, 2019.
Carlos Ansótegui, María Luisa Bonet, Jordi Levy, and Felip Manya. Measuring the hardness of sat instances. In AAAI, volume 8, pp. 222-228, 2008.
Carlos Ansótegui, Jesús Giráldez-Cru, and Jordi Levy. The community strueture of sat formulas. In International Conference on Theory and Applications of Satisfiability Testing, pp. 410-423. Springer, 2012.
Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools,
2018.

---

Under review as a conference paper at ICLR 2020
Erik Aurell, Uri Gordon, and Scott Kirkpatrick. Comparing beliefs, surveys, and random walks, In Advances in Neural Information Processing Systems. pp. 49-56, 2005.
Irwan Bello, Hieu Pham, Quoe V Le, Mohammad Norouzi, and Samy Bengio. Neural combinatorial optimization with reinforcement learning. arXiv preprini arXiv:161 1.09940, 2016.
Yoshua Bengio, Andrea Lodi, and Antoine Prouvost. Machine learning for combinatorial optimization: methodological tour d' horrrizon. arXiv preprint 1811. 1.1128, 2018.
Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009a.
Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. Conflict-driven clause learning solvers. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pp. 131-153, 2009b.
Alfredo Braunstein, Marc Mézard, and Riccardo Zecchina. Survey propagation: An algorithm for satisfiability. Random Structures & Algorithms, 27(2):201-226, 2005.
Michael M Bronstein, Joan Bruna, Yann LeCun, Arthur Szlam, and Pierre Vandergheynst. Geometric deep learning: going beyond euclidean data. IEEE Signal Processing Magazine, 34(4):18 42, 2017.
Joel Chavas, Cyril Furtlchner, Mare Mézard, and Riccardo Zecchina. Survey-propagation decimation through distributed local computations. Journal of Statistical Mechanics: Theory and Experiment, 2005(11 1) P1: 1016, 2005.
Junyoung Chung, Caglar Gulcehre, KyungHyun Cho, and Yoshua Bengio. Empirical evaluation of gated recurrent neural networks on sequence modeling. arXiv preprint arXiv:1412.3555 2014.
Michaël Defferrard, Xavier Bresson, and Pierre Vandergheynst. Convolutional neural networks on graphs with fast localized spectral filtering. In Advances in Neural Information Processing Systems, pp. 3844-3852, 2016.
Alex Flint and Matthew Blaschko. Perceptron learning of sat. In Advances in Neural Information Processing Systems, pp. 2771-2779, 2012.
Oliver Gableske, Sven Müelich, and Daniel Diepold. On the performance of edcl-based message passing inspired decimation using popmpi. In Pragmatics of SAT' Workshop, 2013.
Jesús Giráldez- Cru and Jordi Levy. Generating sat instances with community structure. Artificial Intelligence, 238: 119-134, 2016.
Aditya Grover, Tudor Achim, and Stefano Ermon. Streamlining variational inference for constraint satisfaction problems. In Advances in Neural Information Processing Systems, pp. 10579-10589, 2018.
Cristian Grozea and Marius Popescu. Can machine learning learn decision oracle for np problems? a test on sat. Fundamenta Informaticae, 131(3-4):441-55,, 2014.
Shai Haim and Toby Walsh. Restart strategy selection using machine learning techniques. In Inter- national Conference on Theory and Applications of Satisfibiliity Testing, pp- 312-325. Springer, 2009.
He He, Hal Daume III, and Jason M Eisner. Learning search in branch and bound algorithms. In Advances in neural information processing systems, pp. 3293-3301, 2014.
Nicolas Heess, Daniel Tarlow, and John Winn. Learning pass expectation propagation messages. In Advances in Neural Information Processing Systems, pp. 3219-3227, 2013.
Frank Hutter, Holger H Hoos, and Kevin Leyton-Brownn Sequential model-based optimization for general algorithm configuration. In International Conference on Learning and Intelligent Optimization, pp. 507-523. Springer, 2011.
10

---

Under review as a conference paper at ICLR 2020
Matthew Johnson, David K. Duvenaud, Alex Wiltschko, Ryan P Adams, and Sandeep R Datta. Composing graphical models with neural networks for structured representations and fast inference. In Advances in neural information processing systems, pp.
2016.
Elias Khalil, Hanjun Dai, Yuyu Zhang, Bistra Dilkina, and Le Song. Learning combinatorial optimization algorithms over graphs. In Advances in Neural Information Processing Systems, pp. 6348 6358, 2017.
Donald Ervin Knuth. The art of computer programming, Volume Fascicle 6: Satisfiability, volume Addison- Addison-Wesley Professional, 2015.
Daphne Koller, Nir Friedman, and Francis Bach. Probabilistic graphical models: principles and techniques. MIT press, 2009.
Florent Krzakala, Andrea Montanari, Federico Ricci- Tersenggs,,,, Guilhem Semerjian, and Lenka Zdeborová. Gibbs states and the set of solutions of random constraint satisfaction problems. Proceedings of the National Academy Sciences, 104(25):03318-0033) 2007.
Vipin Kumar. Algorithms for constraint-saatisactiin problems: A survey, Al magazine, 13(1):32, 1992.
Yujia Li, Daniel Tarlow, Mare Brockschmidt, and Richard Zemel. Gated graph sequence neural networks. arXiv preprini urXiv:/511.0544
Zhuwen Li, Qifeng Chen, and Vladlen Koltun. Combinatorial optimization with graph convolutional networks and guided tree search. In Advances in Neural Information Processing Systems, pp- 537-546, 2018.
Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for sat solvers. In International Conference on Theory and Applications of Satisfiability Testing, pp. 123-140. Springer, 2016.
Guosheng Lin, Chunhua Shen, Ian Reid, and Anton van den Hengel. Deeply learning the messages in message passing inference. In Advances in Neural Information Processing Systems, pp. 361-369, 2015.
Mare Mezard and Andrea Montanari. Information, physics, and computation. Oxford University Press, 2009.
Andrea Montanari, Federico Ricci-Ter,,nghi, and Guilhem Semerjian. Solving constraint satisfaction problems through belief propagation-guica guidedd decimation. arXiv preprint arXiv:0709. (ile:0009..67,, 2007.
Mark EJ Newman. Modularity and community structure in networks. Proceedings of the national academy of sciences, 103(23):5577-852, 2006.
Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. Impact of community structure on sat solver performance. In International Conference Theory and Applications of Satisfiaility Testing, pp. 252-268. Springer, 2014.
Eugene Nudelman, Kevin Leyton-Browd Brown, Holger H Hoos, Alex Devkar, and Yoav Shoham. Un- derstanding random sat: Beyond the -aarial-o ratio. In International Conference Principles and Practice of Constraint Programming, pp. 438-452. Springer, 2004.
Rasmus Palm, Ulrich Paquet, and Ole Winther. Recurrent relational networks. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. BesacBiianch,, and R. Garnett (eds.), Advances in Neural Information Processing Systems 31, pp. 3372-3382. Curran Associates, Inc., 2018.
Marcelo OR Prates, Pedro HC Avelar, Henrique Lemos, Luis Lamb, and Moshe Vardi. Learning to solve up-complete problems-a graph neural network for the decision tsp. arXiv preprint 022.021.09...21 2018
Stephane Ross, Daniel Munoz, Martial Hebert, and J Andrew Bagnell. Learning message-passing inference machines for structured prediction. In Computer Vision and Pattern Recognition (CVPR), 2011 IEEE Conference on, pp. 2737-2744. IEEE, 2011.

---

Under review as a conference paper at ICLR 2020
Daniel Selsam, Matthew Lamm, Benedikt Bunz, Percy Liang, Leonardo de Moura, and David L Dill. Learning a sat solver from single-bit supervision. In International Conference on Learning Representations, 2019.
Rishabh Singh. Joseph P Near, Vijay Ganesh, and Martin Rinard. Avatarsat: An auto-tuning boolean sat solver. 2009.
Oriol Vinyals. Meire Fortunato, and Navdeep Jaitly. Pointer networks. In Advances in Neural Information Processing Systems, pp. (692-2700, 2015.
Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S Yu. A comprehensive survey graph neural networks. arXiv preprint arXiv:/901.00556, 2019.
Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Satzilla: portfolio-based algorithm selection for sat. Journal of artificial intelligence research, 32:565-606, 2008.
Lin Xu, Holger H Hoos, and Kevin Leyton-Brown. Brown. Predicting satisfiability at the phase transition. In AAAI, 2012.
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.
Manzil Zaheer, Satwik Kottur, Siamak Ravanbakhsh, Barnabas Poczos, Ruslan R Salakhutdinov, and Alexander Smola. Deep sets, In Advances in Neural Information Processing Systems, pp. 3391-3401, 2017.
12


Reviews:
[{"review_id": "SylPx5jiYS", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 1, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper 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.  \n\nOverall, 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. \n\nAlthough 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: \n* 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.\n* 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? \n\nThe 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. ", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper."}, "extra_text": {}}, {"review_id": "HJej_nE-9S", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "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.  \n\nStrength:\n-\tThe proposed approach makes sense to me and allows modularity.\n-\tThe 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.\n-\tThe paper is clearly written and seem over all solid.\n\nWeaknesses:\n1.\tComparison to prior work\n1.1.\tTo 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.\n1.2.\tIt would be interest to know if and how the proposed model performs on the problems evaluated in Selsam 2019.\n2.\tThe 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.\n\nAn 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.\nI am borderline on this paper, also given my limited knowledge of the field.\n\n", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory."}, "extra_text": {}}, {"review_id": "Bke5fKG0tr", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "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.\n\nThis 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.\n\nOverall, 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.\n\nComments\nThe 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.\n\nI don't often see field names such as \"Machine Learning\" and \"Deep Learning\" capitalized as they are in this paper.\n\nTypos\nIn contract -> In contrast\nN discrete variable X -> N discrete variables X?", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I made a quick assessment of this paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "N/A"}, "extra_text": {}}]

Author rebuttal:

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