Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning
Authors: Gil Lederman
Markus Rabe
Sanjit Seshia
Edward A. Lee
Venue:  (2020)
Keywords: Logic
QBF
Logical Reasoning
SAT
Graph
Reinforcement Learning
GNN

Abstract: We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking search algorithm, which can already solve formulas of impressive size - up to hundreds of thousands of variables. The main challenge is to find a representation of these formulas that lends itself to making predictions in a scalable way. For a family of challenging problems, we learned a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.

Published as a conference paper at ICLR 2020
LEARNING HEURISTICS FOR QUANTIFIED BOOLEAN FORMULAS THROUGH REINFORCEMENT LEARNING
Gil Lederman
Markus N. Rabe
Electrical Engineering and Computer Sciences University of Californaa at Berkeley gilledèeecs www.weey..ee.e...............ee. edu
Google Research
mrabeegoogle..com
Edward A. Lee
Sanjit A. Seshia Electrical Engineering and Computer Sciences University of California at Berkeley ssesh i a aêeecs. berke rrkeeey.... edu
Electrical Engineering and Computer Sciences University of California at Berkeley ea Beees.e.............e....eee.... berkeley. eduu edu
ABSTRACT
We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on backtracking search algorithm, which can already solve formulas of impressive size up to hundreds of thousands of variables. The main challenge is to find a representation of these formulas that lends itself making predictions way. For family of challenging problems in 2QBF we learn a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.
scalable
INTRODUCTION
One of the most intriguing questions for artificial intelligence is: can (deep) learning be effectively used for symbolic reasoning? The benefits of combining deductive reasoning with inductive learning for automated reasoning and in formal methods for system design have been noted (e.g., see (Seshia (2015)). There is a whole spectrum of approaches to combine them: One extreme to use learning for predicting which of small pool of algorithms (or heuristics) performs best, and run only that one to solve the given problem (e.g. SATzilla (Xu et al. 2008)). This approach is clearly limited by the availability of handwritten algorithms and heuristics (i.e. it can only solve problems for which we have written at least one algorithm that can solve it). The other extreme is to analyze formulas solely with deep learning approaches (Allamanis et al.) 2016 Evans et al.) 2018 Selsam et al. 2018 Amizadeh et al.) 2019). However, this approach shows poor scalability compared to the state-of Mfte-of-the-ard thrt in the respective domains depsite the recent breakthroughs in deep learning. Instead of relying entirely on deep learning or on the availability of good handwritten algorithms, we explore the middle ground. We ask the question how tightly combine deep learning with formal reasoning algorithms with the goal to improve the state-of-the i.e. to solve formulas that could not be solved previously.
Existing formal reasoning tools work in a mechanical way: they only apply small number of carefully crafted operations and use heuristics to resolve the degrees of freedom how to apply them. We address the problem of automatically learning better heuristics for given set of formulas. We focus on the branching heuristic in modern backtracking search algorithms, as they are known have high impact the performance of the algorithm. We cast the problem to learn better branching heuristics for backtracking search algorithms as a reinforcement learning problem: Initially, the reinforcement learning environment randomly picks formula from given set of formulas, and then runs the backtracking search algorithm on that formula. The actions that are controlled by the learning agent the branching decisions, i.e. pick variable and assign it value everything else is handled by the solver.
Challenges
This reinforcement learning problem comes with several unique challenges:

---

Published as a conference paper at ICLR 2020
Representation:
While learning algorithms for images and board-gandn gannes usually rely the grid-like structure of the imput and employ neural networks that match that structure (e.g. convolutional neural networks). For formulas, however, there is standard representation for learning algorithms.
may seem reasonable to treat Boolean formulas as text and learn embeddings for formulas through techniques such word2vec (Mikolov al., 2013), LSTMs, tree RNNs. However, formulas in formal reasoning tools typically consist of thousands of variables, which is much larger than the text-fragments typically analyzed with neural networks. Further, unlike words in natural language, individual variables in Boolean formulas are completely devoid of meaning. The meaning of variable one formula is basically independent from variable in a second formula. Hence, learning embeddings for variables and sharing them between formulas would be futile.
Unbounded action space: An action consists of choice of variable and value. While values will be Boolean, the number of variables depends on the size of the input formula. Therefore, we have an unbounded number of actions, which are further different for every formula.
Length of episodes: As we are dealing with a highly complex search problem, solver runs (= learning episodes) can be very long-in fact, for many of the formulas we have never observed a terminating run-and we observed a huge variance in the length of runs.
Performance: Our aim to solve more formulas in less time. The use of neural networks incurs a huge runtime overhead for each decision (the solver takes 2 10x fewer decisions per second). So the decisions taken by the neural networks need to dramatically better than the handcoded heuristic decisions outweigh their runtime cost.
Correctness: Reinforcement learning algorithms have shown to often find and exploit subtle im- plementation errors in the environment, instead of solving the intended problem. While testing and manual inspection of the results is feasible approach for board games and Atari games, it is neither possible nor sufficient in large-scale formal reasoning manually and even tiny mistake can invalidate the result. In order to ensure correctness, we need an environment with the ability to produce formal proofs, and check the proofs by an independent tool.
solver
is simply too large to inspect
Quantified Boolean Formulas In this paper we focus on 2QBF, that is quantified Boolean formulas of the form V..EY.4p. where X and Y are sets of Boolean variables and is in conjunctive normal form. 2QBFs are complex enough to serve as an interesting proxy for complex mathematical reasoning tasks. Challenging applications such as program synthesis and the synthesis of controllers and ranking functions have been encoded into 2QBFs [Solar-Lezams et al. (2006); |Famonville et al.) (2017); Cook et al.] (2013). However, the problem definition and also the syntactical structure of 2QBF is simple compared to more general settings, such as first-order or even higher-order logics. This makes algorithms for 2QBF good target for the study of neural architectures.
While our approach in principle works with most algorithms for QBF, we decided to demonstrate its use in Incremental Determinization (Rabe & Seshia 2016). We modified CADET, an open- source implementation of Incremental Determinization that performed competitively in recent QBF competitions (Pulina 2016) and turned it into reinforcement learning environment. The advantage of CADET in the context of reinforcement learning is its ability to produce proofs (which most other solvers do not), which ensures that the reinforcement learning cannot simply learn exploit bugs in the environment.
Graph Neural Networks We consider each constraint and each variable of given formula as node in graph. Whenever a variable occurs constraint, we draw an edge between their nodes. We then use a Graph Neural Network (GNN) (Scarselli et al. (209)) to predict the quality of each variable as a decision variable, and pick our next action accordingly. GNNs allow us to compute an embedding for every variable, based the occurrences of that variable in the given formula, instead of learning an embedding that is shared across all formulas. Based on this embedding, we then use policy network predict the quality of each variable (or literal), and choose the next action accordingly. GNNs also allow us to scale to arbitrarily large formulas with a small and constant number of parameters.
2

---

