Learning Better Representations From Less Data For Propositional Satisfiability

Authors: mohamed  ghanem
frederik  schmitt
julian  siber
bernd  finkbeiner
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-14 18:56:13

Abstract: Training neural networks on NP-complete problems typically demands very large amounts of training data and often needs to be coupled with computationally expensive symbolic verifiers to ensure output correctness. In this paper, we present NeuRes, a neuro-symbolic approach to address both challenges for propositional satisfiability, being the quintessential NP-complete problem. By combining certificate-driven training and expert iteration, our model learns better representations than models trained for classification only, with a much higher data efficiency -- requiring orders of magnitude less training data. NeuRes employs propositional resolution as a proof system to generate proofs of unsatisfiability and to accelerate the process of finding satisfying truth assignments, exploring both possibilities in parallel. To realize this, we propose an attention-based architecture that autoregressively selects pairs of clauses from a dynamic formula embedding to derive new clauses. Furthermore, we employ expert iteration whereby model-generated proofs progressively replace longer teacher proofs as the new ground truth. This enables our model to reduce a dataset of proofs generated by an advanced solver by $\sim$$32$% after training on it with no extra guidance. This shows that NeuRes is not limited by the optimality of the teacher algorithm owing to its self-improving workflow. We show that our model achieves far better performance than NeuroSAT in terms of both correctly classified and proven instances.

Main paper: 
 introduction: 
 Boolean satisfiability (SAT) is a fundamental problem in computer science. For theory, this stems from SAT being the first problem proven NP-complete [13] . For practice, this is due to many highlyoptimized SAT solvers being used as flexible reasoning engines in a variety of tasks such as model checking [12, 47] , software verification [17] , planning [27] , and mathematical proof search [24] . Recently, SAT has also served as a litmus test for assessing the symbolic reasoning capabilities of neural models and a promising domain for neuro-symbolic systems [43, 42, 1, 10, 36] . So far, neural models only provide limited, if any, justification for unsatisfiability predictions. NeuroCore [42] , for example, predicts an unsatisfiable core, the verification of which can be as hard as solving the original problem. No certificates at all or certificates that are hard to check limit neural methods in a domain where correctness is critical and prevents close integrations with symbolic methods. Therefore, we propose a neuro-symbolic model that utilizes resolution to solve SAT problems by generating easy-to-check certificates.A resolution proof is a sequence of case distinctions, each involving two clauses, that ends in the empty clause (falsum). This technique can also be used to prove satisfiability by exhaustively applying it until no further new resolution steps are possible and the empty clause has not been derived. Generating such a proof is an interesting problem from a neuro-symbolic perspective because unlike other discrete combinatorial problems that have been considered before [46, 7, 28, 30, 11] , it requires selecting compatible pairs of clauses from the dynamically growing pool, as newly derived clauses are naturally considered for derivation in subsequent steps. In this work, we devise three attention-based mechanisms to perform this pair-selection needed for generating resolution proofs. In addition, we augment the architecture to efficiently handle sat (satisfiable) formulas with an assignment decoding mechanism that assigns a truth value to each literal. We hypothesize that, despite their final goals being in complete opposition, resolution and sat assignment finding can form a mutually beneficial collaboration. On the one hand, clauses derived by resolution incrementally inject additional information into the network, e.g., deriving a single-literal clause by resolution directly implies that literal should be true in any possible sat assignment. On the other hand, finding a sat assignment absolves the resolution network from having to prove satisfiability by exhaustion. On that basis, given an input formula, NeuRes proceeds in two parallel tracks: (1) finding a sat assignment, and (2) deriving a resolution proof of unsatisfiability. Both tracks operate on a shared representation of the problem state. Depending on which track succeeds, NeuRes produces the corresponding SAT verdict which is guaranteed to be sound by virtue of its certificate-based design. Since both of our certificate types are efficient to check, we can afford to perform these symbolic checks at each step. When comparing NeuRes with NeuroSAT [43] , which has been trained to predict satisfiability with millions of samples, we demonstrate that NeuRes achieves a higher accuracy while providing a proof and requires only thousands of training samples.As for most problems in theorem proving we are not only interest in finding any proof but a short proof. Resolution proofs can vary largely in their size depending on the resolution steps taken. Being able to efficiently check the proof, also allows us to adapt the proof target while training the model. In particular, we explore an expert iteration mechanism [2, 39] that pre-rolls the resolution proof of the model and replaces the target proof whenever the pre-rolled proof is shorter. We demonstrate that this bootstrapping mechanism iteratively shortens the proofs of our training dataset while further improving the overall performance of the model.We make the following contributions:1. We introduce novel architectures which combine graph neural networks with attention mechanisms for generating resolution proofs and assignments for CNF formulas (Section 4).2. We show that for propositional logic, learning to prove rather than predict satisfiability results in better representations and requires far less training samples (Section 6 and 7).3. We devise a bootstrapped training procedure where our model progressively produces shorter resolution proofs than its teacher (Section 6.2) boosting the model's overall performance.The implementation of our framework can be found at https://github.com/Oschart/NeuRes. 
