Title: IMPROVING SAT SOLVER HEURISTICS WITH GRAPH NETWORKS AND REINFORCEMENT LEARNING

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.

1. INTRODUCTION:

Boolean satisfiability (SAT) is an important problem for both industry and academia impacting various fields, including circuit design, computer security, artificial intelligence, automatic theorem proving, and combinatorial optimization. As a result, modern SAT solvers are well-crafted, sophisticated, reliable pieces of software that can scale to problems with hundreds of thousands of variables (Ohrimenko et al., 2009) .

SAT is known to be NP-complete (Karp, 1972) , and most state-of-the-art open-source and commercial solvers rely on multiple heuristics to speed up the exhaustive search, which is otherwise intractable. These heuristics are usually meticulously crafted using expert domain knowledge and are often iterated on using trial and error. In this paper, we investigate how we can use machine learning to improve upon an existing branching heuristic without leveraging domain expertise.

We present Graph-Q-SAT (GQSAT), a branching heuristic in a Conflict Driven Clause Learning (Marques-Silva & Sakallah, 1999; Bayardo Jr & Schrag, 1997, CDCL) SAT solver trained with value-based reinforcement learning (RL), based on DQN (Mnih et al., 2015) . GQSAT uses a graph representation of SAT problems similar to Selsam et al. (2018) which provides permutation and variable relabeling invariance. It uses a Graph Neural Network (Gori et al., 2005; Battaglia et al., 2018, GNN) as a function approximator to provide generalization as well as support for a dynamic state-action space. GQSAT uses a simple state representation and a binary reward that requires no feature engineering or problem domain knowledge. GQSAT modifies only part of the CDCL based solver, keeping it complete, i.e. always leading to a correct solution.

