Improving SAT Solver Heuristics with Graph Networks and Reinforcement Learning
Authors: Vitaly Kurin
Saad Godil
Shimon Whiteson
Bryan Catanzaro
Venue:  (2020)
Keywords: SAT
reinforcement learning
graph neural networks
heuristics
DQN
boolean satisfiability

Abstract: We present GQSAT, a branching heuristic in a Boolean SAT solver trained with value-based reinforcement learning (RL) using Graph Neural Networks for function approximation. Solvers using GQSAT are complete SAT solvers that either provide a satisfying assignment or a proof of unsatisfiability, which is required for many SAT applications. The branching heuristic commonly used in SAT solvers today suffers from bad decisions during their warm-up period, whereas GQSAT has been trained to examine the structure of the particular problem instance to make better decisions at the beginning of the search. Training GQSAT is data efficient and does not require elaborate dataset preparation or feature engineering to train. We train GQSAT on small SAT problems using RL interfacing with an existing SAT solver. We show that GQSAT is able to reduce the number of iterations required to solve SAT problems by 2-3X, and it generalizes to unsatisfiable SAT instances, as well as to problems with 5X more variables than it was trained on. We also show that, to a lesser extent, it generalizes to SAT problems from different domains by evaluating it on graph coloring. Our experiments show that augmenting SAT solvers with agents trained with RL and graph neural networks can improve performance on the SAT search problem.

Under review as a conference paper at ICLR 2020
IMPROVING SAT SOLVER HEURISTICS WITH GRAPH NETWORKS AND REINFORCEMENT LEARNING
Anonymous authors Paper under double-blind review
ABSTRACT
We present GQSAT, branching heuristic in Boolean SAT solver trained with value-based reinforcement learning (RL) using Graph Neural Networks for func- tion approximation. Solvers using GQSAT are complete SAT solvers that either provide satisfying assignment proof of unsatisfiability, which is required for many SAT applications. The branching heuristic commonly used in SAT solvers today suffers from bad decisions during their warm-up period, whereas GQSAT has been trained to examine the structure of the particular problem instance to make better decisions at the beginning of the search. Training GQSAT is data efficient and does not require elaborate dataset preparation or feature engineering to train. We train GQSAT on small SAT problems using RL interfacing with existing SAT solver. We show that GQSAT is able to reduce the number of itera- tions required to solve SAT problems by 2-3X, and it generalizes SAT instances, as well as to problems with 5X more variables than it was trained on. We also show that, different domains by evaluating it on graph coloring. Our experiments show that augmenting SAT solvers with agents trained with RL and graph neural networks can improve performance on the SAT search problem.
unsatisfiable
lesser extent, generalizes
SAT problems from
INTRODUCTION
Boolean satisfiability (SAT) is an important problem for both industry and academia impacting var- ious fields, including circuit design, computer security, artificial intelligence, automatic theorem proving, and combinatorial optimization. phisticated, reliable pieces of software that scale to problems with hundreds of thousands of variables (Ohrimenko et al. 2009).
a result, modern SAT solvers are well-crafted, so-
SAT is known to be NP-complete (Karp) 1972), and most state-of-the-art open-source and com- mercial solvers rely on multiple heuristics to speed up the exhaustive search, which is otherwise intractable. These heuristics are often iterated on using trial and error. In this paper, we investigate how we can use machine learning to improve upon existing branching heuristic without leveraging domain expertise.
usually meticulously crafted using expert domain knowledge and
We present Graph- Q-SAT (GQSAT), a branching heuristic in Conflict Driven Clause Learn- Schrag 1997, CDCL) SAT solver trained with
ing (Marques-Silva Sakallah 1999 Bayardo value-based reinforcement learning (RL), based on DQN (Mnih et al. 2015). GQSAT uses graph representation of SAT problems similar to Selsam et al. (2018) which provides permutation and variable relabeling invariance. It uses Graph Neural Network (Gori et al. 2005 Battaglia et al., 2018 GNN) as a function approximator provide generalization state-action space. GQSAT uses a simple state representation and binary reward that requires no feature engineering or problem domain knowledge. GQSAT modifies only part of the CDCL. based solver, keeping it complete, i.c. always leading to correct solution.
well support for dynamic
We demonstrate that GQSAT outperforms Variable State Independent Decaying Sum MMokkewicz et al. 2001 VSIDS), most frequently used CDCL branching heuristic, reducing the number of iterations required to solve SAT problems by 2-3X. GQSAT is trained to examine the structure of the particular problem instance to make better decisions at the beginning of the search whereas the VSIDS heuristic suffers from bad decision during the warm-up period. We show that our method generalizes to problems five times larger than those it was trained on. We also show that our method

---