Published as a conference paper at ICLR 2020
This paper presents the successful integration of GNNs in a modern automated reasoning algorithm in a reinforcement learning setup I Our approach balances the performance penalty incured by the use of neural networks with the impact that improved heuristic decisions have on the overall reasoning capabilities. The branching heuristic that we learn significantly improves CADET's reasoning capabilities on the test set of the benchmark, i.e. it solves more formulas within the same resource constraints. This is huge step towards replacing VSIDS, the dominant branching heuristic in CDCL-based solvers for the last 20 years Moskewicz al. (200Tb); Ečn & Sörensson (2003): Biere et al. 2009); Lonsing & Biere 2010); Rabe & Seshia (2016).
Contributions
We also study the generalization properties of our approach: We show that training heuristic on small and easy formulas helps us to solve much larger and harder formulas; generalization to formulas from different benchmarks is still limited though. Further, we provide an open-source learning environment for reasoning in quantified Boolean formulas. The environment includes the ability to verify its own runs, and thereby ensures that the reinforcement learning agent does not only learn to exploit implementation errors of the environment.
Structure: After a primer on Boolean logics in Section 2 we define the problem Section 3 and
describe the network architecture in Section 4 We describe our experiments in Section 5 discuss related work in Section 6 and present our conclusions in Section 7
2 BOOLEAN LOGICS AND SEARCH ALGORITTM
We start with describing propositional (i.e. quantifier-free) Boolean logic. Propositional Boolean logic allows us to use the constants 0 (false) and 1 (true), variables, and the standard Boolean operators like A ("and"), V ("or"), and - -(not")
literal of variable v is either the variable itself or its negation -v. By we denote the logical negation of literal 1. We call a disjunction of literals a clause and say that a formula is in conjunctive normal form (CNF), if it is a conjunction of clauses. For example, (x V y) A (-z V y) is in CNF It is well known that any Boolean formula can be transformed into CNF. It is less well known that this increases the size only linearly, if we allow the transformation to introduce additional variables Tseitin 1968). We thus assume that all formulas in this work are given in CNF.
DPLL and CDCL. The satisfiability problem of propositional Boolean logics (SAT) is to find satisfying assignment for given Boolean formula or to determine that there is no such assignment. SAT is the prototypical NP-complete problem and many other problems in NP can be easily reduced to it. The first backtracking search algorithms for SAT are attributed to Davis, Putnam, Logemann, and Loveland (DPLL) (Davis Putnam 1960; Davis al.) 1962). Backtracking search algorithms gradually extend a partial assignment until it becomes a satisfying assignment, or until a conflict is reached. conflict reached when the current partial assignment violates one of the clauses and hence cannot be completed to a satisfying assignment. In case of conflict, the search has to backtrack and continue in a different part of the search tree.
Conflict- clause learning (CDCL) is significant improvement over DPLL due to Marques- Silva and Sakallah (Marques-Sile & Sakallah 1997). CDCL combines backtracking search with clause learning. While DPLL simply backtracks out of conflicts, CDCL "analyzes" the conflict by performing a couple of resolution steps. Resolution is an operation that takes two existing clauses (1, v... v l.)) and (1 V... V (2,) that contain pair of complementary literals 4 -1i. and derives the clause (12 V ... V in V 12 V .... V I,,). Conflict analysis adds new clauses over time, which cuts off large parts of the search space and thereby speeds up the search process.
Since the introduction of CDCL in 1997, countless refinements of CDCL have been explored and clever data structures improved its efficiency significantly (Moskewicz al. 200 Eén & Sörensson
2003, Goldberg & Novikov] 2007). Today, the cop-performing SAT solvers, such as Lingeling (Biere
2010, Crypominisat (Soos) 2014), Glucose (Audemard & Simon [2014), [im04]2014), and MapleSAT (Liang et al.
2016), all rely on CDCL and they solve formulas with millions of variables for industrial applications
such as bounded model checking (Biere et al. 2003).
An earlier version of this work was published https://anx.w.or///bbs..
3

---

Published as a conference paper at ICLR 2020
Quantified Boolean Formulas. QBF extends propositional Boolean logic by quantifiers, which are statements of the form "for all x" (vz) and "there is an x" (Ez). The formula Vz. yp is true if, and only if, o is true if is replaced by 0 (false) and also if is replaced by (true). The semantics of 3 arises from Ax. 4 -Yar. mp. We say that QBF is in prenex normal form if all quantifiers are in the beginning of the formula. W.I.o.g., we will only consider QBF that are in prenex normal form and whose propositional part is in CNF. Further, we assume that for every variable in the formula there is exactly one quantifier in the prefix. An example QBF in prenex CNF is Vx. By. (x V y) (-r y).
We focus on 2QBF, a subset of QBF that admits only one quantifier alternation. W.l.o.g. we can assume that the quantifier prefix of formulas in 2QBF consists of a sequence of universal quantifiers Vxi....aa Vzn, followed by sequence of existential quantifiers Byz ... Zym. While 2QBF is less powerful than QBF, we can encode many interesting applications from verification and synthesis, e.g. program synthesis (Solar-Lezaaa et al., 2006 Alur et al., 2013). Solvers for (2)QBF typically address the decision problem to determine the truth of a given formula (TQBF). After the success of
CDCL for SAT, CDCL-like algorithms have been explored for QBF as well (Giunchiglia et al. |000 Lonsing & Biere 2010 Rabe & Seshia 2016 Rabe et al. 2018). We focus on CADET, solver that implements Incremental Determinization generalized CDCL backtracking search algorithm (Rabe) & Seshia 2016) Rabe et al.] 2018). Instead of considering only Booleans as values, the Incremental Determinization algorithm assigns and propagates on the level of Skolem functions. For the purpose of this work, however, we do not have to dive into the details of Incremental Determinization and can consider it simply as some backtracking algorithm.
Correctness. Writing performant code is an error- arror-prone task, and correctness is critical for many applications of formal reasoning. Some automated reasoning tools hence have the ability to produce proofs, which can be checked independently. CADET is one of the few QBF solvers that can produce proofs without runtime overhead. We believe that the ability to verify results of solvers is particularly crucial for learning applications, it allows us ensure that the reinforcement learning algorithm does not simply exploit implementation error (bugs) in the environment.
3 PROBLEM DEFINITION
In this section, we first revisit reinforcement learning and explain how it maps to the setting of logic solvers. In reinforcement learning, consider an agent that interacts with an environment & which is modeled as a Markov Decision Process (MDP) over discrete time steps and accumulates reward. Formally, a MDP is a 4-tuple of states S, action space A. transition probabilities P and reward function R. A policy is mapping from states to probability distributions over the actions : S - dist (.).. The goal of the agent is maximize the expected (possibly discounted) reward accumulated over the episode; formally [(r = E (E 7/re/=].
In our setting, the environment & is the solver CADET (Rabe & Seshia 2016). The environment is deterministic except for the initial state, where formula is chosen randomly from a distribution. At each time step. the agent gets an observation, which consists of the formula and the solver state. Only those variables that do not have value yet are valid actions, and we assume that the observation includes the set of available actions. The agent then selects one action from the subset of the available variables. Formally, the space of actions is the set of all variables in all possible formulas in all solver states, where at every state only a small finite number of them is available. Practically, the agent will never see the effect of even small part of these actions, and it must generalize unseen actions. An episode is the result of the interaction of the agent with the environment. We consider an episode to be complete, if the solver reaches terminating state in the last step. As there are arbitrarily long episodes, we want to abort them after some step limit (the decision limit) and consider these episodes as incomplete.
3.1 BASELINES
While there are no competing learning approaches yet, human researchers and engineers have tried many heuristics for selecting the next variable. VSIDS is the best known heuristic for the solver we consider. It has been a dominant heuristic for SAT and several CDCL-based QBF algorithms for over 20 years now Moskewicz et al. (2001b); Eén & Sörensson (2003); Biere et al. (2009): Lonsing &
Biere 2010):
Rabe & Seshia (2016). We therefore consider VSIDS the main baseline. VSIDS
4

---

Published as a conference paper at ICLR 2020
probabilities E 2
Softmax
qual. of
qual. of -l
Policy NN
Policy NN
$g
5g
emb. of
emb. of 7
Encoder GNN
A. Vi...ry Vas Cly... Cm
Figure 1:
Sketch of the architecture for a formula with n variables by and m clauses. so is the global state of the solver, .A is the adjacency matrix, and V, and e, are the variable and clause labels.
maintains an activity score per variable and always chooses the variable with the highest activity that still available. The activity reflects how often a variable recently occurred in conflict analysis. To select literal of the chosen variable, VSIDS uses the Jeroslow- Prroslow-Wangge heuristic (Jeroslow & Wang) 1990), which selects the polarity of the variable that occurs more often, weighted by the size of clauses they occur in. For reference, also consider the Random heuristic, which chooses of the available actions uniformly at random.
4 THE NEURAL NETWORK ARCHITECTURE
Our model gets an observation, consisting of a formula and the state of the solver, and selects one of the formula's literals (= variable and a Boolean value) its action. The model has two components: An encoder that produces an embedding for every literal, and policy network that that rates the quality of each literal based its embedding. We give overview of the architecture in Fig. I describe the GNN in Subsection 4.1 and the policy network in Subsection
4.1 A GNN ENCODER FOR BOOLEAN FORMULAS
In order employ GNNs, view the formula a graph, where each clause and each literal a node (see Fig. 2] For each literal in each clause, we draw an edge between their nodes. The resulting graph bipartite and hence, we represent its edges an 2n x m adjacency matrix AA with values f0, 1). where 2n is the number of literals and is the number of clauses. This graph structure determines the semantics of the formula except for the quantification of variables (i.e. whether variable is universally existentially quantified), which are provided as labels to the vari- ables. For each variable v, the variable label RR with xv 7, indicates whether the variable is universally existentially quanti- fied, whether currently has a value assigned, and whether it was selected as decision variable already We use the variable label for both of its literals and by Vi we denote the label of the variable of For each clause c, the clause label E R is single scalar (in {0, 1)), indicating whether the clause was original or derived during conflict analysis.
(r V y)
V y)
7V
Figure 2: The bipartite graph
the current search branch.
for (x V y) A (-z V y).
While we ultimately only interested in embeddings for literals, GNN also computes embed- dings for clauses as intermediate values. Literal embeddings have dimension 6, = 16 and clause embeddings have dimension &c 64. The GNN computes the embeddings rounds. We define
5