related work: 
 SAT Solving and Certificates. We refer to the annual SAT competitions [5] for a comprehensive overview on the ever-evolving landscape of SAT solvers, benchmarks, and proof checkers. SAT solvers are complex systems with a documented history of bugs [9, 26] , hence proof certificates have been partially required in this competition since 2013 [3] . Unlike satisfiable formulas, there are several ways to certify unsatisfiable formulas [23] . Resolution proofs [52, 20] are easy to verify [15] , but non-trivial to generate from modern solvers based on the paradigm of conflict-driven clause learning [34] . Clausal proofs, e.g., in DRAT format [50] , are easier to generate and space-efficient, but hard to validate. Verifying the proofs can take longer than their discovery [22] and requires highly optimized algorithms [31] .Deep Learning for SAT Solving. NeuroSAT [43] was the first study of the Boolean satisfiability problem as an end-to-end learning task. Building upon the NeuroSAT architecture, a simplified version has been trained to predict unsatisfiable cores and successfully integrated as a branching heuristic in a state-of-the-art SAT solver [42] . Recent work has employed a related architecture as a phase selection heuristic [49] . It has been shown that both the NeuroSAT architecture and a newly introduced deep exchangeable architecture can outperform SAT solvers on instances of 3-SAT problems [10] . The NeuroSAT architecture has also been applied on special classes of crypto-analysis problems [44] . In addition to supervised learning, unsupervised methods have been proposed for solving SAT problems. For Circuit-SAT a deep-gated DAG recursive neural architecture has been presented together with a differentiable training objective to optimize towards solving the Circuit-SAT problem and finding a satisfying assignment [1] . For Boolean satisfiability, a differentiable training objective has been proposed together with a query mechanism that allows for recurrent solution trials [36] .Deep Learning for Formal Proof Generation. In formal mathematics, deep learning has been integrated with theorem proving for clause selection [33, 18] , premise selection [25, 48, 6, 35] , tactic prediction [51, 37] and whole proof searches [40, 19] . For SMT formulas specifically, deep reinforcement learning has been applied to tactic prediction [4] . In the domain of quantified boolean formulas, heuristics have been learned to guide search algorithms in proving the satisfiability and unsatisfiability of formulas [32] . For temporal logics, deep learning has been applied to prove the satisfiability of linear-time temporal logic formulas and the realizability of specifications [21, 41, 14] .Question: Does the paper discuss the limitations of the work performed by the authors?Answer: [Yes]Justification: We have highlighted the limitations with respect to industrial-grade SAT solving in the conclusion of the paper (Section 10).Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 
