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 in 2QBF we learn a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.
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.
Overall, 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. 
Section 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). 
Section 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.
Section 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? 
Section 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. 
In 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.