---

Published as a conference paper at ICLR 2020
the initial literal embedding to = 0, and for each round 1 < t S define the literal embedding 4 E I2 for every literal and the clause embedding Ct E &e for every clause с C C as follows:
G: (ico Wr.lv. 4-11--11= + Br.), and ReLU ReLU(Eccee Wolc ,c]] Be).
The trainable parameters of our model are indicated as bold capital letters. They consist of the matrix WL of shape (28g + Ay. &c), the vector Bg of dimension éc, the matrix We of shape (6c tc. 6L), and the vector Be of dimension òz.
Invariance properties. The meaning of formula in CNF invariant under permutations of its clauses and of literals within each clause due to the commutativity of conjunction and disjunction. Our GNN architecture is invariant under these reorderings, as both conjunctions and disjunctions are computed through commutative operations (a sum), and, therefore, it cannot accidentally overspecialize to the ordering of clauses or literals. Swapping the literals of a variable does not change the truth of the formula either, and our GNN architecture respects that as well. The only place in our architecture where we use the information of which literals belong to the same variable is in the input to q, Depending on which literal of a variable occurs in the clause we order its literal embeddings differently. Lastly, note that variables are completely nameless in our representation.
4.2 POLICY NETWORK
The policy network predicts the quality of each literal based on the literal embedding and the global solver state. The global solver state is collection of ÀG 5 values that include only the essential parts of solver state that are not associated with any particular variable or clause We provide additional details in Appendix A The policy network thus maps the final literal embedding [v ] concatenated with the global solver state to a single numerical value indicating the quality of the literal. The policy network thus has λv + 20,, + Ao inputs, which are followed by two fully-connected layers. The two hidden layers use the ReLU nonlinearity. We turn the predictions of the policy network into action probabilities by a masked softmax. We mask all "illegal" actions, effectively ignoring the embeddings of variables which are universal, or are assigned already.
Note that the policy network predicts a score for each literal independently. All information about the graph that is relevant to the policy network must hence flow through the literal embedding. Since we experimented with graph neural networks with few iterations this means that the quality of each literal is decided locally. The rationale behind this design is that it is simple and efficient.
5 EXPERIMENTS
We conducted several experiments to examine whether improve the heuristics of the logic solver CADET through our deep reinforcement learning approach.
QI Can we learn to predict good actions for a family of formulas?
Q2 How does the policy trained on short episodes generalize to long episodes?
Q3 How well does the learned policy generalize to formulas from different family of formulas?
Q4 Does the improvement in the policy outweigh the additional computational effort? That is, can we solve more formulas in less time with the learned policy?
5.1 DATA
In contrast to most other works in the area, we evaluate our approach over a benchmark that (1) has been generated by a third party before the conception of this paper, and (2) is challenging state- of-the-art solvers in the area. We consider a set of formulas representing the search for reductions between collections of first-order formulas generated by Jordan & Kaiser (2013). which we call Reductions in the following, Reductions is interesting from the perspective of QBF solvers, as its formulas are often part of the QBF competition. consists of 4608 formulas of varying sizes and with varying degrees of hardness. On average the formulas have 316 variables; the largest formulas the set have over 1600 variables and 12000 clauses. We filtered out 2573 formulas that are solved
We provide the code and data of our experiments i wttphhhttt//ttttoeeee com www.o//////de.r.emmmo eeeeeederggggee http:////mm/edeeee/eee/nnnngggg/ hewgg/aaaangggrrrrr

---

Published as a conference paper at ICLR 2020
10a
time limit in seconds
103
VSIDS
decision limit
10
Learned
10a
10
Random
10
10a
VSIDS
Learned
10
10
10-2
0
20
40
60
20
60
100
120
solved formulas
solved formulas
Figure 3: Two cactus plots showing how the number solved formulas from the test set grows with increasing resource bounds. Left: Comparing the number of formulas solved with growing decision limit for Random, VSIDS, and our learned heuristic. Right: Comparing the number formulas solved with growing wall clock time. Lower and further the right is better.
without any heuristic decisions. In order enable us answer question (see above), further set aside a test set of 200 formulas, leaving us with a training set of 1835 formulas.
We additionally consider the 2QBF evaluation set of the annual competition of QBF solvers, QBFE- VAL (Pulina 2016). This will help us to study cross-benchmark generalization.
5.2 REWARDS AND TRAINING
We jointly train the encoder network and the policy network using REINFORCE (Williams 1992). For each batch we sample a formula from the training set, and generate episodes by solving multiple times. In each episode assign rewards to the episodes and estimate the gradient. We apply standard techniques to improve the training, including gradient clipping, normalization of rewards, and whitening of input data.
CADET for up 400 steps using the latest policy. Then
We assign a small negative reward of 10- for each decision to encourage the heuristic to solve each formula in fewer steps. When formula is solved successfully, we assign reward 1 to the last decision. In this way. we effectively treat unfinished episodes (>> 400 steps) as if they take 10000 steps, punishing them strongly.
5.3 RESULTS
We trained the model described in Section Jon the Reductions training set. We denote the resulting policy Learned and present the aggregate results in Figure as a cactus plot, usual for logic solvers. The cactus plot in Findicatess how the number of solved formulas grows for increasing decision limits the test of the Reductions formulas. In cactus plot, we record one episode for each formula and each heuristic. We then sort the runs of each heuristic by the number of decisions taken the episode and plot the series. When comparing heuristics, lower lines (or lines reaching further to the right) are thus better, as they indicate that more formulas were solved in less time.
We see that for a decision limit 400 (dashed line in Fig- 3 left), i.e. the decision limit during training, Learned solved significantly more formulas than either of the baselines. The advantage of Learned over VSIDS is about as large as VSIDS over purely random choices. This is remarkable for the field and we can answer QI positively.
Figure 3 (left) also shows us that Learned performs well far beyond the decision limit of 400 steps that was used during its training. Observing the vertical distance between the lines of Learned and VSIDS, we can see that the advantage of Learned over VSIDS even grows exponentially with an increasing decision limit. (Note that the axis indicating the number of decisions is log-scaled.) We can thus answer Q2 positively.
A surprising fact is that small and shallow neural networks already achieved the best results. Our best model uses 5 = 1, which means that for judging the quality of each variable, only looks at the variable itself and the immediate neighbors (i.e. those variables occurs together with in constraint).
7