proofs of (un-)satisfiability: 
 We start with a brief review of certifying the (un-)satisfiability of propositional formulas in conjunctive normal form. For a set of Boolean variables V , we identify with each variable x ∈ V the positive literal x and the negative literal ¬x denoted by x. A clause corresponds to a disjunction of literals and is abbreviated by a set of literals, e.g., { 1, 3} represents (¬x 1 ∨ x 3 ). A formula in conjunctive normal form (CNF) is a conjunction of clauses and is abbreviated by a set of clauses, e.g., {{ 1, 3}, {1, 2, 4}} represents (¬x 1 ∨ x 3 ) ∧ (x 1 ∨ x 2 ∨ ¬x 4 ). Any Boolean formula can be converted to an equisatisfiable CNF formula in polynomial time, for example with Tseitin transformation [45] .A CNF formula is satisfiable if there exists an assignment A : V → {⊤, ⊥} such that all clauses are satisfied, i.e., each clause contains a positive literal x such that A(x) = ⊤ or a negative literal x such that A(x) = ⊥. If no such assignment exists we call the formula unsatisfiable. To prove unsatisfiability we rely on resolution, a fundamental inference rule in satisfiability testing [16] . The resolution rule (Res) picks clauses with two opposite literals and performs the following inference:C 1 ∪ {x} C 2 ∪ {x} Res C 1 ∪ C 2Resolution effectively performs a case distinction on the value of variable x: Either it is assigned to false, then C 1 has to evaluate to true, or it is assigned to true, then C 2 has to evaluate to true. Hence, we may infer the clause C 1 ∪ C 2 . A resolution proof for a CNF formula is a sequence of applications of the Res rule ending in the empty clause.Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?Answer: [Yes]Justification: Data and code are publicly available through the link provided in the paper.Guidelines:• The answer NA means that paper does not include experiments requiring code.• Please see the NeurIPS code and data submission guidelines (https://nips.cc/ public/guides/CodeSubmissionPolicy) for more details. • While we encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. • Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted. 
general architecture: 
 NeuRes is a neural network that takes a CNF formula as a set of clauses and outputs either a satisfying truth assignment or a resolution proof of unsatisfiability. As such, our model comprises a formula embedder connected to two downstream heads: (1) an attention network responsible for selecting clause pairs, and (2) a truth assignment decoder. See Figure 1 for an overview of the NeuRes architecture. After obtaining the initial clause and literal embeddings (representing the input formula), we continue with the iterative certificate generation phase. At each step, the model selects a clause pair which gets resolved into a new clause to append to the current formula graph while decoding a candidate truth assignment in parallel. The model keeps deriving new clauses until the empty clause is found (marking resolution proof completion), a satisfying assignment is found (marking a certified sat verdict), or the limit on episode length is reached (marking timeout).Similar to NeuroSAT, we use a message-passing GNN to obtain clause and literal embeddings by performing a predetermined number of rounds. Our formula graph is also constructed in a similar fashion to NeuroSAT graphs where clause nodes are connected to their constituent literal nodes and literals are connect to their complements (cf. Appendix A). For a formula in m variables and n clauses, the outputs of this GNN are two matrices: E L ∈ R m×d for literal embeddings and E C ∈ R n×d for clause embedding, where d ∈ N + is the embedding dimension. Here we have two key differences from NeuroSAT. Firstly, NeuroSAT uses these embeddings as voters to predict satisfiability through a classification MLP. In our case, we use these embeddings as clause tokens for clause pair selection and literal tokens for truth value assignment. Secondly, since our model derives new clauses with every resolution step, we need to embed these new clauses, as well as update existing embeddings to reflect their relation to the newly inferred clauses. Consequently, we need to introduce a new phase to the message-passing protocol, for which we explore two approaches: static embeddings and dynamic embeddings.In a static approach, we do not change the embeddings of initial clauses upon inferring a new clause. Instead, we exchange local messages between the node corresponding to the new clause and its literal nodes, in both directions. The main advantage of this approach is its low cost. A major drawback is that initial clauses never learn information about their relation to newly inferred clauses.In a dynamic approach, we do not only generate a new clause and its embedding, we also update the embeddings of all other clauses. This accounts for the fact that the utility of an existing clause may change with the introduction of a new clause. We perform one message-passing round on the mature graph for every newly derived clause, which produces the new clause embedding and updates other clause embeddings. Since message-passing rounds are parallel across clauses, a single update to the whole embedding matrix is reasonably efficient.After producing clause and literal embeddings, NeuRes enters the derivation stage. At each step, our model needs to select two clauses to resolve, produce the resultant clause, and add it to the current formula. To realize our clause-pair selection mechanism, we employ three attention-based designs. In this design, pairs are selected by making two consecutive attention queries on the clause pool. We condition the second attention query on the outcome (i.e., the clause) of the first query. Figure 2 shows this scheme where we perform the first query using the mean of the literal embeddings E L concatenated with a zero vector while performing the second query using the mean of the literal embeddings concatenated with the embedding vector E C c1 of the clause selected in the first query. Formally, Casc-Attn selects a clause index pair (c 1 , c 2 ) as follows:EQUATIONwhereW 1 ∈ R 2d×d , W 2 ∈ R d×d , u ∈ R d are trainable network parameters.The advantage of this design is that it is not limited to pair selection and can be used to select a tuple of arbitrary length. The main downside, however, is that this design chooses c 1 independently from c 2 , which is undesirable because the utility of a resolution step is determined by both clauses simultaneously (not sequentially).To address the downside of independent clause selection, this variant performs self-attention between all clauses to obtain a matrix S ∈ R n×n where S i,j represents the attention score of the clause pair (c i , c j ) as shown in Figure 3 . The model selects clause pairs by choosing the cell with the maximal score. In this attention scheme, the clause embeddings are used as both queries and keys. EQUATIONwhere W Q ∈ R d×d , W K ∈ R d×d are trainable network parameters. Since S contains many cells that correspond to invalid resolution steps (i.e., clause pairs that cannot be resolved), we mask out the invalid cells from the attention grid in ensure the network selection is valid at every step.In Full-Attn, the attention grid grows quadratically with the number of clauses. In this variant, we relax this cost by exploiting a property of binary resolution where each step targets a single variable in the two resolvent clauses. This allows us to narrow down candidate clause pairs by first selecting a variable as an anchor on which our clauses should be resolved. As such, we do not need to consider the full clause set at once, only the clauses containing the chosen variable v. We further compress the attention grid by lining clauses containing the literal v on rows while lining clauses containing the literal ¬v on columns. This reduces the redundancy of the attention grid since clauses containing the variable v with the same parity cannot be resolved on v, so there is no point in matching them.In this scheme, we have two attention modules: one attention network to choose an anchor variable followed by a self-attention network to produce the anchored score grid.In light of Figure 4 , this approach combines structural elements from Casc-Attn and Full-Attn; however, both elements are used differently in Anch-Attn. Firstly, the attention mechanism in Casc-Attn is used to select clauses whereas Anch-Attn uses it to select variables. Secondly, self-attention in Full-Attn matches any pair of clauses (c i , c j ) in both directions as the row and column dimensions in the attention score grid reflect the same clauses (all clauses). By contrast, Anch-Attn computes selfattention scores for clause pairs in only one order (positive instance to negative instance). Formally, EQUATIONwhereW 1 ∈ R d×d , W 2 ∈ R d×d , u ∈ R d are trainable network parameters. The clause index pair (c 1 , c 2 )is then selected according to the same equations of Full-Attn (Eq. 2) using the v-anchored set of clause embeddings.To extract satisfying assignments, we use a sigmoid-activated MLP ψ on top of the literal embeddings E L to assign a truth value Â(l i ) to a literal l i as shown in Eq. 4.EQUATIONNote that since for each variable, we have a positive and a negative literal embeddings, we can construct two different truth assignments at a time using this method. However, supervising both assignments did not improve the performance compared to only supervising the positive assignment (on positive literal embeddings). Thus, to simplify our loss function, we only derive truth assignments from the positive literal embeddings at train time while extracting both at test time. Interestingly, at test time, we found using negative literals (in addition to the positive ones) sometimes produces satisfying assignments before the positive branch despite receiving no direct supervision during training. Our intuition regarding this observation attributes it to the fact that the formula graph has no explicit notion of positive and negative literals, it only represents connections to clauses (positive and negative literals are connected by an undirected edge that does not distinguish their parity). As such, both literal nodes have a different local view into the rest of formula, which could result in one of them leading to a satisfying assignment faster than the other.5 Training and Hyperparameters 
dataset: 
 For our training and testing data, we adopt the same formula generation method as NeuroSAT [43] , namely SR(n) where n is the number of variables in the formula. This method was designed to generate a generalized formula distribution that is not limited to a particular domain of SAT problems.To control our data distributions, we vary the range on the number of Boolean variables involved in each formula. For our training data, we use formulas in SR(U (10, 40)) where U (10, 40) denotes the uniform distribution on integers between 10 and 40 (inclusive). To generate our teacher certificates comprising resolution proofs and truth assignments, we use the BooleForce solver [8] on the formulas generated on the SR distribution.We train our model in a supervised fashion using teacher-forcing on solver certificates. During unsat episodes, teacher actions (clause pairs) are imposed over the whole run. The length of the teacher proof dictates the length of the respective episode, denoted as T . Model parameters θ maximize the likelihood of teacher choices y t thereby minimizing the resolution loss L Res shown in Eq 5.EQUATIONDuring sat episodes, we minimize L sat computed as the binary cross-entropy loss between the sigmoid-activated outputs of assignment decoder Â : V → [0, 1] and the teacher assignment A : V → {0, 1} as shown in Eq. 6.EQUATIONIn both types of episodes, step-wise losses are weighted by a time-horizon discounting factor γ < 1.0 over the whole episode. The main rationale behind this is that later losses should have higher weights as the formula tends to get easier to solve with each new clause inferred by resolution.NeuRes has several hyperparameters that influence network size, depth, and loss weighting. In the experiments we fix the embedding dimension to 128. We train our models with a batch size of 1 and the Adam optimizer [29] for 50 epochs which took about six days on a single NVIDIA A100 GPU. We linearly anneal the learning rate from 5 × 10 -5 to zero over the training episodes. This empirically yields better results than using a constant learning rate. We use a time discounting factor γ = 0.99 for the episodic loss. We apply global-norm gradient clipping with a ratio of 0.5 [38] . 
generating resolution proofs: 
 NeuRes uses resolution as the core reasoning technique for certificate generation, both in the unsat and sat cases. Hence, we start with an in-depth comparative evaluation of several internal variants for resolution only. In particular, we evaluate the success rate (i.e., problems solved before timeout) and proof length relative to the teacher, denoted by p-Len = |PNeuRes| |Pteacher| . We use a limit of 4 on this ratio as a timeout to avoid simply brute-forcing a resolution proof. Note that we measure p-Len only for solved formulas to avoid diluting the average with resolution trails that timed out. For experiments in this section, we train on 8K unsat formulas in SR(U (10, 40) ) and test our models on 10K unseen formulas belonging to the same distribution. We use more formulas than the model was trained on to more reliably demonstrate its learning capacity. To assess the basic resolution performance of NeuRes, we evaluate each attention variant using both static and dynamic embeddings. For this experiment, we perform 32 rounds of message-passing for each input formula. As shown in Table 1 , dynamic embedding is decisively better for all three attention variants, thereby confirming its conceptual merit. While anchored attention leads over other variants under static embeddings, full attention performs significantly better for dynamic embeddings, albeit at the cost of longer proofs on average. We believe that Anch-Attn's better performance in the static setting can be explained through the full connectivity of its attention grid (proven in Appendix B). Since dynamic-embedding Full-Attn is the best-performing configuration over indistribution test settings, we will demonstrate the remaining evaluation experiments exclusively on this variant. During our initial experiments, we discovered proofs produced by NeuRes that were shorter than the corresponding teacher proofs in the training data. Although teacher proofs were generated by a traditional SAT solver, they are not guaranteed to be size-optimal. The size of resolution proofs is their only real drawback, hence any method that can reduce this size would be immensely useful.Upon closer inspection we find that, on average, our previous best performer trained with regular teacher-forcing manages to shorten ∼18% of teacher proofs by a notable factor (cf. Appendix C). This inspired us to devise a bootstrapped training procedure to capitalize on this feature: We pre-roll each input problem using model actions only, and whenever the model proof is shorter than the teacher's, it replaces the teacher's proof in the dataset. In other words, we maximize the likelihood of the shorter proof. In doing so iteratively, the model progressively becomes its own teacher by exploiting redundancies in the teacher algorithm.The outcome of this bootstrapped training process is summarized in Table 6 . We find that bootstrapping results in notable gains in terms of both success rate and optimality. The sharp decline in proof length (relatively quantified by p-Len) at test time shows that the models transfers the bootstrapped knowledge to unseen test formulas, as opposed to merely overfitting on training formulas. In addition to success rate and p-Len, we inspect the reduction statistics of our bootstrapped variant (first three rows of Table 6 ). Since the bootstrapped model performs multiple reduction scans over the training dataset, we add a metric for reduction depth computed as the number of progressive reductions made to a proof. To further quantify this effect, we report the maximum and average reduction ratios of reduced proofs relative to teacher proofs. Finally, we report the total reduction made to the dataset size in terms of total number of proof steps.In Appendix C, we have compiled additional statistics (cf. Table 5 ) on proof shortening during the training process, as well as an example proof reduced by the bootstrapped NeuRes (Figure 7 ). We only include a small reduction example (from 20 steps to 10 steps) for space constraints, but we observed many more examples of much larger reductions (e.g., over 400 steps).Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?Answer: [Yes] Justification: Training and test splits are specified at the beginning of Section 6 and Section 7.Optimization and hyperparameters are detailed in Section 5.2 and Section 5.3.Guidelines:• The answer NA means that the paper does not include experiments.• The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them. • The full details can be provided either with the code, in appendix, or as supplemental material. 
resolution-aided sat solving: 
 In this section, we evaluate the performance of our fully integrated model trained on a hybrid dataset comprising 8K unsatisfiable formulas (and their resolution proofs) and 8K satisfiable formulas (and their satisfying assignments). For the unsatisfiable formulas, timeout (4 × |P teacher |) and optimality (p-Len) are measured similarly to previous experiments. For satisfiable formulas, we set the timeout (maximum #trials) to 2 × |V |. Ultimately, this section aims to investigate the effect of incorporating a certificate-driven downstream head on the quality of the learnt representations through its impact on the performance of the complementary task, i.e., proving/predicting satisfiability. We use NeuroSAT as our baseline as it employs the same formula embedding architecture. Since NeuroSAT proves sat but only predicts unsat, we train a classification MLP on top of our trained NeuRes model to further showcase the benefit of our representations on prediction accuracy. trained on millions of formulas while NeuRes was trained on only 16K formulas. Lastly, we find that augmenting sat formulas by resolution derivations results in relative improvements (∼ 2.3%) in success rate even though these derivations are attempting to prove unsatisfiability.Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?Answer: [No] Justification: Due to the computational budget, errors bars are not reported.Guidelines:• The answer NA means that the paper does not include experiments.• The authors should answer "Yes" if the results are accompanied by error bars, confidence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper. • The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).• The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.) • The assumptions made should be given (e.g., Normally distributed errors). • It should be clear whether the error bar is the standard deviation or the standard error of the mean. • It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have a 96% CI, if the hypothesis of Normality of errors is not verified. • For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative error rates). • If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text. 
utilizing model fan-out: 
 In our Full-Attention module, we compute n 2 scores and only perform the top-score resolution step. This greedy approach arguably underutilizes the attention grid computations as it ignores other high-scoring steps that might lead to a shorter proof thereby improving the success rate in addition to reducing the number of queries to the model. The latter leads to an overall runtime reduction since performing an extra symbolic resolution step is much faster than a forward model pass. As such, we experiment with performing the top k steps of the attention grid after each forward pass. It should be noted, however, that this yields diminishing returns as it leads to a faster growth of the clause base which in turn inflates the attention grid. For k > 1, after deriving the empty clause, only clauses that connect to it in the resolution graph are kept in the final proof. This post-processing step is linear in the proof length and eliminates redundant resolution steps resulting from the higher fan-out. Table 4 shows that taking the top 3 steps already yields a massive reduction in proof lengths along with a significant boost to the success rate. One way to offset the attention grid inflation with higher fan-out would be to keep a saliency map for all clauses then discarding k clauses with the least saliency scores after each forward pass. One simple way to compute this saliency score for a clause would be the sum/mean/max of its respective row in the attention scores grid. Another proxy for saliency could be the recency score reflecting how many steps have elapsed since the last time a given clause was used.Question: For each experiment, does the paper provide sufficient information on the computer resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?Answer: [Yes] Justification: The compute resources are reported in Section 5.3.Guidelines:• The answer NA means that the paper does not include experiments.• The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage. • The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute. • The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make it into the paper). 
generalizing to larger problems: 
 In order to test our model's out-of-distribution performance, we evaluate our NeuRes model on five datasets comprising formulas with up to 5 times more variables than encountered during training. We use the same distributions reported by NeuroSAT and we run our model for the same maximum number of iterations (1000).Figure 5 shows the scalability of NeuRes to larger problems by letting it run for more iterations. Compared to NeuroSAT [43] , NeuRes scores a much higher first-try success rate on all 5 problem distributions, and a higher final success rate on all of them except for SR (40) on which both models nearly score 100%. Particularly, NeuRes shows higher first-try success on the 3 largest problem sizes where NeuroSAT solves zero or near-zero problems on the first try. Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? 
conclusion: 
 In this paper, we introduced a deep learning approach for proving and predicting propositional satisfiability. We proposed an architecture that combines graph neural networks with attention mechanisms to generate resolution proofs of unsatisfiability. Unlike methods that merely predict unsatisfiability, our models provide easily verifiable certificates for their verdicts. We demonstrated that our certificate-based training and resolution-aided mode of operation surpass previous approaches in terms of performance and data efficiency, which we attribute to learning better representations.Despite its promising benchmark performance, our model cannot solely outperform highly engineered industrial solvers, as is currently the case for all neural methods as standalone tools. The gap between neural networks and symbolic algorithms is still rather large, and our hope is to bring deep learning methods one concrete step closer to filling this gap. For NeuRes, this step is recognizing the immense value of carefully integrating certificates into the model design and training as opposed to using shallow supervision labels. Last but not least, it is worth noting that even at their present state, neural networks stand great potential to advance traditional solvers by combining them into hybrid solvers that utilize the deep long-range dependencies captured by neural networks along with the exploration speed of symbolic algorithms. Moreover, we demonstrated a unique potential to advance SAT solving through proof reduction, as proof size is a major challenge in certifying the results of traditional solvers. This proof reduction is facilitated by a bootstrapped training procedure that uses teacher proofs as a guide as opposed to a golden standard.Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [Yes]Justification: As discussed in the conclusion, a potential application of this work is to build hybrid SAT solvers. Such solvers are used in a variety of applications to improve the reliability of software and hardware, and hence this work may have positive societal impact in this area. Since the proposed models back their verdicts by easily verifiable certificates, there is little risk of harm since incorrect results can be detected easily, unlike in, e.g., mere satisfiability prediction.Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] .Justification: We do not recognize any risk of misuse of the datasets and models presented in this work.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [NA] Justification: No existing assets were used.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided. • If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. • If this information is not available online, the authors are encouraged to reach out to the asset's creators. 
