Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 3: Weak Reject
review_content: The paper proposes learning a branching heuristic to be used inside the SAT solver MiniSat using reinforcement learning. The state is represented as a graph representation of the Boolean formula as in previous works, and the policy is parameterized as a graph neural network. At each step of an episode the policy selects a variable to branch on and assigns a value to it. The episode terminates once the solver finds a satisfying assignment or proves unsatisfiability. The reward function encourages the policy to reach terminal state in as few steps as possible. The policy is trained using DQN. Results on randomly generated SAT instances show that the learned policy is able to solve problems with fewer steps than VSIDS, the branching heuristic commonly used by state-of-the-art solvers.

Pros:
- The paper is nicely written and easy to read.
- The general idea of using RL to learn distribution-specific branching heuristics is a very interesting research problem, and SAT is a difficult test case for it.
- The experiments provide interesting insights, especially Figure 2 and the graph coloring results in Table 3.

Cons:
- Showing improvements in the number of steps compared to VSIDS is not interesting because VSIDS as implemented in MiniSat and state-of-the-art solvers like Glucose has been tuned to minimize running time rather than number of steps.  A better comparison would be to compare against a branching heuristic that is designed to be step-efficient -- e.g., the branching heuristic GGB proposed in Chapter 3 of Liang’s PhD thesis (available here: https://drive.google.com/file/d/1RzJtmdbjFeT2N84WDWQkBfQoGPF-qRoT/view?usp=sharing). GGB is more expensive than VSIDS, but if the time needed for branching is removed, a solver using GGB is faster than one using VSIDS (see figure 3.1 in the thesis).

- A better discussion of how to scale up the proposed approach to instances with millions of variables is needed. Although most ML papers on SAT deal with at most hundreds of variables, such small instances are trivial for the state-of-the-art solvers. The real challenge is to scale up to the instance sizes that are considered in SAT competitions. For example, Selsam and Bjorner 2019 https://arxiv.org/pdf/1903.04671.pdf tackle such instances in their NeuroCore work. (While the paper references that work, it doesn’t compare to it.) There is no attempt to address the scalability issue in this work. Apart from considering the challenges of successfully learning on large instances (briefly discussed in the conclusion), there should be an analysis on the inference cost of the graph neural network (which scales linearly with the number of variables and clauses) to make a single branching decision vs. that of VSIDS, and what that implies on how much reduction in the number of steps a learned branching policy would need to achieve before it can provide time savings over VSIDS. It may turn out that the reductions required of a learned branching policy are implausibly large. Without a better understanding of these challenges, it is not clear that learning can help much to improve the state-of-the-art SAT solvers.
review_title: Official Blind Review #2

final_score: rating: 3: Weak Reject
review_content: === Summary ===
The authors apply Q-learning with GNN function approximation as a branching heuristic in Conflict Driven Clause Learning (CDCL) SAT solvers. The GQSAT agent assigns unassigned variables to True or False in a CDCL SAT environment and receives a negative reward for each non-terminal state, thus encouraging the agent to finish an episode as quickly as possible.
The agent is trained with Q-learning and GNN as the function approximator: the input is presented as a bipartite graph with variables and clauses corresponding to a SAT instance in CNF form and the GNN predicts Q-values for assigning each unassigned variable to True or False.
Then authors compare their method to the popular VSIDS branching heuristic (which counts the number of conflicts a literal or variable has been involved in) and report the median relative iteration reduction over all problems (~2-3x for satisfiable instances, a bit less for unsatisfiable instances).
GQSAT generalizes well to larger satisfiable instances than those seen during training and somewhat to unsatisfiable instances (unSAT). It doesn't seem to provide improvements compared to VSIDS when when generalizing to different problem structures (as shown by the graph coloring generalization experiments).

=== Recommendation ===

This paper is well-motivated (improving speed of complete SAT solvers) and presents a good overview of related work.
The paper is well written overall, although I found section 3 hard to read and I think the writing can be a bit improved by writing explicitly the algorithm or at least the MDP (see misc comments)
While the reduction in number of branching decisions is satisfactory, this does not necessarily translates to actual speed-ups (since the VSIDS branching heuristic is faster in practice) and there are some concerns about applying GQSAT to larger instances.

I slightly lean for rejecting this paper.

=== Misc ===
- Can the authors hypothesize on why GQSAT does not benefit from seeing more instances of SAT during training?
- What is the motivation for using Median Relative Iteration Reduction as a metric? How about using the ratio of the means over all problems instead?
- Beginning of section 3 is quite confusing: "We represent the set of all possible SAT problems as an MDP. The state of such an MDP consists of unassigned variables and unsatisfied clauses.". It would help to write properly the MDP corresponding to the CDCL SAT solver.
- 'NeuroSAT cannot generalize from SAT to unSAT': the NeuroSAT paper showed that they could learn to predict satisfiability as well.
review_title: Official Blind Review #1

final_score: rating: 8: Accept
review_content: This paper investigates the problem of learning new branching heuristics in SAT solvers. The idea is very simple: take MiniSat, remove the usual VSIDS heuristic, and replace it with a variable selection policy that has been trained from a deep reinforcement learning algorithm. The architecture advocated in the present study is based on GNNs coupled with usual DQN techniques. The resulting GQSAT heuristic is endowed with attractive properties: on random SAT instances, it outperforms VSIDS and generalizes relatively well to other SAT distributions. 

Overall, this is a very interesting paper. It is well-written, well-motivated, and well-positioned with respect to related work. The conceptual idea is simple and elegant, the choice of the graph-based DQN architecture is relevant, the experimental protocol is well-detailed, and the experimental results look promising. To sum up, I have no major reasons for not accepting this paper. 

Some potential improvements:

(a) Obviously, the decision model for GQSAT is an “episodic” MDP. It would be relevant to emphasize this aspect by presenting episodic MDPs (instead of standard ones) in Sec 2.2. 
(b) States representations only encode SAT formulae (using Q-labeled incidence graphs). Although this is a conceptually simple idea, GQSAT could exploit additional information provided by MiniSAT (e.g. number of propagations, number of clauses which have been learned, etc.). I am wondering whether such “solver features” in state representations could improve the GQSAT heuristic, and could help in generalizing from a class of SAT problems to another one. 
(c) The notion of "terminal state" is a bit ambiguous. Since the number of actions per episode is capped, a terminal state can be a leaf of the MiniSat search tree (where a satisfying assignment was found, or a dead-end was reached), or an internal node of the tree (when the maximum number of actions per episode was reached). 

review_title: Official Blind Review #3

Meta-review: SAT is NP-complete (Karp, 1972) due its intractable exhaustive search. As such, heuristics are commonly used to reduce the search space. While usually these heuristics rely on some in-domain expert knowledge, the authors propose a generic method that uses RL to learn a branching heuristic. The policy is parametrized by a GNN, and at each step selects a variable to expand and the process repeats until either a satisfying assignment has been found or the problem has been proved unsatisfiable. The main result of this is that the proposed heuristic results in fewer steps than VSIDS,  a commonly used heuristic. 

All reviewers agreed that this is an interesting and well-presented submission. However, both R1 and R2 (rightly according to my judgment) point that at the moment the paper seems to be conducting an evaluation that is not entirely fair. Specifically, VSIDS has been implemented within a framework optimized for running time rather than number of iterations, whereas the proposed heuristic is doing the opposite. Moreover, the proposed heuristic is not stressed-test against larger datasets. So, the authors take a heuristic/framework that has been optimized to operate specifically well on large datasets (where running time is what ultimately makes the difference) scale it down to a smaller dataset and evaluate it on a metric that the proposed algorithm is optimized for. At the same time, they do not consider evaluation in larger datasets and defer all concerns about scalability to the one of industrial use vs answering ML questions related to whether or not it is possible to  “stretch existing RL techniques to learn a branching heuristic”. This is a valid point and not all techniques need to be super scalable from iteration day 0, but this being ML, we need to make sure that our evaluation criteria are fair and that we are comparing apples to apples in testing hypotheses. As such, I do not feel comfortable suggesting acceptance of this submission, but I do sincerely hope the authors will take the reviewers' feedback and improve the evaluation protocols of their manuscript, resulting in a stronger future submission.
Decision: Reject