---

Published as a conference paper at ICLR 2020
The hyperparameters that resulted in the best model are و1 16, dc 64, and 7 = 1, leading to model with merely 8353 parameters. The small size of our model was also helpful to achieve quick inference times.
To answer Q3, we evaluated the learned heuristic also on our second data set of formulas from the QBF solver competition QBFEVAL. Random solved 67 formulas, VSIDS solved 125 formulas, and Learned solved 111 formulas. The policy trained on Reductions significantly improved over random choices, but does not beat VSIDS. This is hardly surprising, as our learning approach specialized the solver to a specific--diffreett--e dii-firrrenttddiiiiiutiioo of formulas. Also it must be taken into account that the solver CADET has been tuned QBFEVAL over year, and hence may perform much stronger on QBFEVAL than on the Reductions benchmark. We include further cross cross-benchmary generalization studies in the Appendix.
To answer our last question, Q4, we compare the runtime of CADET in with our learned heuristic to CADET with the standard VSIDS heuristic. In Fig. B (right) we see that for small time limits (up to 10 seconds), VSIDS still solves more formulas than the learned heuristic. But, for higher time limits, the learned heuristic starts to outperform VSIDS. For a time limit of hour, we solved 120 formulas with the learned heuristic while only 110 formulas were solved with VSIDS (see right top corner). Conversely, for solving 1 10 formulas the learned heuristic required a timeout of less than 12 minutes, while VSIDS took hour. Furthermore, our learning and inference implementation is written in Python and not particularly optimized. The NN agent is running in a different process from CADET, and incurs overhead per step for inter-process communication and context switches, which is enormous compared to the pure C implementation of CADET using VSIDS, This overhead could be easily reduced, and so we expect the advantage of our approach to grow.
6 RELATED WORK
Independent from our work, GNNs for Boolean logic have been explored in NeuroSAT (Selsam al., (2018), where the authors use solve the SAT problem directly. While using similar neural architecture, the network is not integrated in a state-of-the-art logic solver, and does not improve the state of the art performance. Selsam & Bjørner 2019) recently extended NeuroSAT to use its predictions in a state-of tfee-oo-theeartt art SAT solver. In contrast to their work, we integrate GNNs much tigher into the solver and train the heuristies directly through reinforcement learning. Thus allow deep learning to take direct control of the solving process. Also, we focus on QBF instead of SAT, which strongly affects the runtime tradeoffs between spending time on "thinking" about a better decision versus executing many "stupid" decisions.
Amizadeh et al. 2019) suggest an architecture that solves circuit-SAT problems. Unlike NeuroSAT, and similar to our approach, they train their model directly to find satisfying assignment by using differentiable "soft" satisfiability score as their loss. However, like NeuroSAT, their approach aims to solve the problem from scratch, without leveraging an existing solver, and so is difficult to scale to state-of-the-arr performance. They hence focus on small random problems. In contrast, our approach improves the performance of a state-of-the-aar algorithm. Furthermore, our learned heuristic applies to SAT and UNSAT problems alike.
Yang et al. 2019 extended the NeuroSAT architecture 2QBF problems. In contrast to our work. they do not embed their GNN model in a modern DPLL solver, and instead try to predict good counter-examples for a CEGAR solving approach. They focus on formulas with 18 variables, which are trivial for state-of-thee -hrr solvers. Chen & Yang (201)) showed that a pure GNN approach is unable to solve Boolean formulas when they are unsatishable, which in our work is addressed by combining GNNs with logic reasoning engine.
Reinforcement learning has been applied to other logic reasoning tasks. Kaliszyk et al. (018))
recently explored learning linear policies for tableaux-style theorem proving. Kurin et al. (0199
follow a similar approach to ours for SAT solvers, but only evaluate on small synthetic formulas
and do not improve the overall performance of the underlying SAT solver. Kusumoto et al. (2018)
applied reinforcement learning to propositional logic in a setting similar to ours; just that we employ the learning in existing strong solving algorithms, leading to much better scalability. Balunovic et al.) (2018) use deep reinforcement learning to improve the application of high-level strategies in SMT solvers, but do not investigate tighter integration of deep learning with logic solvers. Also other
8

---