new assets: 
 Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?Answer: [NA] Justification: We will make new assets publically available after the double-blind review ended.Guidelines:• The answer NA means that the paper does not release new assets.• Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc. • The paper should discuss whether and how consent was obtained from people whose asset is used. • At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file. 
crowdsourcing and research with human subjects: 
 Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?Answer: [NA]Justification: The paper does not involve crowdsourcing nor research with human subjects.Guidelines:• The answer NA means that the paper does not involve crowdsourcing nor research with human subjects. • Including this information in the supplemental material is fine, but if the main contribution of the paper involves human subjects, then as much detail as possible should be included in the main paper. • According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector. 
institutional review board (irb) approvals or equivalent for research with human subjects: 
 Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?Answer: [NA]Justification: The paper does not involve crowdsourcing nor research with human subjects.Guidelines:• The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.• Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper. • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 
 
 Appendix: One rather interesting observation on Table 5 is that the model appears to be marginally better at producing shorter proofs for unseen (test) formulas than for training formulas. While we would normally expect the opposite, a fair speculation would be that the trained model was teacher-forced to match teacher proofs during training over multiple epochs while the same does not hold for unseen formulas where the bias towards teacher behavior is significantly lower. Definitively confirming this would require a more in-depth investigation. In the following table, we compare the average runtimes of our top-1 Full-Attn, top-3 Full-Attn, and the traditional solver we used as a teacher (BooleForce) on our main SR(40) test dataset. For both Full-Attn models, we use our Python prototype implementation; for BooleForce, we use an official C implementation. In terms of the model architecture, both NeuRes and NeuroSAT models can be broken down to:• Embedding/Representation Network: for both models, this network is an LSTM-based GNN that embeds the formula graph by message-passing. We use the exact same architecture and model size to ensure that our improved representations are a result of our fully certificatebased learning objective as opposed to a tweak in the model architecture. This GNN has 429, 824 parameters in total. Justification: We included a contributions section in the introduction which refers to the corresponding sections in the paper.Guidelines:• The answer NA means that the abstract and introduction do not include the claims made in the paper. • The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper.Justification: No harms were caused by the research process nor are harmful consequences expected from the propositional logic problems considered in this work.Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction).38th Conference on Neural Information Processing Systems (NeurIPS 2024).We use the terms connected and disconnected here to refer to the fact of whether two nodes have exchanged messages (in either direction) or not, respectively. 