We demonstrate that GQSAT outperforms Variable State Independent Decaying Sum (Moskewicz 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 generalizes across problem types from SAT to unSAT. We also show, to a lesser extent, it generalizes to SAT problems from different domains, such as graph colouring. Finally, we show that some of these improvements are achieved even when training is limited to single SAT problem demonstrating data efficiency of our method. We believe GQSAT is 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:

A SAT problem involves finding variable assignments such that a propositional logic formula is satisfied or showing that such an assignment does not exist. A propositional formula is a Boolean expression, including Boolen variables, ANDs, ORs and negations. 'x' or 'NOT x' make up a literal. It is convenient to represent Boolean formulas in conjunctive normal form (CNF), i.e., conjunctions (AND) of clauses, where a clause is a disjunction (OR) of literals. An example of a CNF is (x 1 ∨ ¬x 2 ) ∧ (x 2 ∨ ¬x 3 ), where ∧, ∨, ¬ are AND, OR, and negation respectively. This CNF has two clauses: (x 1 ∨ ¬x 2 ) and (x 2 ∨ ¬x 3 ). 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, we focus on 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 a literal, assigns a variable a binary value. This is called a decision. After deciding, the solver simplifies the formula building an implication graph, and checks whether a conflict emerged. Given a conflict, it can infer (learn) new clauses and backtrack to the variable assignments where the newly learned clause becomes unit (consisting of a 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 a variable gets involved in a 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 a tuple S, A, R, T , ρ, γ with a set of states S, a set of actions A, a reward function R = R(s, a, s ) and the transition function T = p(s, a, s ), where p(s, a, s ) is a probability distribution, s, s ∈ S, a ∈ A. ρ is the probability distribution over initial states. γ ∈ [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 an optimal policy, a mapping which outputs an action or distribution over actions given the state, such that we maximize the expected discounted cumulative return R = E[ ∞ t=0 γ t r t ], where r t = R(s t , a t , s t+1 ) is the reward for the transition from s t to s t+1 . In Section 3 we apply deep Q-networks (Mnih et al., 2015, DQN) , a value-based RL algorithm that approximates an optimal Q-function, an action-value function that estimates the sum of future rewards after taking an action a in state s and following the optimal policy π thereafter:

Q * (s, a) = E π,T ,ρ [R(s, a, s ) + γ max a Q * (s , a )].

A mean squared temporal difference (TD) error is used to make an update step: L(θ) = (Q θ (s, a) -r -γ max a Qθ(s , a )) 2 . Qθ is called a target network (Mnih et al., 2015) . It is used to stabilise DQN by splitting the decision and evaluation operations. Its weights are copied from the main network Q θ after each k minibatch updates. We use Graph Neural Networks (Gori et al., 2005, GNN) to approximate our Q-function due to 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 of functions that take a labeled graph as input and output a graph with modified labels but the same topology.

0,1 0,1 0,1 0,1 1,0 1,0 0,1 0,1 x1 x2 x3 c1 c2 [1,0] [1,0] [1,0] [0,1] [0,1]

Here, a graph is a directed graph V, E, U , where V is the set of vertices, E is the set of edges with e = (s, r) ∈ E, s, r ∈ V , and U is a 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. A GNN changes this features as a result of its operations.

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 compute 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-Decode architecture (Battaglia et al., 2018) processes the graph in a recurrent way, enabling information propagation between remote vertices.

3. GQSAT:

As noted in Section 2.2, we use the MDP formalism for our purposes. Each state of our MDP consists of unassigned variables and unsatisfied clauses containing these variables. The initial state distribution is a distribution over all possible SAT problems. Our problem has an episodic nature with a clear terminal state: when a satisfying assignment is found or the algorithm has exhausted all the possible options proving unSAT. The action set includes two actions for each unassigned variable: assigning it to true or false. We modify the MiniSat-based environment of Wang & Rompf (2018) which is responsible for the transition function. It takes the actions, modifies its implication graph internally and returns a new state, containing newly learned clauses and without the variables removed after the propagation. Strictly speaking, this state is not fully observable. In the case of a conflict, the solver undoes the assignments for variables that are not in the agent's observation. However, in practice, this should not inhibit the goal of quickly pruning the search tree: the information in the state is enough to pick a variable that leads to more propagations in the remaining formula.

We use a simple reward function: the agent gets a negative reinforcement p for each non-terminal transition and 0 for reaching the terminal state. This reward encourages an agent to finish an episode as quickly as possible and does not require elaborate reward shaping to start using GQSAT.

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 (x i , c i ) means that a clause c i contains literal x i . If a 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 a variable or a 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 1a gives an example of the state for (x 1 ∨ x 2 ) ∧ (¬x 2 ∨ x 3 ).

3.2. Q-FUNCTION REPRESENTATION:

We use the encode-process-decode architecture (Battaglia et al., 2018 ), which we discuss in more detail in Appendix B.1. Similarly to Bapst et al. (2019) , our GNN labels variable vertices with Qvalues. Each variable vertex has two actions: pick the variable and set it to true or false as shown on Figure 1b . We choose the action which gives the maximum Q-value across all variable vertices. The graph contains only unassigned variables so all actions are valid. We use common DQN techniques such as memory replay, target network and -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., 2016) .

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-Y, where SAT means that all problems are satisfiable, unSAT stands for all problems are unsatisfiable. X and Y stands for the number of variables and clauses in the initial formula.

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 to 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 unSAT (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 a 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 on 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 our models using Pytorch (Paszke et al., 2017) and Pytorch Geometric (Fey & Lenssen, 2019) . We provide all the hyperparameters needed to reproduce our results in Appendix B. We will release our experimental code as well as the MiniSat gym environment. 

4. EXPERIMENTAL RESULTS:



4.1. IMPROVING UPON VSIDS:

In our first experiment, we consider whether it is possible improve upon VSIDS using no domain knowledge, a simple state representation, and a simple reward function. The first row in Table 2 gives us a 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 4.18). 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, on 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 at the beginning of the solution procedure before we hand the control back to VSIDS. The results of the experiment in Figure 2 support this hypothesis. Even if our model is used for only the first ten iterations, it 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 our focus, however even with the current unoptimized implementation, if we use the model for the first 500 iterations and assuming this gives us a 2x reduction in total iterations, our approach is competitive if it takes more than 20 seconds for a base solver to solve the problem. Table 2 shows that GQSAT has no difficulties generalizing to bigger problems, showing almost 4x improvement in iterations for the dataset 5 times bigger than the training set. GQSAT on 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, our 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 et al., 2018) .

The performance is, however, worse than the performance on satisfiable problems. On the one hand, SAT and unSAT problems are 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 is 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 a random 3-SAT problem looks much different than that of a 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 in the benchmark are satisfiable.

Table 3 shows a 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 3 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/test dataset using flat-75-80 for training and flat-100-239 to do model selection. We use the same hyperparameters as in all previous experiments changing only the gradient clipping parameter to 0.1. The results on Table 4 show that GQSAT can scale to bigger problems on the flat graph coloring benchmark. Apart from scaling to bigger graphs, we could test scaling for longer episodes. Table 1 shows exponential growth in the number of iterations it takes MiniSat to solve larger problems. Our preliminary experiments show that generalizing is easier than learning. Learning on SAT-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 in 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 on RL with GNN.

4.3. DATA EFFICIENCY:

We design our next experiment to understand how many different SAT problems GQSAT needs to learn from. We varied the SAT-50-218 train set from a single problem to 800 problems. Figure 3 demonstrates that GQSAT is extremely data efficient. Having more data helps in most cases but, even with a single problem, GQSAT generalizes across problem sizes and to 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 a single instance. In supervised learning, the data diversity is addressed at the training data generation step.

5. RELATED WORK:

Using machine learning for the SAT problem is not a new idea (Haim & Walsh, 2009; Grozea & Popescu, 2014; Flint & Blaschko, 2012; Singh et al., 2009) . Xu et al. (2008) propose a portfoliobased approach which yielded strong results in 2007 SAT competition. Liang et al. (2016) treat each SAT problem as a 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 a problem end-to-end or learning heuristics while keeping the algorithm backbone the same. Selsam et al. (2018, NeuroSAT) take an end-to-end supervised learning approach demonstrating that GNN can generalize to 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. Moreover, the method is incomplete and might generate incorrect results, which is extremely important especially for unSAT 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 an extensive training set including over 150,000 data points. Amizadeh et al. (2018) propose an end-to-end GNN architecture to solve circuit-SAT problems. While their model never produces false positives, it cannot solve unSAT problems.

The following methods take the second approach learning a branching heuristic instead of learning an algorithm end-to-end. Jaszczur et al. (2019) take the supervised-learning approach using the same graph representation as in Selsam et al. (2018) . The authors show a 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 a 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 to 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 to 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 approaches differ mainly in the state representation. They use 30 variables for the global state encoding 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 polarities. Also, Lederman et al. (2018) Cai et al. (2019) use RL to find a suboptimal solution that is 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 is 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 a lot of attention in the RL community, enabling the study of RL agents in state/action spaces of dynamic size, which is crucial for generalization beyond the given task. 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 or 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 to VSIDS. GQSAT uses a 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.5-2X from SAT to unSAT. We showed how GQSAT improves VSIDS and showed that our method is data efficient. While our method generalizes across problem structures to a lesser extent, we showed that training on 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 experiments 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 shaping, etc. Further research will focus on scaling GQSAT using latest stabilizing techniques (Hessel et al., 2018) , more sophisticated exploration methods and curriculum learning.

From reducing iterations to speeding up. SAT heuristics are good because they are fast. It takes constant time to make a decision with VSIDS. GNN inference takes much longer. However, our experiments show that GQSAT can show an 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 problems is related to the problem complexity. We are interested in understanding how graph structure influences the performance of GQSAT and how we can exploit this knowledge to improve GQSAT.

Although we showed the powerful generalization properties of graph-based RL, we believe the problem is still far from solved and our work is just one stepping stone towards a new generation of solvers that can discover and exploit heuristics that are too difficult for a human to design. 

:



Figures and Tables:

(a) Bipartite graph representation of the Boolean formula (x1 ∨ x2) ∧ (¬x2 ∨ x3). The numbers next to the vertices distinguish variables and clauses. Edge labels encode literal polarities. The global component does not contain any information about the state.

Graph Q-function values for setting variables to true and false respectively. The action is 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.

Figure 1: State-action space representation of GQSAT

Figure 2: GQSAT number of maximum first decisions vs performance. GQSAT shows improvement starting from 10 iterations confirming our hypothesis of VSIDS initialization problem. Best viewed in colour.

Figure 3: Dataset size effect on generalization.While GQSAT profits from having more data in most of the cases, it is able to generalize even from one data point. Model is trained on SAT-50-218. Best viewed in colour.

Figure 4: Average number of variable assignments change per step for (un)SAT-50-218 and (un)SAT-100-430.

Figure 5: Encode-Process-Decode architecture. Encoder and Decoder are independent graph networks, i.e. MLPs taking whole vertex/edge data array as a batch. k is the index of a message passing iteration. When concatenating for the first time, encoder output is concatenated with zeros.

Number of iterations (no restarts) it takes MiniSat to solve random 3-SAT instances.

Table content: <table><tr><td>dataset</td><td>median</td><td>mean</td></tr><tr><td>SAT 50-218</td><td>38</td><td>42</td></tr><tr><td>SAT 100-430</td><td>232</td><td>286</td></tr><tr><td>SAT 250-1065</td><td>62 192</td><td>76 120</td></tr><tr><td>unSAT 50-128</td><td>68</td><td>68</td></tr><tr><td>unSAT 100-430</td><td>587</td><td>596</td></tr><tr><td colspan="3">unSAT 250-1065 178 956 182 799</td></tr></table>

MRIR for GQSAT trained on SAT-50-218. Evaluation for SAT-50-218 is on a separate test data not seen during training.

Table content: <table><tr><td>dataset</td><td>mean min max</td></tr><tr><td>SAT 50-218</td><td>2.46 2.26 2.72</td></tr><tr><td>SAT 100-430</td><td>3.94 3.53 4.41</td></tr><tr><td>SAT 250-1065</td><td>3.91 2.88 5.22</td></tr><tr><td>unSAT 50-128</td><td>2.34 2.07 2.51</td></tr><tr><td>unSAT 100-430</td><td>2.24 1.85 2.66</td></tr><tr><td colspan="2">unSAT 250-1065 1.54 1.30 1.64</td></tr></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.

Table content: <table><tr><td>dataset</td><td colspan="3">variables clauses MiniSat median iterations</td><td colspan="2">GQSAT MRIR average min max</td></tr><tr><td>flat-30-60</td><td>90</td><td>300</td><td>10</td><td>1.51</td><td>1.25 1.65</td></tr><tr><td>flat-50-115</td><td>150</td><td>545</td><td>15</td><td>1.36</td><td>0.47 1.80</td></tr><tr><td>flat-75-80</td><td>225</td><td>840</td><td>29</td><td>1.40</td><td>0.31 2.06</td></tr><tr><td>flat-100-239</td><td>300</td><td>1117</td><td>55</td><td>1.44</td><td>0.31 2.38</td></tr><tr><td>flat-125-301</td><td>375</td><td>1403</td><td>106</td><td>1.02</td><td>0.32 1.87</td></tr><tr><td>flat-150-360</td><td>450</td><td>1680</td><td>179</td><td>0.76</td><td>0.37 1.40</td></tr><tr><td>flat-175-417</td><td>525</td><td>1951</td><td>272</td><td>0.67</td><td>0.44 1.36</td></tr><tr><td>flat-200-479</td><td>600</td><td>2237</td><td>501</td><td>0.67</td><td>0.54 0.87</td></tr><tr><td colspan="3">4.2 GENERALIZATION PROPERTIES OF GQSAT</td><td/><td/><td/></tr><tr><td colspan="3">4.2.1 GENERALIZATION ACROSS PROBLEM SIZES</td><td/><td/><td/></tr></table>

GQSAT Median Relative Iteration Reduction (MRIR) for the model trained on flat-75-80, evaluated on flat-100-239. flat-75-80 and flat-100-239 are separated, because the model was trained using the former and validated on the second. The results are for five training runs.

Table content: <table><tr><td>dataset</td><td colspan="2">GQSAT MRIR average min max</td></tr><tr><td>flat75-180</td><td>2.44</td><td>2.25 2.70</td></tr><tr><td>flat-100-239</td><td>2.89</td><td>2.77 2.98</td></tr><tr><td>flat-30-60</td><td>1.74</td><td>1.33 2.00</td></tr><tr><td>flat-50-115</td><td>2.08</td><td>2.00 2.13</td></tr><tr><td>flat-125-301</td><td>2.43</td><td>2.20 2.66</td></tr><tr><td>flat-150-360</td><td>2.07</td><td>2.00 2.11</td></tr><tr><td>flat-175-417</td><td>1.98</td><td>1.69 2.21</td></tr><tr><td>flat-200-479</td><td>1.70</td><td>1.38 1.98</td></tr></table>

use separate vertices for x and ¬x in the graph representation.Vinyals et al. (2015) introduce a recurrent architecture for approximately solving complex geometric problems, such as the Traveling Salesman Problem (TSP), approaching it in a supervised way.Bello et al. (2016) consider combinatorial optimization problems with RL, showing results on TSP and the Knapsack Problem.Khalil et al. (2017) approach combinatorial optimization using GNNs and DQN, learning a heuristic that is later used greedily. It is slightly different from the approach we take since their heuristic is effectively the algorithm itself. We augment only a part of the algorithmthe branching heuristic.Paliwal et al. (2019) use GNN with imitation learning for theorem proving.Carbune et al. (2018) propose a general framework of injecting an RL agent into existing algorithms.

Table content: <table/>

Peer review (iclr2020):
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.