Under review as a conference paper at ICLR 2020
generalizes across problem types from SAT to unSAT. We also show, to lesser extent, it generalizes to SAT problems from different domains, such as graph colouring. Finally, we show that some of achieved even when training is limited to single SAT problem demonstrating
these improvements data efficiency of our method. We believe GQSAT a stepping stone to a new generation of SAT solvers leveraging data to build better heuristics learned from past experience.
2 BACKGROUND
2.1 SAT PROBLEM
SAT problem involves finding variable assignments such that a propositional logic formula is satisfied or showing that such assignment does not exist. A propositional formula is a Boolean expression, including Boolen variables, ANDs, ORs and negations. 'x' or 'NOT make up a literal. It is convenient to represent Boolean formulas in conjunctive normal form (CNF), i.e., con- junctions (AND) of clauses, where a clause a disjunction (OR) of literals. An example of CNF is (2) V -22) A (I2 V -xz). where A, V, are AND, OR, and negation respectively. This CNF has two clauses: (x) V mx2) and (I2 V - In this work, we use SAT to both denote the Boolean Satisfiability problem and a satisfiable instance, which should be clear from the context. We use unSAT to denote unsatisfiable instances.
There are many types of SAT solvers. In this work, focus CDCL solvers, MiniSat (Sorensson & Een 2005) in particular, because it is an open source, minimal, but powerful implementation. A CDCL solver repeats the following steps: every iteration it picks literal, assigns a variable binary value. This is called decision. After deciding, the solver simplifies the formula building an implication graph, and checks whether conflict emerged. Given conflict, can infer (learn) new clauses and backtrack to the variable assignments where the newly learned clause becomes unit (consisting of single literal) forcing a variable assignment which avoids the previous conflict. Sometimes, CDCL solver undoes all the variable assignments keeping the learned clauses to escape futile regions of the search space. This is called a restart.
We focus on the branching heuristic because it is one of the most heavily used during the solution procedure. The branching heuristic is responsible for picking the variable and assigning some value to it. VSIDS (Moskewicz et al. 2001) is one of the most used CDCL branching heuristics. It is a counter-based heuristic which keeps a scalar value for each literal or variable (MiniSat uses the latter). These values are increased every time variable gets involved in conflict. The algorithm behaves greedily with respect to these values called activities. Activities are usually initialized with zeroes (Liang et al. 2015).
2.2 REINFORCEMENT LEARNING
We formulate the RL problem as a Markov decision process (MDP). An MDP is tuple (S, A. R, T, p. with of states S, set of actions A, a reward function R(s, a, s') and the transition function T= p(s, a, 8'), where p(s, a, 8') is probability distribution, 8, s' E S, a E A. p is the probability distribution over initial states. ? E (0,1) is the discount factor responsible for trading off the preferences between the current immediate reward and the future reward. In the case of episodic tasks, the state space is split into the set of non-terminal states and the terminal state S+. To solve an MDP means to find optimal policy. a mapping which outputs action distribu- tion over actions given the state, such that we maximize the expected discounted cumulative return R = E /re,), where = R(s,, aq 8t+1) is the reward for the transition from s, $
In Section 3 we apply deep Q-networks (Mnih et al. 2015 DQN), a value-based RL algorithm that approximates optimal Q-function, an action-value function that estimates the sum of fu- ture rewards after taking an action a in state 8 and following the optimal policy æ thereafter: (s) E., [[[(s (, a, s') 7 max, (s), A mean squared temporal difference (TD) error is used make an update step: L(0) (Qo(s. r y max,' Qá(s', a²))². Qa is called target network (Mnih et al. 2013). It is used to stabilise DQN by splitting the decision and evaluation operations. Its weights copied from the main network Qo after each k minibatch updates.
2

---

Under review as a conference paper at ICLR 2020
[1,0]
(42.0,3.14)
[0.1]
[1,0]
[1.62, 2.70]
1,0
[0.1]
[1,0]
[6.02. 1.67]
JP3
(a) Bipartite graph representation of the Boolcan for- mula (I1 V x2) (-xz xa). The numbers next to the vertices distinguish variables and clauses. Edge labels encode literal polarities. The global component does
(b) Graph Q-function values for setting variables to true and false respectively. The action chosen using arg max across all Q values of variable nodes. Since
GNN work on directed graphs, we add two directional edges to connect two nodes.
not contain any information about the state.
Figure I: State-action space representation of GQSAT
2.3 GRAPH NEURAL NETWORKS
We use Graph Neural Networks (Gori et al. 2005 GNN) to approximate our Q-function due their input size, structure, and permutation invariance. We use the formalism of Battaglia et al. (2018) which unifies most existing GNN approaches. Under this formalism, GNN is a set functions that take labeled graph input and output graph with modified labels but the same topology.
Here, a graph a directed graph (V, F., U), where V is the set of vertices, (s, r) E E, s, V. and U is global attribute. The global attribute contains information, relevant to the whole graph. We call vertices, edges and the global attribute entities. Each entity has its features vectors. GNN changes this features result of its operations.
the set edges with
A graph network can be seen as a set of six functions: three update functions and three aggregation functions. The information propagates between vertices along graph edges. Update functions com- pute new entity labels. Aggregation functions exist to ensure the GNN's ability to process graphs of arbitrary topologies, compressing multiple entities features into vectors of fixed size. GNN blocks can be combined such that the output of one becomes input of the other. For example, the Encode- Process- -eccode architecture (Battaglia al. (018)) processes the graph in a recurrent way, enabling information propagation between remote vertices.
3 GQSAT
the MDP formalism for purposes. Each state of our MDP consists of unassigned variables and unsatisfied clauses containing these variables. The initial state distribution is distribution over all possible SAT problems. Our problem has an episodic nature with a clear terminal state: when satisfying assignment is found or the algorithm has exhausted all the possible options proving AASAT. The action set includes two actions for each unassigned variable: assigning it to true or false. We modify the MiniSat-bar based environment of Wang & Rompf (2018) which responsible for the transition function. It takes the actions, modifies its implication graph internally and returns new state, containing newly learned clauses and without the variables removed after the propagation. Strietly speaking, this state is not fully observable. In the case of conflict, the solver undoes the assignments for variables that are not in the agent's 's observation. However, in practice, this should not inhibit the goal of quickly pruning the search tree: the infor- mation in the state is enough to pick variable that leads to propagations in the remaining formula.
As noted in Section 2.2
We use simple reward function: the agent gets negative reinforcement for each non-terminal transition and for reaching the terminal state. This reward encourages an agent to finish an episode quickly possible and does require elaborate reward shaping start using GQSAT.
3

---

Under review as a conference paper at ICLR 2020
3.1 STATE REPRESENTATION
We represent a SAT problem as a graph similar to Selsam et al. (2018). We make it more compact, using vertices to denote variables instead of literals. We use nodes to encode clauses as well.
Our state representation is simple and does not require scrupulous feature engineering. An edge (1a,ca Gi) means that clause e contains literal zi. If literal contains a negation, a corresponding edge has a [1.0] label and [0, 1] otherwise. GNN process directed graphs so we create two directed edges with the same labels: from a variable to a clause and vice-versa. Vertex features are two dimensional one-hot vectors, denoting either variable or clause. We do not provide any other information to the model. The global attribute input is empty and is only used for message passing. Figure la gives example of the state for (I1 V 2:2) A (-a22 V xz).
3.2 Q-FUNCTION REPRESENTATION
We use the encode proeodderroces-deecod architecture (Battaglia et al. 2018), which we discuss in more detail in Appendix B. Similarly to [Bapst et al. (2019), our GNN labels variable vertices with Q- values. Each variable vertex has two actions: pick the variable and set it true or false as shown on Figure lb We choose the action which gives the maximum Q-value across all variable vertices. The graph contains only unassigned variables all actions are valid. We use common DQN techniques such as memory replay, target network and e-greedy exploration. To expose the agent to more episodes and prevent it from getting stuck, we cap the maximum number of actions per episode. This is similar to the episode length parameter in gym (Brockman et al. (016)).
3.3 TRAINING AND EVALUATION PROTOCOL
We train our agent using Random 3-SAT instances from the SATLIB benchmark (Hoos & Stützle, 2000). To measure generalization, we split these data into train, validation and test sets. The train set includes 800 problems, while the validation and test sets are 100 problems each. We provide more details about dataset in Appendinx B.2
To illustrate the problem complexities, Table 1 provides the number of steps it takes MiniSat to solve the problem. Each random 3-SAT problem is denoted as SAT-X-Y or unSAT-X-V where SAT means that all problems are satisfiable, unSAT stands for all problems stands for the number of variables and clauses in the initial formula.
unsatisfiable. X and Y
While random 3-SAT problems have relatively small number of variables/clauses, they have an interesting property which makes them more challenging for a solver. For this dataset, the ratio of clauses variables is close to 4.3:1 which is near the phase transition, when it is hard to say whether the problem is SAT or unS AT (Cheeseman et al.) 1991). In 3-SAT problems each clause has exactly 3 variables, however, learned clauses might be of arbitrary size and GQSAT is able to deal with it.
We use Median Relative Iteration Reduction (MRIR) w.r.t. MiniSat as our main performance metric which is a number of iterations it takes MiniSat to solve a problem divided by GQSAT's number of iterations. Similarly to the median human normalised score adopted in the Atari domain, we use the median instead of the mean to avoid the situation when the outliers skew the mean considerably. By one iteration we mean one decision, i.e. choosing a variable and setting it to value. MRIR is the median across all the problems in the dataset. We compare ourselves with the best MiniSat results having run MiniSat with and without restarts. We cap the number of decisions our method takes at the beginning of the solution procedure and then we give control to MiniSat.
When training, we evaluate the model every 1000 batch updates the validation subsets of the same distribution as the train dataset and pick the one with the best validation results. After that, we evaluate this model on the test dataset and report the results. For each of the model we do 5 training runs and report the average MRIR results, the maximum and the minimum.
We implement Lenssen 20019). We provide all the hyperparameters needed to reproduce our results in Appendix We will release our experimental code as well as the MiniSat gym environment.
models using Pytorch (Paszke et al. 2017) and Pytorch Geometric (Fey &
4

---

Under review as a conference paper at ICLR 2020
Table 1: Number of iterations (no restarts) it takes MiniSat to solve random 3-SAT in- stances.
Table 2: MRIR for GQSAT trained on SAT-
50-218. Evaluation for SAT-50-218 is on separate data not seen during training.
dataset
median
mean
dataset
mean
min
SAT 50-218
38
42
SAT 50-218
2.46
2.26
2.72
SAT 100-430
232
286
SAT 100-430
3.94
3.53
4.41
SAT 250-1065
62 192
76 120
SAT 250-1065
3.91
2.88
5.22
unSAT 50-128
68
68
unSAT 50-128
2.34
2.07
2.51
unSAT 100-430
587
596
unSAT 100-430
2.24
1.85
2.66
unSAT 250-1065
178 956
182 799
unSAT 250-1065
1.54
1.30
1.64
SAT 100-430
UnSAT 4.30
100-430 SAT 250 1065
USATT 300-436
SAT 250-1065
UISAT 250 1065
uSSTT 250- 1055
SAT 50-218
unSAT 90-218
SAT 50-218
unSAT 50-218
800
Figure GQSAT number maximum first decisions vs performance. GQSAT shows im- provement starting from 10 iterations confirm- ing our hypothesis of VSIDS initialization prob- lem. Best viewed in colour.
Figure 3: Dataset size effeet on generalization. While GQSAT profits from having data in most of the cases, it is able to generalize even from one data point. Model is trained SAT- 50-218 8. Best viewed in colour.
EXPERIMENTAL RESULTS
4.1 IMPROVING UPON VSIDS
In our first experiment, we consider whether possible improve upon VSIDS using no domain knowledge, simple state representation, and simple reward function. The first in Table gives us positive answer to that question. DQN equipped with GNN as a function approximation solves the problems in fewer than half the iterations of MiniSat.
GQSAT makes decisions resulting in more propagations, i.e., inferring variable values based on other variable assignments and clauses. This helps GQSAT prune the search tree faster. For SAT-
50-218, GQSAT does on average 2.44 more propagations than MiniSat (6.62 versus 48). We plot the average number of variable assignments for each problem individually in the Appendix A
These results raise the question: Why does GQSAT outperform VSIDS? VSIDS is a counter-based heuristic that takes time to warm up. Our model, the other hand, perceives the whole problem structure and can make more informed decisions from step one. To check this hypothesis, we vary the number of decisions our model makes the beginning of the solution procedure before hand the control back to VSIDS. The results of the experiment in [nguree]suppon this hypothesis. Even our model used for only the first ten iterations, still improves performance over VSIDS.
One strength of GQSAT is that VSIDS keeps being updated while the decisions are made with GQSAT. We believe that GQSAT complements VSIDS by providing better quality decisions in the initial phase while VSIDS is warming up. Capping the number of model calls can significantly reduce the main bottleneck of our approach - wall clock time spent on model evaluation. Optimizing for speed was not focus, however
with the current unoptimized implementation, if the model for the first 500 iterations and assuming this gives us 2x reduction in total iterations, our approach is competitive if takes more than 20 seconds for base solver solve the problem.
5

---

Under review as a conference paper at ICLR 2020
Table SAT-50 models performance on SATLIB flat graph coloring benchmark. Median Relative Iteration Reduction (MRIR) is w.r.t. MiniSat with restarts, since MiniSat performs better in this mode for this benchmark.
GQSAT MRIR
dataset
variables
clauses
MiniSat median iterations
average
min
max
flat-30-60
90
300
10
1.51
1.25
1.65
flat-50-115
150
545
15
1.36
0.47
1.80
flat-75-80
225
840
29
1.40
0.31
2.06
flat-100-2399
300
1117
55
1.44
0.31
2.38
flat-125-301
375
1403
106
1.02
0.32
1.87
flat-150-360
450
1680
179
0.76
0.37
1.40
flat-175-417
525
1951
272
0.67
0.44
1.36
flat-200-479
600
2237
501
0.67
0.54
0.87
4.2
GENERALIZATION PROPERTIES OF GQSAT
4.2.1
GENERALIZATION ACROSS PROBLEM SIZES
Table [ shows that GQSAT has no difficulties generalizing to bigger problems, showing almost 4x improvement in iterations for the dataset times bigger than the training set. GQSAT average leads to more variable assignments changes per step, e.g., 7.58 vs 5.89 on SAT-100-430. It might seem surprising that the model performs better for larger problems. However, performance metric is relative. An increase in score for different problem sizes might also mean that the base solver scales worse than our method does for this benchmark.
4.2.2 GENERALIZATION FROM SAT TO UNSAT
An important characteristic of GQSAT is that the problem formulation and representation makes it possible to solve unSAT problems when training only on SAT, which was problematic for some of the existing approaches (Selsam al. 2018).
The performance is, however, worse than the performance on satisfiable problems. On the one hand, SAT and unSAT problems different. When the solver finds one satisfying assignment, the problem is solved. For unSAT, the algorithm needs to exhaust all possible options to prove that there no such assignment. On the other hand, there is one important similarity between these two types of problems an algorithm has to prune the search tree as fast as possible. Our measurements of average propagations per step demonstrate that GQSAT learns how to prune the tree more efficiently than VSIDS (6.36 vs 4.17 for unSAT-50-218),
4.2.3 GENERALIZATION ACROSS PROBLEM STRUCTURES
SAT problems have distinct structures. The graph representation of random 3-SAT problem looks much different than that of graph coloring problem. To investigate how much our model, trained on SAT-50, can generalize to problems of different structures, we evaluate it on the flat graph coloring benchmark from SATLIB Hoos & Stützle 2000). All the problems the benchmark are satisfiable.
decrease in GQSAT performance when generalizing to another problem distribution. We believe there are two potential reasons. First, different SAT problem distributions have different graph properties that are not captured during training on another distribution. Second, this might be related to our model selection process which does not favor generalization across problem structures.
Table shows that graph coloring problems have more variables. We conducted an experiment investigating GQSAT's ability to scale to larger problems (more variables, more clauses). We trained GQSAT on flat75-180 with problems of 225 variables and 840 clauses. Graph Coloring benchmarks have only 100 problems each, so we do not split them into train/validation/tes dataset using using.flat-2 flat-75- in all
80 for training and flat- 100-239 to do model selection. We the same hyperparameters previous experiments changing only the gradient clipping parameter to 0.1. The results on Table show that GQSAT can scale bigger problems on the flat graph coloring benchmark.

---

Under review as a conference paper at ICLR 2020
Table GQSAT Median Relative Iteration Reduction (MRIR) for the model trained on flat-75-80, evaluated on flat-100- 100-239. flat-75-80 and 100-100-239 are separated, because the model was trained using the former and validated on the second. The results are for five training runs.
GQSAT MRIR
dataset
average
min
max
flat75-180
2.44
2.25
2.70
flat 100-290
2.89
2.77
2.98
flat-30-60
1.74
1.33
2.00
flat-50-115
2.08
2.00
2.13
flat-125-301
2.43
2.20
2.66
flat-150-360
2.07
2.00
2.11
Ila--175-417
1.98
1.69
2.21
flat-200-479
1.70
1.38
1.98
Apart from scaling to bigger graphs, we could test scaling for longer episodes. Table shows expo- nential growth in the number of iterations it takes MiniSat to solve larger problems. Our preliminary experiments show that generalizing easier than learning. Learning on AAT-100-430 requires more resources, does not generalize as well, and is generally less stable than training on SAT-50-218 This is most likely related to higher variance the returns caused by longer episodes, challenges for temporal credit assignment, and difficulties with exploration, motivating further research. It also motivates curriculum learning as the next step of GQSAT development, [Bapst et al. (2019) shows a positive effect of curriculum learning RL with GNN.
4.3 DATA EFFICIENCY
We design our next experiment to understand how many different SAT problems GQSAT needs to leam from. We varied the SAT-50-218 train set from single problem to 800 problems. Figure demonstrates that GQSAT is extremely data efficient. Having more data helps in most cases but, even with single problem, GQSAT generalizes across problem sizes and unSAT instances. This should allow GQSAT to generalize to new benchmarks without access to many problems from it. We suppose that GQSAT's data efficiency is one of the benefits of using RL. The environment allows the agent to explore diverse state-action space regions making it possible to learn useful policies even from single instance. In supervised learning, the data diversity is addressed at the training data generation step.
RELATED WORK
Using machine learning for the SAT problem is not a new idea (Haim & Walsh 2009 Grozea & Popescu 2014 Flint & Blaschko, 2012 Singh al. 2009). Xu al. (2008) propose portfolio- based approach which yielded strong results in 2007 SAT competition. Liang et al. (2016) treat each SAT problem multi-armed bandit problem capturing variables' ability to generate learnt clauses.
Recently, SAT has attracted interest in the deep learning community. There are two main approaches: solving problem end-to-end or learning heuristics while keeping the algorithm backbone the same. Selsam et al. (2018) NeuroSAT) take end-to-end supervised learning approach demonstrating that GNN can generalize SAT problems bigger than those used for training. NeuroSAT finds satisfying assignments for the SAT formulae and thus cannot generalize from SAT to unSAT problems. More- over, the method incomplete and might generate incorrect results, which is extremely important especially for AT problems. [Selsam & Bjørner (2019) modify NeuroSAT and integrate it into popular SAT solvers to improve timing on SATCOMP 2018 benchmark. While the approach shows its potential to scale to large problems, it requires extensive training set including over 150,000 data points. Amiizddhh et al. (2018) propose an end-to-end GNN architecture to solve circuit-SAT problems. While their model never produces false positives, cannot solve unSAT problems.
The following methods take the second approach learning a branching heuristic instead of learning an algorithm end-to-end. Jaszezur et al. (2019) take the supervised-learmt approach using the same

---

Under review as a conference paper at ICLR 2020
graph representation in Selsam et al. (2018). The authors show positive effect of combining DPLL/CDCL solver with the learnt model. As in Selsam et al. (2018). their approach requires a diligent process of the test set crafting. Also, the authors do not compare their approach to the VSIDS heuristic, which is known to be crucial component of CDCL (Katebi et al. 2011).
Wang & Rompf (2018), whose environment we took as starting point, show that DQN does not generalize for 20-91 3-SAT problems, whereas Alpha(GO) Zero does. Our results show that the issue is related to the state representation. They use CNNs, which are not invariant variable renaming or permutations. Moreover, CNNs require a fixed input size which makes it infeasible when applying to problems with different number of variables or clauses.
The work of Lederman et al. (2018) is closest to ours. They train a REINFORCE (Williams) 1992) agent replace the branching heuristic for Quantified Boolean Formulas using GNNs for function approximation. They note positive generalization properties across the problem size for problems from similar distributions. Besides the base RL algorithm and some minor differences, our ap- proaches differ mainly in the state representation. They use 30 variables for the global state encod- ing and seven variables for vertex feature vectors. GQSAT does not require feature engineering to construct the state. We use only two bits to distinguish variables from clauses and encode literal po- larities. Also, Lederman et al. 2018) use separate vertices for x and z in the graph representation.
Vinyals et al. 2015) introduce recurrent architecture for approximately solving complex geometric problems, such as the Traveling Salesman Problem (TSP), approaching it in a supervised way. [ello et al. (2016) consider combinatorial optimization problems with RL, showing results TSP and the Knapsack Problem. Khalil et al. (2017) approach combinatorial optimization using GNNs and DQN, learning a heuristic that later used greedily. is slightly different from the approach we take since their heuristic is effectively the algorithm itself. We augment only a part of the algorithm the branching heuristic. Paliwal et al. (2019) use GNN with imitation learning for theorem proving.
Carbune et al. (2018) propose general framework of injecting an RL agent into existing algorithms.
Cai et al. (2019) use RL find a suboptimal solution that further refined by another optimization algorithm, simulated annealing (Kirkpatrick et al. 1983 SA) in their case. The method is not limited with SA, and this modularity is valuable. However, there one important drawback of the approach. The second optimization algorithm might benefit more from the first algorithm if they are interleaved. For instance, GQSAT can guide search before VSIDS overcomes its initialization bias.
Recently, GNN received lot of attention in the RL community, enabling the study of RL agents in state/action spaces of dynamic size, which crucial for generalization beyond the given task. |Wang] et al. (0118) and (Sanchez- (Sanchez-Gonzlezz Gonzalez et al. (2018) consider GNN for the generalization of the control problem. Bapst et al. (2019) investigate graph-based representation for the construction task and notice high generalization capabilities of their agents. Diang et al. (2018); Malysheva et al. (2018) [Agarwal et (2019) study generalization of the behaviour in multi-agent systems, noting the GNN benefits due to their invariance to the number of agents in the team other environmental entities.
6 CONCLUSION AND FUTURE WORK
In this paper, we introduced GQSAT, a branching heuristic of a SAT solver that causes more variable propagations per step solving the SAT problem in fewer iterations comparing VSIDS. GQSAT uses simple state representation and does not require elaborate reward shaping. We demonstrated its generalization abilities. showing more than 2-3X reduction in iterations for the problems up to 5X larger and 1 1.5-2X from SAT to unSAT. We showed how GQSAT improves VSIDS and showed that our method data efficient. While our method generalizes across problem structures to lesser extent, we showed that training data from other distributions might lead to further performance improvements. Our findings lay the groundwork for future research that we outline below.
Scaling GQSAT to larger problems. Industrial-sized benchmarks have millions of variables. Our ex- periments training on SAT- 100 and graph coloring show that increases in problem complexity makes our method less stable due to typical RL challenges: longer credit assignment spans, reward shap- ing, etc. Further research will focus on scaling GQSAT using latest stabilizing techniques (Hessel et al. 2018), more sophisticated exploration methods and curriculum learning.
8

---

Under review as a conference paper at ICLR 2020
From reducing iterations speeding up. SAT heuristics are good because they fast. It takes constant time to make decision with VSIDS. GNN inference takes much longer. However, our experiments show that GQSAT show improvement using only the first k steps. Reducing the network polling frequency and replacing the variable activities with GQSAT"s output similarly to [Selsam & Bjørner (2019) is another interesting avenue of the future research. An efficient C++ implementation of our method should also help.
Interpretation of the results. Newsham et al. 2014) show that the community structure of SAT prob- lems is related to the problem complexity. We are interested in understanding how graph structure influences the performance GQSAT and how we can exploit this knowledge improve GQSAT.
Although we showed the powerful generalization properties of graph-based RL, we believe the prob- lem still far from solved and our work is just one stepping stone towards new generation of solvers that can discover and exploit heuristics that are too diffccutt for human to design.
REFERENCES
Akshat Agarwal, Sumit Kumar, and Katia Sycara. Learning transferable cooperative behavior in multi-agent teams, 2019.
Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. Learning to solve circuit-sat: An unsu- pervised differentiable approach. 2018.
Victor Bapst, Alvaro Manchez-Gonzaler Carl Doersch, Kimberly Stachenfeld, Pushmeet Kohli, Peter W. Battaglia, and Jessica B. Hamrick. Structured agents for physical construction, 2019.
Peter W Battaglia, Jessica B Hamrick, Victor Bapst, Alvaro Sonzaez-Gonzalez, Vinicius Zambaldi, Mateusz Malinowski, Andrea Tacchetti, David Raposo, Adam Santoro, Ryan Faulkner, et al. Relational inductive biases, deep learning, and graph networks. arXiv preprint arXiv: 1806.0126, 2018.
Roberto Bayardo Jr and Robert Schrag. Using csp look-back techniques to solve real-world sat instances. In Aaai/iaii, pp. 203-208. Providence, RI, 1997.
Irwan Bello, Hieu Pham, Quoc Le, Mohammad Norouzi, and Samy Bengio. Neural combinatorial optimization with reinforcement learning, arXiv preprint 16Xiv:1611.09941 2016.
Greg Brockman, Vicki Cheung, Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojeiech Zaremba. Openai gym, 2016.
Qingpeng Cai, Will Hang, Azalia Mirhoseini, George Tucker, Jingtao Wang, and Wei Wei. Rein- forcement learning driven heuristic optimization, 2019.
Victor Carbune, Thierry Coppey, Alexander Daryin, Thomas Deselaers, Nikhil Sarda, and Jay Yag- nik. Smartchoices: Hybridizing programming and machine learning, 2018.
Peter C Cheeseman, Bob Kanefsky, and William M Taylor. Where the really hard problems are. In IJCAL, volume 91, pp. 331-337, 1991.
Matthias Fey and Jan E. Lenssen. Fast graph representation learning with PyTorch Geometric. In ICLR Workshop on Representation Learning on Graphs and Manifolds, 2019.
Alex Flint and Matthew Blaschko. Perceptron learning of sat. In Advances in Neural Information Processing Systems, pp. 177192779, 2012.
Marco Gori, Gabriele Monfardini, and Franco Scarselli. A new model for learning in graph domains. In Proceedings. 2005 IEEE International Joint Conference on Neural Networks, 2005., volume 2, pp. 729-734. IEEE, 2005.
Cristian Grozea and Marius Popescu. Can machine learning learn a decision oracle for np problems? test on sat. Fundamenta Informaticae, 131(3-4):441-550 2014.
Shai Haim and Toby Walsh. Restart strategy selection using machine learning techniques. In Inter- national Conference on Theory and Applications of Satisfiability Testing, pp. 312-325. Springer, 2009.

---

Under review as a conference paper at ICLR 2020
Matteo Hessel, Joseph Modayil, Hado Van Hasselt, Tom Schaul, Georg Ostrovski, Will Dabney, Dan Horgan, Bilal Piot, Mohammad Azar, and David Silver. Rainbow: Combining improvements in deep reinforcement learning. In Thirty-Second AAAI Conference Artificial Intelligence, 2018.
Holger Hoos and Thomas Stützle. Satlib: An online resource for research on sat. Sat, 2000:283- 292, 2000. URL httpp::/wwwt cs wbc www.aaaaaooosacaaeeoeeoo SAT.IIS//AATT//// www...t............tmmmmm html accessed September 18, 2019.
Sebastian Jaszezur, uszezyk Micha, and Henryk Michalewski. Neural heuristics for sat solving, 2019.
Jiechuan Jiang, Chen Dun, and Zongqing Lu. Graph convolutional reinforcement learning for multi- agent cooperation, 2018.
Richard M Karp. Reducibility among combinatorial problems. Complexity of computer compu- tations, pp. 85-103. Springer, 1972.
Hadi Katebi, Karem Sakallah, and João P Marques-Sine Silla. Empirical study of the anatomy of modern sat solvers. In International Conference on Theory and Applications of Satisfiability Testing, pp. 343-356. Springer, 2011.
Elias Khalil, Hanjun Dai, Yuyu Zhang, Bistra Dilkina, and Le Song. Learning combinatorial op- timization algorithms over graphs. Advances Neural Information Processing Systems, pp- 1348-6356 2017.
Scott Kirkpatrick, Daniel Gelatt, and Mario Vecchi. Optimization by simulated annealing. science, 220(4598);671-660, 1983.
Gil Lederman, Markus N. Rabe, Edward A. Lee, and Sanjit A. Seshia. Learning heuristics for automated reasoning through deep reinforcement learning, 2018.
Jia Hui Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, and Krzysztof Czarnecki. Understanding vsids branching heuristics in conflict-driven clause-learning sat solvers. In Haifa Verification Conference, pp. 225-241. Springer, 2015.
Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branch- ing heuristic for sat solvers. In International Conference on Theory and Applications of Satisfia- bility Testing, pp. 123-140. Springer, 2016.
Aleksandra Malysheva, Tegg Taekyong Sung, Chae-Bong Sohn, Daniel Kudenko, and Aleksei Sh- pilman. Deep multi-agent reinforcement learning with relevance graphs, 2018.
Joao P Marques-Silva and Karem A Sakallah. Grasp: A search algorithm for propositional satisfia- bility. IEEE Transactions on Computers, 48(5):506 521, 1999.
Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A Rusu, Joel Veness, Mare G Belle- mare, Alex Graves, Martin Riedmiller, Andreas Fidjeland, Georg Ostrovski, et al. Human-level control through deep reinforcement learning, Nature, 51 518(7540):529, 2015.
Matthew Moskewicz, Conor Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Con- ference, pp. 530-535. ACM, 2001.
Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. Im- pact of community structure on sat solver performance. In International Conference on Theory and Applications of Satisfiability Testing, pp. 252-268. Springer, 2014.
Olga Ohrimenko, Peter J Stuckey, and Michael Codish. Propagation via lazy clause generation. Constraints, 14(3):577339, 2009.
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy, Graph represen- tations for higher-order logic and theorem proving. arXiv preprint arXiv: 19.510055..000 2019.
10

---

Under review as a conference paper at ICLR 2020
Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary Vitioo, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in PyTorch. In NIPS Autodiff Workshop, 2017.
Alvaro Sanchez-Gonzalez, Nicolas Heess, Jost Tobias Springenberg, Josh Merel, Martin Riedmiller, Raia Hadsell, and Peter Battaglia. Graph networks as learnable physics engines for inference and control. arXiv preprint arXiv: 808.0126..22.. 2018.
Daniel Selsam and Nikolaj Bjømnr. Guiding high-performance sat solvers with unsat-core pre- dictions. In International Conference on Theory and Applications of Satisfiability Testing, pp- 336-353. Springer, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David Dill. Learning sat solver from single-bit supervision. arXiv preprint arXiv: 1802.0368, 2018.
Rishabh Singh, Joseph P Near, Vijay Ganesh, and Martin Rinard. Avatarsat: An auto-tuning boolean sat solver. 2009.
Niklas Sorensson and Niklas Een. Minisat vl. 13-a sat solver with conflict-clause minimization. SAT; 2005(53):1-2, 2005.
Oriol Vinyals, Meire Fortunato, and Navdeep Jaitly, Pointer networks. Advances in Neural Information Processing Systems, pp. 2692-2700, 2015.
Fei Wang and Tiark Rompf. From gameplay to symbolic reasoning. 2018.
Tingwu Wang, Renjie Liao, Jimmy Ba, and Sanja Fidler. Nervenet: Learning structured policy with graph neural networks. 2018.
Ronald J Williams. Simple statistical gradient- following algorithms for connectionist reinforcement learning. Machine learning, 8(3-4):229-25 1992.
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.
A PROPAGATIONS PER STEP
B REPRODUCIBILITY
B. MODEL ARCHITECTURE
We use Encoder-Proceet Process-Decode architecture from Battaglia al. (2018). Encoder and decoder are independent graph networks, i.c MLPs taking whole vertex or edge feature matrix as a batch without message passing. We call the middle part "the core'. The output of the core is concatenated with the output of the encoder and gets fed to the core again. We describe all hyperparameters in Appendix B.3 We also plan release the experimental code and the modified version of MiniSat to use as a gym environment.
B.2 DATASET
We split SAT-50-218 into three subsets: 800 training problems, 100 validation and 100 test problems. For generalization experiments, we use 100 problems from all the other benchmarks.
For graph colouring experiments, we train our models using all problems from flat-75-180 dataset. We select model, given performance this two datasets should not be used to judge the performance of the method and they are shown separately in Table 4 All the data from the second part of the table was not seen by the model during training (flat-30-60, flat-50-115 15, flat- 125-301, flat- nat-150 150-360, 1a5-175-417, flat-200-479).
all 100 problems from flat- f00--90--239. So, evaluation
B.3 HYPERPARAMETERS
11

---

Under review as a conference paper at ICLR 2020
Average assignments change per step, SAT 50-218
Average assignments change per step, unSAT 50-218
COSAT MinSat
GOGAT MisSat
mean wolprment
change step, UnSAT 100
Average assignments unSAT 430
COSAT MinSat
10
GOSAT
MinSat
wwloyreeee che pordze
60
80
1.00
20
40
100
probiom 1D
probiom ID
Figure 4: Average number of variable assignments change per step for (un)SAT-50-2218 and (un)SATT-00--400.
concat
Core
G
Encoder
Decoder
G
G'
Figure 5: Procode-Process--ee architecture. Encoder and Decoder are independent graph net-
works, i.e. MLPs taking whole vertex/edge data array batch. à is the index of message passing
iteration. When concatenating for the first time, encoder output is concatenated with zeros.
12

---

Under review as a conference paper at ICLR 2020
Hyperparameter
Value
Comment
DON
Batch updates
50 000
Learning rate
0,00002
Batch size
64
Memory replay size
20 000
Initial exploration
1.0
Final exploration
0.01
Exploration decay
30 000
Environment steps.
Enitial exploration steps
5000
Environment steps, filling the buffer, no training.
Discounting ?
0.99
Update frequency
4
Every 4th enviromment step.
Target update frequency
10
Max decisions allowed for training
500
Used safety against being stuck at the episode. Varied among [0, 10, 50, 100. 300, 500, 1000] for the experiment on Figure 2
Max decisions allowed for testing
500
Step penalty size p
-0.1
Optimization
Optimizer
Adam
Adam betas
0.9, 0.999
Pytorch default.
Adam
le-08
Pytorch default.
Gradient clipping
1.0
0.1 for training on the graph coloring dataset.
Gradient clipping norm
L2
Evaluation frequency
1000
Graph Network
Message passing iterations
4
Number of hidden layers for GN core
1
Number of units in GN core
64
Encoder output dimensions
For vertex, edge and global updater.
Core output dimensions
64,64,32
For vertex, edge and global respectively. For vertex updater, since only Q values are used, need for edge/global updater. For everything but the output transformation.
Decoder output dimensions
32
Activation function
ReLU
Edge vertex aggregator
Variable to global aggregator
average
Edge global aggregator
average Layer Normalisation
Normallsation
After each GN updater
13


Reviews:
[{"review_id": "HJgSqc7qFS", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 8, "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 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. \n\nOverall, 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. \n\nSome potential improvements:\n\n(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. \n(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. \n(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). \n", "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": "BkeMdpNkcr", "reviewer": "AnonReviewer2", "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 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.\n\nPros:\n- The paper is nicely written and easy to read.\n- 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.\n- The experiments provide interesting insights, especially Figure 2 and the graph coloring results in Table 3.\n\nCons:\n- 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).\n\n- 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.", "extra_scores": {"experience_assessment": "I have read many papers in 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 assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "BJgFQsXaFr", "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": "=== Summary ===\nThe 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.\nThe 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.\nThen 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).\nGQSAT 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).\n\n=== Recommendation ===\n\nThis paper is well-motivated (improving speed of complete SAT solvers) and presents a good overview of related work.\nThe 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)\nWhile 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.\n\nI slightly lean for rejecting this paper.\n\n=== Misc ===\n- Can the authors hypothesize on why GQSAT does not benefit from seeing more instances of SAT during training?\n- 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?\n- 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.\n- 'NeuroSAT cannot generalize from SAT to unSAT': the NeuroSAT paper showed that they could learn to predict satisfiability as well.", "extra_scores": {"experience_assessment": "I have read many papers in 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 assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

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