Decision: In the propositional satisfiability problem, we are given a formula in conjunctive normal form, and the aim is to either determine its satisfiability by providing a satisfying assignment of all variables, or to determine its unsatisfiability by proving that it logically implies the empty clause. In the context of neural approaches to satisfiability, this study focuses on solving both aspects of the problem by deriving correct assignments for satisfiable instances and correct resolution proofs for unsatisfiable ones. To achieve this, the proposed architecture combines a graph neural network with an attention module to simultaneously generate variable assignments and resolution proofs. The key innovation lies in the generation of resolution proofs: at each step, two clauses are selected from attention queries, the resolvant is added to the pool, and the clause embeddings are updated. The paper introduces several attention mechanisms of increasing efficiency. Comparative experiments with NeuroSAT on both satisfiable and unsatisfiable random instances with up to 40 variables are conducted to validate the framework.

Overall, reviewers agree that a key benefit of this learning approach is providing certificates for satisfiable/unsatisfiable instances instead of just predicting a Boolean value. The NeuRes architecture is well-explained, particularly in presenting the different attention mechanisms used for generating resolution proofs. The idea of coupling learning processes for generating assignments and resolution proofs is considered insightful, as these processes can work together to derive a certificate. Additionally, the fact that resolution proofs generated by NeuRes are often shorter than the teacher's proof can be helpful for interpretability.