Published as a conference paper at ICLR 2020
works combinatorial search explored the use of GNNs (some trained with reinforcement learning)
for problems such as random SAT (Yolcu & Póczos 2019). coloring graphs (Huang et al. 2019). and MILP Gasse et al. 2019).
Most previous approaches that applicd neural networks to logical formulas used LSTMs or tree
models syntax-tree of formulas (Bowman al.] 2014 Irving et al.] 2016 Allamanis et al. 2016
Loos et al., [017] Evans et al., 2018: Chvalovsky [2019] Chen & Tian 2018) or classical ML
models (Gauthier et al. 2017]] Kaliszyk al. [018 Soos et al. 2019). Instead, we suggest GNN
approach, based on a graph-view on formulas in CNF, Recent work suggests that GNNs appear to be
good architecture for logics (Paliwal al.) 2019) Wang et al. 2017). Bansal et al. (2019); Huang et al.)
(2018): (Yag) & Deng 2019) provide a learning environments around interactive theorem provers.
Other competitive QBF algorithms include expansion- bbased algorithms (Biere, 2004 Pigorsch &
Scholl 2010), CEGAR- algorithms (Janota & Marques-Silva 2011 |015 Rabe & Tentrup
2015), circuit-based algorithms (Klieber) [entruup [016 Janota 2018a bj. and hybrids (Janota
al. 2012 [ennrrpp [0017). Recently, Janota 2a) successfully explored the use of (classical)
machine learning techniques to address the generalization problem QBF solvers.
7 CONCLUSIONS
We presented an approach to improve the heuristics of backtracking search algorithm for Boolean logic through deep reinforcement learning. Our approach brings together the best of two worlds: The superior flexibility and performance of intuitive reasoning of neural networks, and the ability to explain (prove) results in formal reasoning. The setting is new and challenging to reinforcement learning: QBF a very general, combinatorial problem class, featuring an unbounded input- size and action space. We demonstrate that these problems can be overcome, and reduce the overall execution time competitive QBF solver by a factor of 10 after training on similar formulas.
This work demonstrates the huge potential that lies in the tight integration of deep learning and logical reasoning algorithms, and hence motivates more aggressive research efforts in the area. Our experiments suggest two challenges that we want to highlight: (1) We used very small neural networks, and modd-coontrintutiivly--ee ones in our experiments. (2) The performance overhead due to the use of neural networks is large; however we think that with more engineering effort we could be significantly reduce this overhead.
neural networks were not able to improve over the small
Acknowledgements. This work was supported in part by National Science Foundation (NSF) grants CNS-1836601, CNS-1446619 CNS- and CCF-1837132, by the iCyPhy center, and by Berkeley Deep Drive. The second author was affiliated with UC Berkeley during the initial part of this work.
REFERENCES
Miltiadis Allamanis, Pankajan Chanthirasegaran, Pushmeet Kohli, and Charles Sutton. Learning continuous semantic representations of symbolic expressions. arXiv preprint arXiv: 161.v11611.011233 2016.
Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar- Leaam, Emina Torlak, and Abhishek Udupa. Syntax- guided synthesis. In Proceedings of the IEEE International Conference Formal Methods in Computer-Aided Design (FMCAD), pp. 1-17, October 2013.
Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. Learning to solve circuit-SAT: An unsupervised differentiable approach. ICLR, 2019.
Gilles Audemard and Laurent Simon. Glucose in the SAT 2014 competition. SAT COMPETITION 2014, pp. 31,2011 2014.
Lei Jimmy Ba, Ryan Kiros, and Geoffrey E. Hinton. Layer normalization. CoRR, abs/1677006450 2016. URL htttt://aaxiie http///xxw...rg/aabe/ org/abrg 607 06450

---

Published as a conference paper at ICLR 2020
Mislav Balunovic, Pavol Bielik, and Martin Vechev. Learning to solve SMT formulas. In NeurIPS. Curran Associates, Inc., 2018. URL http:///pppesssiss.ccom
8233- 223-Learning-to-solveees smt htt.rro-o-oo-eeeeeaeoooooomaaaa.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of oigher-order theorem proving. CoRR, abs/1904.03241, org/ aba/ abw/1904. 1904. C3241
2019. URL URRLAtt://aaxxt
Armin Biere. Resolve and expand. In International Conference on Theory and Applications of Satisfibilitty Testing (SAT). pp. 59-70. Springer, 2004.
Armin Biere. Lingeling, plingeling, picosat and precosat at sat race 2010. FMV Report Series Technical Report, 10(1), 2010.
Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, Yunshan Zhu, et al. Bounded model checking. Advances computers, 18(11):117-148, 2003.
Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009.
Samuel R Bowman, Christopher Potts, and Christopher D Manning. Recursive neural networks can learn logical semantics. arXiv preprint arXi:: 1827 2014.
Xinyun Chen and Yuandong Tian. Learning to progressively plan. CoRR, abs/1810.00337, 2018. URL
Ziliang Chen and Zhanfu Yang. Graph neural reasoning may fail in certifying boolean unsatisfiability, 2019.
Junyoung Chung, Çaglar Gülçehre, KyungHyun Cho, and Yoshua Bengio. Empirical evaluation of gated recurrent neural networks on sequence modeling. CoRR, abs/1412.3555, 2014. URL
htttp://arxiv.orge wttp://...rr/aab//22...... 3555
Karel Chvalovsky. Top-down neural model for formulae. In ICLR, 2019.
Byron Cook, Daniel Kroening, Philipp Rümmer, and Christoph M Wintersteiger. Ranking function synthesis for bit-vector relations. Formal methods in system design, 43(1):93-120, 2013.
Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM (JACM), 73):200 1960.
Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962.
Niklas Fén and Niklas Sörensson. An extensible SAT-solver. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 502-518. Springer, 2003.
Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? arXiv preprint arXiv: 1802.08335, 2018
Peter Faymonville, Bemn Finkbeiner, Markus N Rabe, and Leander Tentrup. Encodings of bounded synthesis. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 354-370. Springer, 2017.
Maxime Gasse, Didier Chételat, Nicola Ferroni, Laurent Charlin, and Andrea Lodi. Exact combina- torial optimization with graph convolutional neural networks. 2019.
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning reason with HOL4 tactics. EPiC Series in Computing, 46: 123-143, 2017.
Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. QUBE: A system for decid- ing quantified boolean formulas satisfiability. In International Joint Conference on Automated Reasoning, pp. 364-369. Springer, 2001.
10

---

Published as a conference paper at ICLR 2020
Eugene Goldberg and Yakov Novikov. Berkmin: A fast and robust sat-solver. Discrete Applied Mathematics, 155(12):159--1561 2007.
Daniel Huang, Prafulla Dhariwal, Dawn Song, and llya Sutskever. Gamepad: learning environment for theorem proving. arXiv preprint arXiv: 00608, 2018.
Jiayi Huang, Mostofa Patwary, and Gregory Diamos. Coloring big graphs with AlphaGoZero. arXiv preprint 1rxXiv:992..11622 2019.
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. NeurlPS, pp. 2235-2243, 2016.
Mikoláš Janota. Towards generalization in QBF solving via machine learning. AAAI Conference on Artificial Intelligence, 201 8a.
Mikoláš Janota. Circuit-based search space pruning in QBF. In International Conference on Theory and Applications of Satisfiability Testing (SAT). Springer, 2018b.
Mikoláš Janota and Joao Marques-Silva. Abstraction-based algorithm for 2QBF. In International Conference Theory and Applications of Satisfiability Testing (SAT), pp. 230-244. Springer, 2011.
Mikolás Janota and Joao Marques-Silva Solving QBF by clause selection. In ICCAI, pp. 325-331, 2015.
Mikoláš Janota, William Klieber, Joao Marques- Silva, and Edmund Clarke. Solving QBF with counterexample guided refinement. In International Conference on Theory and Applications of Satisfiability Testing (SA7), pp. 114-128. Springer, 2012.
Robert Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of mathematics and Artificial Intelligence, 111-4):167-187, 1990.
Charles Jordan and Eukasz Kaiser. Experiments with reduction finding. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 192-207. Springer, 2013.
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Mirek Olšák. Reinforcement learning of theorem proving. arXiv preprint arXiv:1805.07553 2018.
William Klieber. Ghostq QBF solver system description, 2012.
Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro. Improving SAT solver heuristics with graph networks and reinforcement learning. ArXiv, abs/1909. 111.0099.111,,,,..1 2019.
Mitsuru Kusumoto, Keisuke Yahata, and Masahiro Sakai. Automated theorem proving in intuitionistic propositional logic by deep reinforcement learning. arXiv preprint arXiv:1811.0077 007966 2018
Jia Hui Liang. Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for sat solvers. In International Conference on Theory and Applications of Satisfiability Testing (SA7), pp. 123-140. Springer, 2016.
Florian Lonsing and Armin Biere. DepQBF: A dependency-aware QBF solver. JSAT, 7(2-3):71-76. 2010.
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017.
João P Marques-Sin Silva and Karem A Sakallah. GRASP A new search algorithm for satisfiability. In Computer Aided Design, pp. 220-227. IEEE, 1997.
Tomas Mikolov, Kai Chen, Greg Corrado, and Jeffrey Dean. Efficient estimation word representa- tions in vector space. arXiv preprint arXiv: 2013.
Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference, pp. 530-535. ACM, 2001a.
11

---

Published as a conference paper at ICLR 2020
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings DAC, pp. 530-535. ACM, 2001b. ISBN 1-58113-297-2. doi: 10.1 00.114/7772299339017
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. CoRR, abs/ (bb//1905.10 10006, 2019. URL
http://arxiv. wwwpxxiv.org/bbob. htt///b///// /195. 1
Florian Pigorsch and Christoph Scholl. An AIG-based QBF-solver using SAT for preprocessing, In Proceedings of the 47th Design Automation Conference, pp. 170-175. ACM, 2010.
Luca Pulina. The ninth QBF solvers naauuationppreliminne report. In QBF@ SAT, pp. 1-13, 2016.
Markus N Rabe and Sanjit A Seshia. Incremental determinization, In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp- 375-392. Springer International Publishing, 2016.
Markus N Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In Formal Methods in Computer-Aided Design (FMCAD), 2015, pp. 143. IEEE, 2015.
Markus Rabe, Leander Tentrup, Cameron Rasmussen, and Sanjit A Seshia. Understanding and extending incremental determinization for 2QBF. In International Conference on Computer Aided Verification (accepted), 2018.
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfar- dini. The graph neural network model. Trans. Neur. Nenw., 20(1):1-800 January 2009. ISSN 1045-9227, doi: 10. 20C8 2005605
URL /tl.tttp//cx..d..orrrr /0
Daniel Selsam and Nikolaj Björner. Neurocore: Guiding high-performance SAT solvers with unsat-core predictions. CoRR, abs/1903.04671, 2019. URL
04671
Daniel Selsam, Matthew Lamm, Benedikt Bunz, Percy Liang, Leonardo de Moura, and David Dill. Learning a SAT solver from single-bit supervision. arXiv preprint arXiv:1802.03685 2018.
Sanjit A. Seshia. Combining induction, deduction, and structure for verification and synthesis. Proceedings of the IEEE, (03(11):2066-255) 2015.
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combina- torial sketching for finite programs. ACM Sigplan Notices, (11144:444415 2006.
Mate Soos. Cryptominisat v4. SAT Competition, pp. 23, 2014.
Mate Soos, Raghav Kulkarni, and Kuldeep S. Meel. Crystalball: Gazing in the black box of sat solving. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), 7 2019.
Leander Tentrup. Non- kon-prenex QBF solving using abstraction. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 393-401. Springer, 2016.
Leander Tentrup. On expansion and resolution in CEGAR based QBF solving. In International Conference Computer Aided Verification, pp. 475-494. Springer, 2017.
Grigori S Tseitin. On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic, 21115-125):10-13 1968.
Mingzhe Wang, Yihe Tang, J. J. Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In NIPS, 2017.
Ronald J Williams. Simple statistical gradient-following algorithms for connectionist reinforcement learning. Machine learning, 8(3-4):229-25 256, 1992.
Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Brown. Satzilla: portfolio- based algorithm selection for sat. Journal of artificial intelligence research, 32:565-606, 2008.
12

---

Published as a conference paper at ICLR 2020
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, arXiv preprint 1.Xiv:190S.093... 2019.
Zhanfu Yang, Fei Wang, Ziliang Chen, Guannan Wei, and Tiark Rompf. Graph neural reasoning for 2-quantified boolean formula solvers. arXiv preprint arXiv:7904. 12084, 2019.
Emre Yolcu and Barnabás Póczos. Learning local search heuristics for boolean satisfiability. 2019.
13

---

Published as a conference paper at ICLR 2020
A GLOBAL SOLVER STATE
1. Current decision level
2. Number of restarts
3. Restarts since last major restart
4. Conflicts until next restart
5. Ratio of variables that already have Skolem function total variables, Formula is solved when this reaches 1.
B LITERAL LABELS
Here we describe the details of the variable labels presented to the neural network described in Section The vector v consists of the following 7 values:
Do E (0. 1}
indicates whether the variable is universally quantified, indicates whether the variable is existentially quantified, indicates whether the variable has a Skolem function already, indicates whether the variable was assigned constant True, indicates whether the variable was assigned constant False, indicates whether the variable was decided positive, indicates whether the variable was decided negative, and
81 E {0,1}
U2 E {0,1)
va a (0
84 E (0
Us E [0,1]
ys E [0,1]
C THE QDIMACS FILE FORMAT
QDIMACS the standard representation of quantified Boolean formulas in prenex CNE. consists of header "p enf <num_val foum_varia iharial avariable ables>> <n.um_cd catm___lauess" describing the number of variables and the number of clauses in the formula. The lines following the header indicate the quantifiers. Lines starting with 'a' introduce universally quantified variables and lines starting with 'e" introduce existentially quantified variables. All lines except the header are terminated with 0; hence there cannot be variable named O. Every line after the quantifiers deseribes single clause (i.e. disjunction over variables and negated variables). Variables are indicated simply by an index; negated variables indicated by negative index. Below give the QDIMACS representation of the formula Vr. Ry. (x V y) A (-x V y):
enf 2 2
0
2 0
2 0
-1 2 0
There is no way to assign variables strings as names. The reasoning behind this decision is that this format is only meant to be used for the computational backend.
D HYPERPARAMETERS AND TRAINING DETAILS
We trained model on the reduction problems training set for 10M steps AWS server of type C5. We trained with the following hyperparameters, yet we note that training does not seem overly sensitive:
Literal embedding dimension: òz. 16
14

---

Published as a conference paper at ICLR 2020
10a
decision limit
10a
10
Random
VSIDS
Words
100
100
200
300
400
500
600
700
800
900
1,000
solved formulas
Figure 4: A cactus plot describing how many formulas from the test set were solved within growing decision limits on the Words test set. Lower and further to the right is better.
Clause embedding dimension: dc
Learning rate: 0.0006 for the first 2m steps, then 0.0001
Discount factor: 7 0.99
Gradient clipping:
Number of iterations (size of graph convolution): 1
Minimal number of timesteps per batch: 1200
E ADDITIONAL DATASETS AND EXPERIMENTS
While the set of Reductions- formuulss we considered the main part of the paper was created independently from this paper and is therefore unlikely to be biased towards our approach, one may ask it is just a coincidence that our approach was able to learn a good heuristic for that particular set of formulas. In this appendix and Words, and replicated the results from the main part. We show that we can learn a heuristic for a given set/distribution of formulas that outperforms VSIDS by significant margin.
consider two additional sets of formulas that we call Boolean
Boolean is set of formulas of random circuits. Starting from fixed number (8) of Boolean inputs the circuit, individual AND-gates added (with randomly chosen inputs with random polarity) up to a certain randomized limit. This circuit is turned into a propositional Boolean formula using the Tseitin transformation, and then a small fraction of random clauses is added add some irregularities to the circuit. (Up to this point, the process is performed by the fuzz-tester for SAT solvers, FuzzSAT, available here http: fmv. jku. fuzzsat/ To turn this kind propositional formulas into QBFs, we randomly selected 4 variables to be universally quantified. This resulted in a more or less even split of true and false formulas. The formulas have 50.7 variables on average. In Figure we see that training model on these formulas (we call this model Boolean, like the data set) results significantly better performance than VSIDS. The advantage of the learned heuristic over VSIDS and Random is smaller compared to the experiments Reductions in the main part of the paper. We conjecture that this due to the fact that these formulas are much easier to begin with, which means that there is not much potential for improvement.
Words data set of random expressions over (signed) bitvectors. The top-level operator is a comparison (=, 2, >), and the two subexpressions of the comparison arithmetic expressions. The number of operators and leafs in each expression 9, and all bitvectors have word size 8. The expressions contain up to four bitvector variables, alternatingly assigned to be existentially and
15

---

Published as a conference paper at ICLR 2020
10a
decision limit
10a
10
Random
VSIDS
Boolean
100
100
200
300
400
500
600
700
800
900
1,000
solved formulas
Figure 5: A cactus plot describing how many formulas from the test set were solved within growing decision limits on the Boolean test set. Lower and further to the right is better.
universally quantified. The formulas are simplified using the circuit synthesis tool ABC, and then they turned into CNF using the standard Tseitin transformation. The resulting formulas have 71.4 variables on average and are significantly harder for both Random and VSIDS. For example, the first formula from the data set looks follows: V2..2x(((x 2) 2) * + 1, which results in QBF with 115 variables and 298 clauses. This statement happens to be true and is solved with just 9 decisions using the VSIDS heuristic. In Figure 4 see that training new model on the Words dataset again results in significantly improved performance. (We named the model Words, after the data set.)
We did not include the formula sets Boolean and Words in the main part, as they are generated by random process in contrast to Reductions, which is generated with concrete application in mind. In the formal methods community, artificially generated sets of formulas are known to differ from application formulas in non-obvious ways.
F ADDITIONAL. EXPERIMENTS ON GENERALIZATION TO LARGER FORMULAS
An interesting observation that made is that models trained of small formulas generalize well to larger formulas from similar distributions. To demonstrate this, we generated set of larger formulas, similar the Words dataset. We call the new dataset Words30, and the only difference to Words is that the expressions have size 30. The resulting formulas have 186.6 variables on average. This time, instead of training a new model, we test the model trained on Words (from Figure on this new dataset.
In Figure we see that the overall hardness (measured the number of decisions needed solve the formulas) has increased lot, but the relative performance of the heuristics is still very similar. This shows that the heuristic learned on small formulas generalizes relatively well to much larger/harder formulas.
In Fig. we have already observed that the heuristic also generalizes well to much longer episodes than those it was trained on. We believe that this is due to the "locality" of the decisions we force the network to take: The graph neural network approach uses just one iteration, such that we force the heuristics take very local decisions. Not being able optimize globally, the heuristics have to learn local features that are helpful to solve problem sooner rather than later. It seems plausible that this behavior generalizes well to larger formulas (Fig. 6 much longer episodes (Fig. 3
16

---

Published as a conference paper at ICLR 2020
10a
decision limit
10a
10
Random
VSIDS
Words
109
50
100
150
200
250
300
350
400
450
500
550
600
solved formulas
Figure 6: A cactus plot describing how many formulas were solved within growing decision limits on the Words330 test set. Lower and further to the right is better. Note that unlike in the other plots, the model Words was not trained on this distribution of formulas, but on the same Words dataset as before.
G ENCODER VARIANTS AND HYPERPARAMETERS
The encoder described Subsection 4.1 by no means the only reasonable choice. In fact, the graph representation described in Fig. is not unique. One could just as well represent the formula bipartite graph on variables and clauses, with two types of edges, one for each polarity. The encoder then produces encodings of variables rather than literals, and the propagation along edges is performed with different learned parameter matrices, one for each edge type. The equations for such an encoder are:
Q ReLU
Σ WvlvT W BB
1Ec
# ReLU Σ Wolc .. Be
C,.ECc
Where Wy is one of W W (and similarly, We ( W.)). depending the polarity of the occurence of u in c, with v as the variable's label. Accordingly. we change the policy network to produce two scores per variable embedding vr, as the qualities of assigning this variable positive or negative polarity. In our experiments, this variant of the encoder achieved comparable results to those of the literal-based encoder.
The hyperparameter t controls the number of iterations within the GNN. Here too, there are several variants of the encoder one could consider. The architecture described in Subsection [4.] which achieved the reported results, applies the same transformation for every iteration (the matrices Wc- Wt). We've also experimented with a variant that uses different learned transformations, one per iteration, denoted Wt. WT, for 1 < f S (intuitively, this allows the network to perform different computation in every iteration). It achieved comparable results, yet with roughly times the number of parameters. A version with even more parameters gave the t'th transformation access not only to the connections. This version also didn't 't achieve significantly better results. To get results with more than one iteration we had to add a normalization layer between every two iterations. We experimented with both Layer Normalization (Ba et al. 2016) and GRU cell (Chung al. 2014), which gave
embedding, but to all the 1,..., t 1 previous embeddings, through residual
17

---

Published as a conference paper at ICLR 2020
103
decision limit
10a
Random
VSIDS
10a
Zero iterations
Learned
With Activities
10
10
20
30
40
50
60
70
80
90
100
solved formulas
Figure 7: A cactus plot describing how many formulas were solved within growing decision limits on the reduction test with different models. VSIDS, Random, and Learned are same left side of Figure 3
similar results. Adding 2nd and 3rd iteration achieved only slightly better results when measuring number of decisions to solve a formula, at the cost of more parameters, slower training, and more importantly, slower inference runtime. When measuring number of formulas solved in real time, a single iteration achieved best results overall. However, given the large overhead of our agent implementation, is possible that an optimized in-process implementation could still benefit from multiple iterations in the GNN.
is interesting to point that when we tested model with zero iterations, that is, GNN all, where the policy network gets to see only the variable labels from the solver, it achieved results that were better than Random and clearly demonstrated learning, but worse than VSIDS. and considerably less than the results for iteration. That shows that at least the 1-hop neighborhood of variable contains information which is crucial, we cannot achieve comparable results without considering this local topology of the graph.
Another interesting observation is that the model which achieved best results did not have access to the variable VSIDS activity scores! Adding activity scores to the variable feature vectors in fact slightly degraded performence. learns faster, but converges to a lower average reward, and performs slighly worse the validation and test sets, especially on the harder problems. We hypothesize that this because the model learns to rely on the activity scores, and they will quite different in harder (longer) episodes, and outside the range it trained on. Furthermore, shows that is possible to achieve a heuristic which performs better than VSIDS without even computing activities!
The results for the different variants be seen in Figure
18


Reviews:
[{"review_id": "SJeDZyV5tr", "reviewer": "AnonReviewer3", "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": "This paper investigates the problem of predicting the truth of quantified boolean formulae using deep reinforcement learning. In this setting, the problem is formulated as a reinforcement learning task, in which the learner is interacting with a solver (CADET), and its goal is to find a sequence of actions (each associated with a choice of a variable and a value) in order to reach a terminal state as fast as possible. The neural architecture includes a GNN encoder for the input formula, a policy neural net for iteratively assessing the quality of literals, and a final softmax layer for choosing the final literal. Experiments, performed on various 2QBF instances, address several questions such as the ability to compete with existing heuristics (VSIDS) in CADET and to generalize predictions on long episodes or different formulae.\n\nOverall, the paper is well-motivated. The introduction is well-written and explains the interest of learning new heuristics for QBF problems. The learning framework is relatively simple and elegant. Unfortunately, the paper suffers from many clarity issues in the problem formulation, the neural-net architecture, and the experiments. So, it is quite difficult to accept the paper in its current state. \n\nSection 2: In this section, some background knowledge about boolean problems and solvers are provided. Although the second paragraph about CNF formulae and CDCL solvers is well-written, the third paragraph about QBF should be clarified. For QBF formulae, the authors write “The algorithmic problem considered for QBF is to determine the truth of a quantified formula (TQBF)”. Well, this is not an algorithmic problem, but a decision problem. Furthermore, what is TQBF? I guess that the authors are talking about 2-QBF, for which the prenex is of the form $\\forall \\exists$. Here, the decision task should be explained in more detail using, for example, a game tree for explaining the distinct roles of “for all” variables and “there is” variables. As the decision problem for 2-QBF is more complex than the satisfiability problem for CNF, this point should be emphasized (i.e. the decision problem for 2-QBF is $\\Pi_2^P$ complete). \n\nSection 3: The problem of predicting the truth of 2-QBF is formulated as an MDP, where the environment is essentially controlling the input instances (of 2-QBF) and the states of the solver, and the learner’s actions are variable-value selections. First of all, I am not entirely convinced that an MDP is the right choice for specifying this problem. Basically, 2-QBF is a two-player game (“for all” vs “there is”), and the goal of the solver is to play “there is” by finding a satisfying assignment for each possible play (i.e. variable assignment) of the “for all” player. So, a natural framework here would be a stochastic game (SG) which generalizes the MDP framework. Actually, in the present MDP framework there are no distinctions between “for all” variables and “there is” variables. It seems that the learner can choose “for all” variables (which is wrong). Furthermore, the MDP is ill-defined. It is said that a policy is a mapping $\\pi: S \\times A$. This is ill-defined: what is the range of $\\pi$? Usually, a (mixed) policy is a mapping $\\pi$ from $S$ into the $|A|$-dimensional simplex. The reward function is also ambiguous: it is using a discount factor $\\gamma$ but, unless I missed something, this factor is not clarified in the rest of the paper. Finally, what is an “episode”? In the paper it is said “An episode is the result of the interaction of the agent with the environment”. Well, this is quite unclear. Usually, in an episodic-MDP the state space is partitioned into layers, i.e. $X = \\bigcup_{i = 0}^L X_i$, where $X_0$ is a singleton set (the initial state), and $X_L$ specifies the terminal states. Transitions are possible only between consecutive layers.  According to this usual framework, an episode is a sequence of actions made by the agent, starting from $X_0$ and moving forward across the consecutive layers until it reaches a state in $X_L$. For the 2-QBF decision problem, each terminal state in $X_L$ would naturally consists in the affectation of each variable in the prenex to a Boolean value. But this is not clear in the paper, because the authors are saying that “We consider an episode to be complete, if the solver reaches a terminal state in the last step”. This would mean that the number of actions per episodes is capped, and hence, the agent can reach a terminal, yet non-final, decision state.\n\nSection 4: The overall architecture (GNN encoder + Policy Network) is relatively standard, but the choice of the constants for dimension parameters $\\lambda_V$, $\\delta_L$ and $\\delta_C$ is a bit disconcerting. Notably, $\\lambda_V$ is used to capture the features of variables. Specifically, it is written that “$\\lambda_V = 7$ indicates whether the variable is universally or existentially quantified, whether it currently has a value assigned and whether it was selected as a decision variable already on the current search branch.” But what is the difference between the second feature and the third one? If a variable has already been branched, then it has been assigned, and conversely. Furthermore, if you have 3 boolean features $\\lambda_V$ should be fixed to 3. So, why choosing 7? For $\\delta_L$ and $\\delta_C$, it seems that their values correspond to the “best model”. But how this model is chosen? Did the author perform some grid search to find those values?  Finally, some comments about the last layer of the architecture (softmax function) would be welcome. In the end, we get a probability distribution over literals (agent’s available actions) “after masking illegal actions” (as written by the authors). But what is an illegal action? Is it a literal defined on a universally quantified variable? A literal defined on an already assigned existential variable? \n\nSection 5: In the experiments, the authors are examining four different questions, which are all interesting. But the experimental setup and the reported results are quite unclear. In fact, the experimental setup looks wrong, because if the “Reductions” dataset is taken from Jordan & Kaiser (SAT’13), it consists of formulae for which the prenex is of the form $\\exists \\forall$”. Unless I am wrong, this is the inverse of the 2QBF problem examined in the present paper  - Jordan and Kaiser were examining a $\\Sigma_2^P$-complete problem, while you are examining a $\\Pi_2^P$-complete problem. So, did you reverse the quantifiers for making experiments? This should be clarified in the paper. Furthermore, for this dataset which originally consists of 4500 instances, the authors say that “We filtered out 2500 formulas that are solved without any heuristic decisions.” What does this mean? Are all those 2500 formulas containing only universal quantifiers? In the remaining 2000 instances, what is the ratio between universally quantified variables and existentially quantified ones? By the way, how can we get 1835 training instances? 4500 - 2500 - 200 = 1800. \n\nIn the experimental results, which formulae have been used to compute the cactus plots? Training instances (1800)? Test instances (200)? Both of them? For training instances, the protocol reported in Section 5.2 is relatively clear. But for test instances, what is the protocol? Is CADET using the best policy trained on the 1800 instances for solving the remaining 200 instances? Furthermore, the notion of “decision limit” is quite confusing. According to Section 5.2, it seems that the decision limit is the horizon of each episode, i.e. the number of calls to the solver CADET using the latest policy estimated by the NN architecture. But this should be clarified unambiguously. \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 thoroughly."}, "extra_text": {}}, {"review_id": "Hye1Ff45YH", "reviewer": "AnonReviewer2", "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 proposed a GNN to improve an existing search based solver for 2-QBF solvers. The neural network is being used to predict the next steps in the search procedure, in this case, assignment to literals of the 2-QBF formula. Justifiably, a reinforcement learning formulation is used. I thought that the paper was very impressive. All necessary concepts were clearly introduced, the claims were very clear and thoroughly validated. Limitations of the current approach are also properly discussed. \n\nOnly comment I have is that using shallow networks with one iteration sounds not enough for a problem like 2-QBF solving. I noticed that you have this exploration in the appendix, would recommend moving it to the main paper. I would also have liked 2-QBF to be mentioned more explicitly in the abstract and early introduction.\n\nMinor errors:\n\"and\" --> \"an\" in Sec 1\n\"variale\" --> \"variable\" in Sec 4.2\nReference ? in Sec 6 ", "extra_scores": {"experience_assessment": "I do not know much about 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 carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly."}, "extra_text": {}}, {"review_id": "Bkg4fpnatr", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "\nThis will be an uncharacteristically short review. The work poses an interesting idea: why not mix heuristics and learning. It reads as if the paper was written a while ago and the intro was not updated, since there is a lot of related work using the same concept. Please cite existing work in the introduction, it reflects negatively on the paper.\n\nThe elephant in the room is that I have read this paper before. The work has a number of citations and has sparked a good amount of follow-up work. I like the ideas and they have received enough scrutiny already. It was not the best decision for ICLR 2019 to have rejected this paper, honestly. I will argue to accept the paper if the references are updated, it deserves a wider audience.\n\nThat said, I don't like this GNN embedding of the QBF. The negation should have been defined as an edge attribute, not through nodes (as in (Yolcu and Póczos, 2019)). The representation also does not encode the quantifiers well but I feel this is a question for future work.\n\nMinor comments:\n- Please update your paper. It needs a good refresh with the recent literature that cites your work.\n\n- \"An intriguing question for artificial intelligence is: can (deep) learning be effectively used for symbolic reasoning?\" => Can representation learning be effectively used for symbolic reasoning? This is one of the most intriguing question in artificial intelligence today.\n\n", "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: This paper proposes a new method to learning heuristics for quantified boolean formulas through RL. The focus is on a method called backtracking search algorithm. The paper proposes a new representation of formulas to scale the predictions of this method.

The reviewers have an overall positive response to this paper. R1 and R2 both agree that the paper should be accepted, and have given some minor feedback to improve the paper. R3 initially was critical of the paper, but the rebuttal helped to clarify their doubt. They still have one more comment and I encourage the authors to address this in the final version of the paper.

R3 meant to increase their score but somehow this is not reflected in the current score. Based on their comments though, I am assuming the scores to be 6,8,6 which makes the cut for ICLR. Therefore, I recommend to accept this paper.
Decision: Accept (Poster)