However, the main weakness of this study may lie in the choice of the competitor in experiments. Some reviewers observed that comparing NeuRes with NeuroSAT is not entirely fair because the latter is unable to prove that an instance is unsatisfiable. A well-argued discussion about the choice of NeuroSAT and the analysis of results would clearly improve the quality of this study. Furthermore, reviewers had questions about ablation studies, comparative model sizes and runtimes, and the gap between NeuRes and highly engineered SAT solvers. Incorporating your detailed responses to these relevant questions in the paper (or appendix) might also improve its quality.

Reviews: review: paper_summary: paper_summary: This paper presents a deep-learning-based approach for generating resolution proofs for SAT formulas. The proposed method outperforms NeuroSAT on proving/predicting satisfiability on a family of benchmarks.
strength_weakness: strength_weakness: - At its core, the key technical contribution of the paper is that instead of learning an end-to-end SAT solver, the paper proposes to learn a resolution strategy that selects the clauses to resolve for a given formula. This is a fine idea and similar in spirit to many existing lines of work in ML applied to constraint solving, where the goal is to learn a particular heuristics (e.g., branching, restart) to replace some hand-crafted ones. However, to evaluate the proposed method, the paper should compare with existing resolution strategies (potentially including learning-based ones if they exist already) on statistics such as proof lengths and runtime. The comparison with NeuroSAT to me is quite apple-to-orange. 
 - Related to the point above, the paper is entitled "learning better representations from less data", instead of something along the line of "learning to perform resolution". The current title can be a little misleading because words like "better" and "less" do not make much sense when the underlying learning task changes (from satisfiability prediction to resolution clause selection).
- The paper only considers very simple SAT instances and it seems difficult to scale the presented approach to much larger real-world instances.
questions: questions: 1. Could you compare the learned resolution strategy with existing ones?
2. Have you conducted ablation studies of the effect of the model architecture to proof length/success rate?
limitations: limitations: The paper discusses the scalability/efficiency limitation of the proposed method. I do not see the potential negative societal impact of their work.
paper_summary: paper_summary: The authors proposed an attention-based architecture that autoregressively selects pairs of clauses for propositional resolution. The framework can generate proofs of unsatisfiability and accelerate the process of finding satisfying truth assignments simutaneously. Emprical evaluation shows that the resulting model achieves better performance than NeuroSAT in terms of both correctly classified and proven instances.
strength_weakness: strength_weakness: - Speed can potentially be an issue since every resolution step invokes a forward pass of the model, and for large problems, the calls can be quite numerous.
questions: questions: - How easy do you think the approach can be combined with traditional SAT optimization?
- Have you thought about extending the approach to anything beyond propositional SAT?
limitations: limitations: The authors discussed the limitation in section 9 and I agree with them.
paper_summary: paper_summary: The paper presents NeuRes, a system to solve SAT/UNSAT problems. In particular, it is able to provide UNSAT certificates via resolution proofs. The system constructs a resolution proof by iteratively selecting two clauses from all clauses, producing the resolvent from the two clauses, and adding it back to the clause formula. The selection of two clauses is done by a selector network. They experiment with different attention mechanisms in the selector network, including full attention, selecting an anchor variable and then doing full attention on the subset of clauses including the anchor variable, etc. When training, they use an off-the-shelf symbolic solver to generate resolution proofs and train to predict the clause selection with a teacher forcing style. The experiments show that NeuRes is able to generate resolution proofs for UNSAT problems (99.6% problems solved) for small problems with 40 variables, and also shows some generalizability to larger problems.
strength_weakness: strength_weakness: * Resolution-based UNSAT certification may not be as useful or practical as clausal proofs like the DRAT format, due to resolution-based proofs potentially being too large for large SAT instances.
questions: questions: * Could you explain how the method applies to SAT problems? If it's an UNSAT problem, then I can see that it terminates at deriving an empty clause, but how does it work for SAT problems?
* How does the model size of NeuRes compare to the baseline NeuroSAT on the SAT problems? How does the solving time compare between the two methods?
limitations: limitations: The limitation about the performance of neural methods on SAT solving still lags behind symbolic solvers is discussed.
paper_summary: paper_summary: The paper integrates attention-based neural networks into the SAT solving process based on resolution. The neural networks aim to predict pairs of disjunctive clauses to merge. The paper proposes several variants of neural networks for this task and conducted experiments to check their performance. Although the resolution is the algorithm to check unsatisfiability, the proposed framework simultaneously addresses the satisfiability task by decoding the embeddings of formulas.
strength_weakness: strength_weakness: - It is not clear how big the gap between the proposed approach and the highly-engineered SAT solvers is. It is not critical that the highly-engineered SAT solvers work better, but revealing the gap in the current state clarifies the current position of neural SAT solvers.
- Some aspects of the proposed approach and experiment design are unclear (see the below question).
questions: questions: * How big is the gap between the proposed approach and the highly-engineered SAT solvers?
* What is $\overline{E^L}$? How different is it from $E^L$?
* The advantage of Casc-Attn is claimed to be "it ... can be used to select a tuple of arbitrary length." Does this advantage is utilized in the implementation?
* The paper says that at train time only the positive literal embeddings are used to derive truth assignments, but at test time, the negative literal embeddings are used. Why is this okay although the derivation of truth assignments from the negative embeddings should not be learned?
* What is the ratio between sat and unsat problems in the synthesized dataset? 
* At the beginning of Section 6, the paper mentions the training and test datasets, but does not the validation dataset. I think it should be used because hyperparameters should be adjusted. What validation dataset is used?
* (Minor) What is Res-Aided model (mentioned at the beginning of Section 8)? I find this terminology only there.
limitations: limitations: I think the limitations are discussed appropriately.
paper_summary: paper_summary: The paper presents NeuRes, a neural symbolic system designed to solve the Boolean satisfiability problem of CNF (Conjunctive Normal Form). NeuRes utilizes a message-passing graph neural network to embed the information contained in CNF and attempts to predict clause pairs for propositional resolution and value assignments for satisfiability. NeuRes proposes three novel attention mechanisms to better select clause pairs for resolution and employs expert iteration to progressively optimize the generated proofs. The experimental results demonstrate the effectiveness of the proposed NeuRes system.
strength_weakness: strength_weakness: - The paper does not include a thorough ablation study to evaluate the effectiveness of each proposed component. i.e. It lacks an assessment of the true value assignment task’s effectiveness.
- As noted in the Limitation (Section 9), the efficiency of the neural method is concerning. It adds substantial computational overhead for clause selection using the neural network. However, overall, I believe this work represents a solid advancement in neuro-symbolic approaches for SAT solvers.
questions: questions: - Is there a comparison of the efficiency of the three different attention mechanisms as well as the baseline method (NeuroSAT)? It appears that full attention produces the most promising results, but it is also the least efficient.
limitations: limitations: Yes, the authors adequately addressed the limitations and posed no negative societal impact.

Comments: comment: I thank the authors for their patient responses and further clarifications. I agree that the discovery that {sample+certificate} contains a much richer learning signal than {sample+label} is significant, and towards this end, this paper provides sufficient empirical data. 

However, my concern with the presentation issue remains. *A significant portion of the experimental evaluation--more specifically, half of Section 7 (Proven %) and all of Section 8--is comparing the successful solving rates of the learning-aided DP algorithm and NeuroSAT.* I explained above why this does not make much sense. Perhaps this is partially why I was distracted from the key message the paper is conveying, which, again, I believe is a valuable one.

I increased my score to 4, as I still strongly believe this paper would benefit from a round of revision to address the presentation issues. However, I would not be opposed to this paper being accepted if the other reviewers believe that it is fine to include those not entirely fair comparisons in the paper.
Thanks for the response. 

After reading the discussion between the authors and reviewer MVHU, I am inclined to believe that the authors did not misrepresent their contribution. I agree with reviewer MVHU that directly comparing the SAT solving capability of NeuroSAT and NeuRes isn’t entirely fair because NeuRes is built on resolution, which is by itself complete. 

That said, the authors made it clear in the title that the primary focus is on learning a better representation. This is achieved by using the same embedding architecture but learning from a different objective than NeuroSAT. In this context, I believe the title fits the paper very well, and perhaps it is the resulting resolution prover with learned heuristics that should be considered a byproduct here.

Overall, the authors helped me understand their contribution better through the rebuttal. I would like to see this paper occur in this year’s NeurIPS, so I am raising my score to a strong accept.
Thank you for your detailed reply, which we address in the following:

> The paper seems to position itself as an improved solution over NeuroSAT, while the two methods are incomparable.

NeuRes and NeuroSAT do not differ fundamentally in their research direction. While NeuroSAT explores the efficacy of learning a SAT solver by learning satisfiability prediction, NeuRes explores this problem by learning certificate/proof generation. Both approaches are capable of SAT assignment decoding while only NeuRes can prove unsatisfiability.

Naturally, they are still comparable on their shared functionalities. In line with our 2nd contribution (lines 66-67), the comparison with NeuroSAT sheds light on the following:

1. Can certificate-based training improve the learnt representations over label-based training? We answer this question positively through our comparison of prediction accuracy of NeuroSAT. 
2. Is certificate-based training more data-efficient than label-based training in terms of the number of training samples needed? We answer this question positively through the fact NeuRes was trained on two orders of magnitude fewer samples than NeuroSAT. 

That is, **{sample+certificate}** contains a much richer learning signal than **{sample+label}**.

> Any resolution heuristic can generate a correct proof 100% of the time.

The resolution calculus is complete through exhaustive application. We mention this in the introduction (lines 33-36, and 46-47). However, applying resolution naively is practically infeasible since it can easily result in an exponential blow-up in the size of the formula. Indeed, in our evaluation, not a single proof-by-exhaustion case is counted as a successful sample. This is also reflected in the reported $\text{p-Len}$ (ratio between NeuRes and teacher proof lengths). For example, the bootstrapped Full-Attn model has an average $\text{p-Len}$ of 1.15; hence, the proofs are far from the timeout (= 4).

> I also suspect NeuRes takes much longer time than NeuroSAT in the proof generation task.

NeuroSAT does not generate UNSAT proofs. If you are referring to SAT assignment decoding, then NeuRes is much more time-efficient as it generates a full assignment via a single MLP pass on literal embeddings while NeuroSAT performs an iterative k-means clustering on them (which is significantly costlier and could take hundreds of iterations to converge).

> Overall, I don't see the left half of Table 3 adds value to the paper.

The left half of that table shows that NeuRes notably outperforms NeuroSAT at finding SAT assignments.

> While it is true that NeuroSAT learns to predict satisfiability \[...\] I'm not sure whether it should be used as a strong baseline for the pure task of satisfiabiltiy prediction.

We find this argument quite surprising given the fact that NeuroSAT is trained purely as a SAT predictor. The assignment extraction is presented as a desirable byproduct of that learning objective. We used exactly the same prediction method as NeuroSAT to show that the improvement in prediction accuracy is not owed to any variation in the network architecture and can be mainly attributed to a higher quality/informativeness of representations. The prediction comparison serves as a proxy for representation quality.

> It's not surprising that a more expensive resolution heuristic can reduce the proof length.

The point of this experiment (Section 6.2) is that proof reductions done by bootstrapped NeuRes were learned without any extra supervision, which is fair evidence that NeuRes learns deeper insights into the problem as opposed to simply mimicking the teacher algorithm.

> To me, this paper is very similar in spirit to NeuroCore.

The NeuroCore paper is about augmenting a state-of-the-art CDCL-based SAT solver with NeuroSAT as a variable selection heuristic (where the *key question* raised by the reviewer would indeed be essential). This is a fundamentally different objective from our paper, which is about improving learned representations by training on proof certificates. Our better representations (from less data) can positively impact approaches like NeuroCore. As mentioned in our initial response to reviewer R9jd, using our representations in a hybrid solver is interesting future work.

> Follow up question: what is the total training time of NeuRes and NeuroSAT, respectively?

NeuRes takes roughly six days to fully train from scratch on a single NVIDIA A100 GPU (which could be notably sped up by using multiple GPUs). NeuroSAT does not report their total training time, so we do not have this information. 


We hope our arguments above have convinced the reviewer that the comparisons in our experimental evaluation are carefully chosen. This does require stepping away from looking at our approach through the lens of a resolution heuristic, and instead also valuing the impact of improved representations and data-efficiency on the overall progress of neural methods in this domain.
We would like to thank the reviewer again and are happy that all their concerns have been addressed.

In the meantime, we performed a time profiling for our top-3 model to confirm that it shortens the runtime as well as the proof/episode lengths. In the following table, we compare the average runtimes of our top-1 Full-Attn, top-3 Full-Attn, and the traditional solver we used as a teacher (BooleForce) on our main SR(40) test dataset. For both Full-Attn models, we use our Python prototype implementation; for BooleForce, we use an official C implementation.

| Solver          | SAT (ms) | UNSAT (ms) | Combined (ms) |
|-----------------|----------|------------|---------------|
| Top-1 Full-Attn | 2.3      | 88         | 45.15         |
| Top-3 Full-Attn | 3        | 54.4       | 28.7          |
| BooleForce      | 4        | 5          | 4.5           |
I thank the authors for their answers, which help me understand their perspective a little better. I would also like to re-emphasize that I like the general methodology this paper is taking. However, I still think that the paper has some serious presentation issues. 

To me, NeuRes is better categorized as an ML-based resolution heuristics to be installed in a well-established SAT-solving algorithm, i.e., the resolution-based *Davis-Putnam (DP) algorithm*.  This is fundamentally different from NeuroSAT, which is tackling a different research question: to what extend can we learn a SAT-solving procedure completely from scratch? For this reason, it is quite odd that a large portion of the experimental evaluation is focused on comparison against NeuroSAT and the paper seems to position itself as an improved solution over NeuroSAT, while the two methods are **incomparable**.

Consider the comparison on **Proven %** in Table 3. The configuration NeuRes is essentially running a DP-like algorithm (i.e., iteratively performing resolution) while repeatedly using a neural network as the heuristic to decide which variable and clauses to choose. This algorithm is guaranteed to generate a proof, *regardless of the heuristic*. On the other hand, the configuration NeuroSAT performs one inference of the neural network to generate a proof (of satisfiability). The fact that NeuRes generates a correct proof more frequently than NeuroSAT is not surprising and does not say much about NeuRes's effectiveness, because given a sufficient number of resolution steps, *any* resolution heuristic can generate a correct proof 100% of the time. The paper does try to make the comparison "fairer" by putting a upper bound on the number of resolution steps that the configuration NeuRes can perform in Table 3. However, this upper bound is **very loose** (e.g., 4 times the number of resolution steps the original solver takes for UNSAT instances). I also suspect NeuRes takes much longer time than NeuroSAT in the proof generation task.  Overall, I don't see the left half of Table 3 adds value to the paper. 

Now if we move on to the second half of Table 3 (**Predicted %**). While it is true that NeuroSAT learns to predict satisfiability. This is not its ultimate goal. Therefore, I'm not sure whether it should be used as a strong baseline for the pure task of satisfiabiltiy prediction. To show that NeuRes performs better at satisfiability prediction task than previous method, one should probably consider comparing against methods dedicated for satisfiability prediction (e.g., [1]), on a wider/harder set of benchmarks.

Finally, if we judge the effectiveness of NeuRes from the perspective of a resolution heuristics (which I think we should), I am concerned that the experimental result is not convincing enough. First, the paper only showed resolution step reduction on one simple benchmark set (SR-40); Second, it's not surprising that a more expensive resolution heuristic can reduce the proof length. The key question is whether the increase in time spent on making a heuristic choice is out-weighted by the reduction in the proof length. The paper does not provide a good answer to this question. To me, this paper is very similar in spirit to NeuroCore [2], which tries to reduce the overhead with by only calling the NN heuristic periodically. Perhaps something similar could be explored.

Overall, I find the paper could have done a better job positioning itself in the broader literature of ML + SAT-solving and perform experimental evaluation that more directly validates the effectiveness of the proposed method.

[1] https://ojs.aaai.org/index.php/AAAI/article/view/5733

[2] https://arxiv.org/abs/1903.04671

**Follow up question**: what is the total training time of NeuRes and NeuroSAT, respectively?
Thank you for the rebuttal. 

I am happy to see that all my concerns are addressed. One more thing, can you please tell me how much time (in seconds) it took on average on the problems you tested? A rough estimate would be fine, and I won’t hold it against you even if it’s slower compared to traditional methods.
Thank you again for your valuable feedback. We shall include clarifications on the highlights you mentioned mainly in form of a passage on the gap between neural and traditional solvers along with the full ablation experiment of literal assignment supervision.
Thank you for the response. I just hope my concerns are clarified also in the revision if possible.