Learning Better Representations From Less Data For Propositional Satisfiability
Authors: Mohamed Ghanem
Frederik Schmitt
Julian Siber
Bernd Finkbeiner
Venue: NeurIPS 2024 spotlight (2024)
Keywords: Neuro-symbolic
Propositional Logic
Resolution
Attention
Deep Learning
Graph Neural Networks
Expert Iteration
Primary area: machine_learning_for_other_sciences_and_fields
TL;DR: We present a neuro-symbolic approach for learning proofs of propositional satisfiability with largely enhanced data efficiency and a self-improving workflow.

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.

Learning Better Representations From Less Data For Propositional Satisfiability
Mohamed Ghanem" *
Frederik Schmitt"
Julian Siber* Bernd Finkheiner"
*CISPA Helmholtz Center for Information Security
(mohamed, ghanem, frederik. schmitt, j siber, finkbeinerr@cissp..c
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, neuro- symublcc approach to address both challenges for proposi- tional satisfiabilityy being the quintessential NP-complete problem. By combining certificate-driven training and expert iteration, model learns better representa- tions than models trained for classification only, with 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-base sively selects pairs of clauses from a dynamic formula embedding derive new clauses. Furthermore, we employ expert iteration whereby model-generae 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 ~32% after training on 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 terms of both correctly classified and proven instances.
architecture that autoregres-
Introduction
Boolean satisfiability (SAT) is fundamental problem in computer science. For theory. this stems from SAT being the first problem proven NP-complete [33. For practice, this is due to many highly- optimized SAT solvers being used as flexible reasoning engines in a variety of tasks such as model [17]. planning
checking [12 47 software verification
(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 ncuro-symbolic systems [4 42 [0 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 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 neuro-symbolic model that utilizes resolution to solve SAT problems by generating easy-to-check certificates.
A resolution proof is 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 further new resolution steps possible and the empty clause has not been derived. Generating such proof is an interesting problem from neuro-symbolic perspective because unlike other discrete combinatorial problems that have been considered before [6
it
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

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 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 assigmment absolves the resolution network from having to prove satisfiability by exhaustion. On that basis, given input formula, NeuRes proceeds in two parallel tracks: (1) finding 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 sertificate-based design. Since both of our certificate types are efficient 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, demonstrate that NeuRes achieves a higher accuracy while providing proof and requires only thousands of training samples.
As for most problems in theorem proving we not only interest in finding any proof but short proof. Resolution proof's can vary largely in their size depending on the resolution steps taken. Being able to efficiently check the proof, also allows 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 +
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 [dection6@ande and
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 httpa///gggthuub..oooahaaaaaaaee
2 Related Work
SAT Solving and Certificates. We refer to the annual SAT competitions (5) for 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] (6).. hence proof certificates have been partially required in this competition since 2013 [3]. Unlike satisfiable formulas, there are several ways certify unsatisfiable formulas (3) Resolution proofs 152 20 are easy 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 generate and space-efficient, but hard to validate. Verifying the proofs can take longer than their discovery [22] and requires highly optimized algorithms (3]]
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, simplified version has been trained to predict unsatisfiable cores and successfully integrated as branching heuristic in a state-of-the-ee as a phase selection heuristic 449] 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 [0]. The NeuroSAT architecture has also been applied on special classes of crypto-analysis addition to supervised learning, unsupervised methods have been proposed for solving SAT problems. For Circuit-SAT deep-gated DAG recursive neural architecture has been
SAT solver (42. .. Recent work has employed a related architecture
problems

---

Amsign
Assian
Aedign
Xy P2 -. vm..g
Imput
Passin Eibeelder
anbudding
by M/
*Xg
Atteution
Attention
Altection
Derived
ReslCpP33
RedCyCe
Figure 1: Overall NeuRes architecture
presented together with differentiable training objective to optimize towards solving the Circuit-SAAY problem and finding a satisfying assignment [i] For Boolean satisfiability, a differentiable training objective has been proposed together with 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 2
3 Proofs of (Un-)Satisfiability
start with a brief review certifying the (un-) Jutissitifiiaiiltty propositional formulas in conjunctive normal form. For set of Boolean variables V, identify with each variable V the positive literal x and the negative literal -r denoted by F. A clause corresponds to a disjunction literals and abbreviated by set of literals, e.g., {1, 3) represents (-xz V x:s). 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, } represents (-zi V .3)) (Ir, V22 V )..).. Any Boolean formula can be converted an equisatisfiable CNF formula in polynomial time, for example with Tseitin transformation 45]
A CNF formula is satisfiable if there exists assignment A : V - (T.-) such that all clauses are satisfied, i.c., each clause contains a positive literal æ such that A(x) T or a negative literal I such that A(x) 1. If no such assignment exists we call the formula unsatisfiabl.. 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 U {a}
(2U(T)
Res
CUCZ
Resolution effectively performs case distinction the value of variable a: Either it is assigned to false, then C₁ has to evaluate to true, or it is assigned to true, then C2 has to evaluate to true. Hence, may infer the clause C₁ U Cz. A resolution proof for CNF formula is sequence of applications of the Res rule ending in the empty clause.
Models
4.1 General Architecture
NeuRes is a neural network that takes a CNF formula as a set of clauses and outputs either a satisfying truth assignment resolution proof of unsatisfiability. As such, model comprises formula
3

---

embedder connected to two downstream heads: (1) an attention network responsible for selecting clause pairs, and (2) a truth assignment decoder. See Figure | 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, each step, the model selects a clause pair which gets resolved into new clause to append to the current formula graph while decoding candidate truth assignment in parallel. The model keeps deriving new clauses until the empty clause is found (marking resolution proof completion), satisfying assignment is found (marking certified sat verdict), or the limit on episode length is reached (marking timeout).
4.2 Message-Passsing Embedder
Similar NeuroSAT, we use message-passingg 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 Ae graphs where clause nodes are connected their constituent literal nodes and literals are connect to their complements (cf. Appendix A). For formula in m variables and n clauses, the outputs of this GNN are two matrices: E E I for literal embeddings and EC Rnxd for clause embedding, where d E N+ is the embedding dimension. Here we have two key differences from NeuroSAT. Firstly, NeuroSAT uses these embeddings as voters predict satisfiability through classification MIP. 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 update existing embeddings to reflect their relation to the newly inferred clauses. Consequently, we need to introduce new phase to the message-passing protocol, for which we explore two approaches: static embeddings and dynamic embeddings.
In static approach, we do not change the embeddings of initial clauses upon inferring 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 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 reasonably efficient.
Selector Networks
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 to the current formula. To realize our clause-pai pair selection mechanism, employ three attention-batn based designs.
4.3.1 Cascaded Attention (Casc-Attn)
Attn
Attn
E
E
Figure 2: Cascaded attention
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 shows this scheme where we perform the first query using the mean of the literal embeddings F. concatenated with zero vector while performing the second query using the mean of the literal

---

embeddings concatenated with the embedding vector Ex of the clause selected in the first query.
Formally, Casc-Attn selects clause index pair (c1, e2) as follows:
E 0
if
C, = argmax [u" tanh(Wiq: + W2Ef)) with q:
(I)
E
E
= 2
where W1 R2dxd W2 E Fdxd Rd 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 с₁ independently from C2, which is undesirable because the utility resolution step is determined by both clauses simultaneously (not sequentially).
4.3.2 Full Self-Attentin (Full-Attn)
To address the downside of independent clause selection, this variant performs self-altention between all clauses to obtain matrix S E R=** where St,j represents the attention score of the clause pair (ct, ey) 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.
3
E
Self-Attn
Figure 3: Full self-attention
Formally, Full-Attn selects clause index pair (c1, 62) as follows:
(cI, C2) = argmax Sig with Q= &= K K=EWH. S QKT (i,))
(2)
Vd
where Wo E Rddd Wx Bdxd 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 valid every step.
4.3.3 Anchored
(Anch-Attn)
In Full-Attn, the attention grid grows quadratically with the number of clauses. In this variant, we relax this cost by exploiting property of binary resolution where each step targets a single variable in the two resolvent clauses. This allows us narrow down candidate clause pairs by first selecting variable as anchor on which our clauses should be resolved. As such, we do not need to consider the full clause set once, only the clauses containing the chosen variable v. We further compress attention grid by lining clauses containing the literal v rows while lining clauses containing the literal t on columns. This reduces the redundancy of the attention grid since clauses containing the variable with the same parity cannot be resolved In this scheme, we have two attention modules: one attention network to choose an anchor variable followed by self-attention network to produce the anchored score grid.
there no point in matching them.
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 select variables. Secondly, self-attention in Full-Attn matches any pair of clauses (c;, e5) 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 self- attention scores for clause pairs in only one order (positive instance negative instance). Formally,

---

-42
E
Figure 4: Anchored self-attention
Anch-Attn selects an anchor variable follows:
argmax uu tanh(W, + W2 + E )
(3)
where W1 E Rdxd W2 R u E I2 are trainable network parameters. The clause index pair (c1, 02) is then selected according to the same equations of Full-Attn (Eq, 2 using the u-anchored set of clause embeddings.
4.4 Assignment Decoder
To extract satisfying assignments, we use sigmoid-activated MLP d on top the literal embeddings EL to assign a truth value A(4)) to a literal 4 as shown in Eq.
Á(L) o (v(E))
(4)
Note that since for each variable, we have positive and negative literal embeddings, can construct two different truth assignments 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 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 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 clauses (positive and negative literals are connected by an undirected edge that does not distinguish their parity). As such, both literal nodes have different local view into the rest of formula, which could result in one of them leading to a satisfying assignment faster than the other.
direct supervision during
Training and Hyperparameters
5.1
Dataset
For our training and testing data, we adopt the same formula generation method as NeuroSAT [43]. namely SR(n) where the number of variables in the formula. This method was designed to generate generalized formula distribution that is not limited a particular domain of SAT problems. To control data distributions, each formula. For our training data, we use formulas in SU 40)) where U110, 41),40) denotes the uniform distribution comprising resolution proofs and truth assignments, we use the BooleForce solver [8] on the formulas generated the SR distribution.
vary the range the number of Boolean variables involved in
integers between 10 and 40 (inclusive). To generate teacher certificates
5.2
Loss Function
We train our model in supervised fashion using leacher-foreing on solver certificates. During unsar 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 likelihood of teacher choices y,. thereby minimizing the resolution loss L shown in Eq
LRes ---- Σ log(p(ye: 0)) (T-t)
(5)

---

During sar episodes, we minimize Lea computed as the binary cross-entropy loss between the sigmoid-activated outputs of assignment decoder A V [0, 1] and the teacher assignment A:V {0, }] as shown in Eq. 6
TT Σ BCE(A()).
sat T Σ
(6)
In both types of episodes, step-wise losses are weighted by a hime-horizon discounting factor Y < 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.
5.3 Hyperparameters
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 batch size of and the Adam optimizer 2 for 50 epochs which took about six days on single NVIDIA A100 GPU. We linearly anneal the learning rate from x 10 to zero over the training episodes. This empirically yields better results than using a constant learning rate. We use time discounting factor 7 0.99 for the episodic loss. We apply global-norm gradient clipping with ratio of 0.5
38
6 Generating Resolution Proofs
NeuRes uses resolution as the core reasoning technique for certificate generation, both in the unsar and sat cases. Hence, we start with an in-depth comparative evaluation of several internal variants for resolution only. In particular, proof length relative the teacher, denoted by p-Len iPiete 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 SR(U(10 (10, 40)) and test our models on 10K unseen formulas belonging to the same distribution. We more formulas than the model was trained to more reliably demonstrate its learning capacity.
evaluate the success rate (i.c., problems solved before timeout) and |Pasated
Table 1: Performance of attention variants on unsat SR(U(10,40) test problems.
STATIC-EMBED
DYNAMIC-EMBED
VARIANT
PROVEN (%)
P-LEN
PROVEN (%)
P-LEN
CASC-ATTN
14.72
1.87
37.33
1.79
FULL-ATTN
25.38
1.61
95.2
1.67
ANCH-ATTN
28.72
2.12
60.5
2.28
6.1 Attention Variants
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 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 the static setting can explained through the full connectivity of its attention grid (proven in Appendix B). Since dynamic-embedding Full-Attn is the best-performing configuration over in- distribution test settings, we will demonstrate the remaining evaluation experiments exclusively on this variant.

---

Table 2: Bootstrapped training data reduction statisties. Reduction statisties computed on the SR 40)) training set while p-Len and success rate are computed on a test set of the same distribution.
REDUCTION DEPTH
MAX: 23, AVG: 6.6
PROOF REDUCTION (%)
MAX: 86.11, AVG: 33.51
PROOFS REDUCED (%)
90.08
TOTAL REDUCTION (%)
31.85
P-IEN
1.15
SUCCESS RATE (%)
100.0
6.2 Shortening Teacher Proofs with Bootstrapping
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-foree forcing manages to shorten 188% of teacher proofs by notable factor (ef. 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 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 We find that bootstrap- ping 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 metric for reduction depth computed the number of progressive reductions made to proof. To further quantify this effect, we report the maximum and average reduction ratios of reduced proofs relative teacher proofs. Finally, report the total reduction made 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 small reduction example (from 20 steps to 10 steps) for space constraints, but observed many more examples of much larger reductions (e.g., over 400 steps).
7 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 x (Prexcher)) and optimality (p-Len) are measured similarly to previous experiments. For satisfiable formulas, we set the timcout (maximum #trials) to 2 x [V). Ultimately, this section aims to investigate the effect of incorporating certificate-driver 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 sar but only predicts unsat, we train classificaiion MLP top of our trained NeuRes model to further showcase the benefit of our representations on prediction accuracy.
Table 3 confirms this main hypothesis. In essence, this result points to the fact that learning signals obtained from training on unsat certificates largely enhance the ability the neural network to extract useful information from the input formula. This is doubly promising considering NeuroSAT was

---

Table 3: Performance of full solver mode tested SR(40) problems and trained on SR (10, 40))
problems where PREDICTED refers to the satisfiability prediction without certificate.
PROVEN (%)
PREDICTED (%)
MODEL
SAT
UNSAT
TOTAL
SAT
UNSAT
TOTAL
NEURES
96.8
99.6
98.2
84.28
99.2
91.65
NEUROSAT
43 70
73
96
85
trained on millions 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.
Utilizing Model Fan-Out
In our Full-Attention module, we compute n² 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 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 steps of the attention grid after each forward pass. 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 shows that taking the top 3 steps already yields a massive reduction in proof lengths along with significant boost to the success rate.
Table 4: Performance of different model fan-outs SR(40) test data. Proof length (p-Len) and #Model Calls are both normalized by the length of the teacher proof.
FULL-ATTN FAN-OUT
P-LEN
#MODEL CALLS
TOTAL PROVEN ( (%)
TOP-1
1.15
1.15
98.2
Top-3
0.57
0.49
99.9
TOP-5
0.52
0.43
100.0
One way to offset the attention grid inflation with higher fan-out would be to keep saliency map for all clauses then discarding i: clauses with the least saliency scores after each forward pass. One simple way to compute this saliency score for clause would be the sum/mean/max of its respective row in the attention scores grid. Another proxy for saliency could the recency score reflecting how many steps have elapsed since the last time given clause was used.
9 Generalizing to Larger Problems
In order to test model's auttof-ddistibution performance, 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 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 problem distributions, and a higher final success rate on all of them except for SR(40) which both models nearly score 100%. Particularly, NeuRes shows higher first-try success on the 3 largest problem sizes where AA solves zero near-zero problems the first try.

---

SP240 SR (14)
SA1 SucDse Rate
Figure 5: SAT success rate over iterations.
10 Conclusion
In this paper, we introduced 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 pertificate-bsse training and resolution-aide 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 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 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 bootstrapped training procedure that uses teacher proofs as guide as opposed to a golden standard.
opposed to using
Acknowledgments and Disclosure of Funding
This work was supported by the European Research Council (ERC) Grant HYPER (No. 101055412).
References
[1] S. Amizadeh, S. Matusevych, and M. Weimer. Learning to solve circuit-sat: An unsupervised differentiable approach. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans. LA, USA, May 6-9, 2019. OpenReview.net, 2019.
[2] T. Anthony, Z. Tian, and D. Barber. Thinking fast and slow with deep learning and tree search. In I. Guyon, U. von Luxburg, S. Bengio, H. M. Wallach, R. Fergus, S. V. N. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 5360-5370, 2017.
[3] A. Balint, A. Belov, M. Heule, and M. Járvisalo, editors. Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, volume B-2013-1 of Department of Computer Science Series of Publications B. University of Helsinki, Finland, 2013.
10

---

[4] M. Balunovic, P. Bielik, and M. T. Vechev. Learning to solve SMT formulas. In S. Bengio, H. M. Wallach, H. Larochelle, K. Grauman. N. Cesa-Bianchi and R. Garnet,, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, pages 10338-10349, 2018.
[5] Balyo, M. Heule, M. Iser, M. Järvisalo, and M. Suda, editors. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023.
[6] K. Bansal, M. Loos, M. N. Rabe, C. Szegedy, and S. Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In K. Chaudhuri and R. Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 454-463. PMLR, 2019.
[7] I. Bello, H. Pham, Q. V. Le, M. Norouzi, and S. Bengio. Neural combinatorial optimization with reinforcement learning. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, Frunce, April 24-26, 2017, Workshop Track Proceedings. OpenReview.net, 2017.
[8] A. Biere. Booleforce sat solver. https://ffv. /tt.uaatboolleoorce... 2010.
[9] R. Brummayer, F. Lonsing, and A. Biere. Automated testing and debugging of SAT and QBF solvers. In O. Strichman and S. Szeider, editors, Theory and Applications of Satisfiability Testing- SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, 2010.
[10] C. Cameron, R. Chen, J. S. Hartford, and K. Leyton-Brown. Predicting propositional satisfiabil- ity via end-to-end learning. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, New York, NY, USA, February 7-12, 2020, pages 3324-3331. AAAI Press, 2020.
[1]] Q Cappart, D. Chételat, E. B. Khalil, A. Lodi, C. Morris, and P. Velickovic. Combinatorial optimization and reasoning with graph neural networks. J. Mach. Learn. Res., 24:130:1-130:61 -130661, 2023.
[12] E. M. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods Syst. Des., 19(1):4-34, 2001.
[13] S. A. Cook. The complexity of theorem- theorem-proving procedures. In M. A. Harrison, R. B. Banerji, and J. D. Ullman, editors, Proceedings of the 3rd Anmual ACM Symposium Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151-158. ACM, 1971.
[14] M. Cosler, F. Schmitt, C. Hahn, and B. Finkbeiner. Iterative circuit repair against formal specifications. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023.
[15] A. Darbari, B. Fischer, and J. Marques-Sile Silva. Industrial strenggh certified SAT solving through verified SAT proof checking. In A. Cavalcanti, D. Déharbe, M. Gaudel, and J. Woodcock, editors, Theoretical Aspects of Computing ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings, volume 6255 of Lecture Notes in Computer Science, pages 260-274. Springer, 2010.
[16] M. Davis and H. Putnam. A computing procedure for quantification theory. J. ACM, 7(3)2011 215, 1960.
[17] I. M. de Moura and N. S. Bjömer. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69-77, 2011.
[18] V. Firoiu, E. Aygün, A. Anand, Z. Ahmed, X. Glorot, L. Orseau, L. M. Zhang, D. Precup, and Mourad. Training first-order theorem prover from synthetic data. CoRR, abs/2103.00775 2021.
11

---

[19] E. First, M. N. Rabe, T. Ringer, and Y. Brun. Baldur: Whole-proof generation and repair with large language models. CoRR, 009000 2023.
[20] E. I. Goldberg and Y. Novikov. Verification of proofs of unsatisfiability for CNF formulas. In 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany, pages 10886-10891. IEEE Computer Society, 2003.
[21] C. Hahn, F. Schmitt, J. U. Kreber, M. N. Rabe, and B. Finkheiner. Teaching temporal logics to neural networks. In 9th International Conference on Learning Representations, ICIR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021.
[22] M. Heule, W. A. H. Jr., and N. Wetzler. Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verification Reliab., 246 2014.
[23] M. H. Heule. Proofs of unsatisfiability.. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 368. IOS Press, 2021.
[24] M. J. H. Heule and O. Kullmann. The science of brute force. Commun. ACM, 60(8):70-79, 2017.
[25] G. Irving, C. Szegedy, A. A. Alemi, N. Eén, F. Chollet, and J. Urban. Deepmath deep sequence models for premise selection. In D. D. Lee, M. Sugiyama, U. von Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems 29: Annual Conference on Neurul Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pages 2235-2243, 2016.
[26] M. Järvisalo, M. Heule, and A. Biere. Inprocessing rules. In B. Gramlich, D. Miller, and U. Sattler, editors, Automated Reasoning 6th International Joint Conference, IJCAR 2012. Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 355-370. Springer, 2012.
[27] H. A. Kautz and B. Selman. Planning as satisfiability. In B. Neumann, editor, 10th European Conference on Artificial Intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings, pages 359-363. John Wiley and Sons, 1992.
[28] E. B. Khalil, H. Dai, Y. Zhang, B. Dilkina, and L. Song. Learning combinatorial optimization algorithms over graphs. In I. Guyon, U. von Luxburg, S. Bengio, H. M. Wallach, R. Fergus, S. V. N. Vishwanathan, and R. Gamett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017 December 4-9, 2017, Long Beach, CA, USA, pages 6348 6358, 2017.
[29] D. P. Kingma and J. Ba. Adam: A method for stochastic optimization. arXiv preprint arxiv: I4I:: 1.... 6980, 2014.
[30] W. Kool, H. van Hoof, and M. Welling. Attention, learn solve routing problems! In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.nee 2019.
[31] P. Lammich. Efficient verified (UN)SAT certificate checking. J. Autom. Reason., 64(3):133-332 2020.
[32] G. Lederman, M. N. Rabe, S. Seshia, and E. A. Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
[33] S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk. Deep network guided proof search. In T. Eiter and D. Sands, editors, I.AR-21, 21, 2/st International Conference on for Program- ming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC Series in Computing, pages 85-105 EasyChair, 2017.
[34] J. Marques-Silva, Lynce, and S. Malik. Conflict-driven clause learning SAT solvers. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability SScond Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2021.
12

---

[35] M. Mikula, S. Antoniak, S. Tworkowski, A. Q. Jiang, J. P. Zhou, C. Szegedy, L. Kucinski, Milos, and Y. Wu. Magnushammer. transformer-based approach to premise selection. CoRR, abs/2303.04488 2023.
[36] E. Ozolins, K. Freivalds, A. Draguns, E. Gaile, R. Zakovskis, and S. Kozlovics, Goal-aware neural SAT solver. In International Joint Conference on Neural Networks. IJCNN 2022, Padua, Italy, July 18-23, 2022, pages 1-8. IEEE, 2022.
[37] A. Paliwal, S. M. Loos, M. N. Rabe, K. Bansal, and C. Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, New York, NY, USA, February 7-12, 2020, pages 2967-2974. AAAI Press, 2020.
[38] R. Pascanu, T. Mikolov, and Y. Bengio. Understanding the exploding gradient problem. CoRR, abs/1211.5063, 2(417):1, 2012.
[39] S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal mathe- matics statement curriculum learning. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023.
[40] S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. CoRR, 00//2009003933. 2020.
[41] F. Schmitt, C. Hahn, M. N. Rabe, and B. Finkheiner. Neural circuit synthesis from specification patterns. In M. Ranzato, A. Beygelzimer, Y. N. Dauphin, P. Liang, and J. W. Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurlPS 2021, December 6-14, 2021, virtual, pages 15408-15420, 2021.
[42] D. Selsam and N. S. Bjørner. Guiding high-performance SAT solvers with unsat-core predictions. In M. Janota and Lynce, editors, Theory and Applications of Satisfiability Testing SAT 2019 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 336-353, Springer, 2019.
[43] D. Selsam, M. Lamm, B. Bünz, P. Liang, L. de Moura, and D. L. Dill. Learning a SAT solver from single-bit supervision. In 7th International Conference Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019.
[44] L. Sun, D. Gérault, A. Benamira, and T. Peyrin. Neurogift: Using machine learning based sat solver for cryptanalysis. In S. Dolev, V. Kolesnikov, S. Lodha, and G. Weiss, editors, Cyber Security Cryptography and Machine Learning- Fourth International Symposium, CSCML 2020, Be's er Sheva, Israel, July 2-3, 2020, Proceedings, volume 12161 of Lecture Notes Computer Science, pages 62-84. Springer, 2020.
[45] G. S. Tseitin. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967-1970, pages 466-483, 1983.
[46] O. Vinyals, M. Fortunato, and N. Jaitly. Pointer networks. Advances in neural information processing systems, 28, 2015.
[47] Y. Vizel, G. Weissenbacher, and S. Malik. Boolean satisfiability solvers and their applications in model checking. Proc. IEEE, 103(1 1):2011-2035, 2015.
[48] M. Wang, Y. Tang, J. Wang, and J. Deng. Premise selection for theorem proving by deep graph embedding. In I. Guyon, U. von Luxburg, S. Bengio, H. M. Wallach, R. Fergus, S. V. N. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA. pages 2786-2796, 2017.
[49] W. Wang, Hu, M. Tiwari, S. Khurshid, K. L. McMillan, and R. Miikkulainen. Neuroback: Improving CDCL SAT solving using graph neural networks. In The Twelfih International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. Open- Review.net, 2024.
13

---

[50] N. Wetzler, M. Heule, and W. A. H. Jr. Drat-trim: Efficient checking and trimming using expres- sive clausal proofs. In C. Sinz and U. Egly, editors. Theory and Applications of Satisfiability Testing- SAT 2014- - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSI. 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer, 2014.
[51] K. Yang and J. Deng. Learning to prove theorems via interacting with proof assistants. In K. Chaudhuri and R. Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California. USA, volume 97 of Proceedings of Machine Learning Research, pages 6984-6994. PMLR, 2019.
[52] L. Zhang and S. Malik. Validating SAT solvers using an independent resolution-basel checker: Practical implementations and other applications. In 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany, pages 10880-10885. IEEE Computer Society, 2003.
14

---

Appendix
A NeuroSAT Formula Graph Construction
(a) Literal-to-Clause Phase
(b) Clause-to-Literal Phase
Figure 6: Two-phase message- message-passing round on NeuroSAT formula graph.
NeuroSAT-style formula graphs have designated node types: clause nodes connected to the literal nodes corresponding to their constituent literals [43] For example, in Figure the clause contents as follows: C1 (a b), C2 (a V b). C3 (a b). Each message-passing and (2) Clause-to-Literal (and implicitly Literal-to- Co-o-plemmmm))t This construction is particularly efficient as it allows the message-passingg protocol to cover the entire graph connectivity in at most [V] + 1 rounds where V is the set of variables in the formula.
round involves two exchange phases: (1) Literal-to-Clann
B Clause Connectivity Under Static Embeddings
In Section 4.2 we stated that under static embeddings for a derived clause, as the embedder creates its embedding. only updates the representations of the variables involved it leaving other clause embeddings intact. This might present problem for Full-Attn where the attention grid contains all clauses including disconnected" pairs. An example of such pair would be two derived clauses that do not share variable. This could potentially lower the efficacy of the Full-Attn mechanism as it tries to match clauses that are unaware of each other. Interestingly, despite being a relaxation on Full-Attn, Anch-Attn has distinct edge over Full-Attn under static embeddings form of the following property:
Lemma B.1. Clauses in the variable-anchorer attention grid of Anch-Attn are guaranteed to be connected under both static and dynamic embeddings.
Proof. Let e be a variable in the input formula, and the set of clauses a u-anchored attention grid be A. We show that always have least one clause A, A that reaches all other clauses in A on the formula graph. We make two case distinctions:
Case 1: All clauses in A are input clauses (in the original formula). Here, the lemma follows trivially since these clause were connected during the input-phase message-passing protocol as they share at least one variable v.
Case A contains derived clauses. Let A, be the most recently derived clause in A. Since A shares variable v with all other clauses in A. then A, would be connected to them all during the derivation- phase message-passing protocol immediately after A, was derived. This because A, receives a message from V (under both static and dynamic embeddings) containing information about all other clauses containing e, which precisely A ( {A,). Therefore, the lemma holds.
O
Wee use the terms connected and disconnected here to refer to the fact of whether two nodes have exchanged messages (in either direction) not, respectively.
15

---

C Teacher Proof Reduction
One rather interesting observation Table 5 is that the model appears be marginally better 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 teacher-foreed 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.
Table 5: Teacher proof reduction statistics of ton-bootstrapped model trained on unreduced SR 40)) dataset. Note that all rows, except for Total Reduction, are computed over the reduced portion of the dataset, i.e. the proofs that were successfully shortened by NeuRes.
TRAIN
TEST
PROOFS REDUCED
17.82
18.29
MAX. REDUCTION
86.11
76.4
AVG. REDUCTION
23.55
23.65
TOTAL REDUCTION
3.07
3.15
D Runtime Comparison with Traditional Solver
In the following table, 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 test dataset. For both Full-Attn models, implementation.
Python prototype implementation; for BooleForce, we use official C
Table 6: Average time (ms) to solve an instance by neural model vs. teacher solver.
SOLVER
SAT (MS)
UNSAT (MS)
ToTal (MS)
FULL-AUTN TOP-1
2.3
88
45.15
FULL-ATTN TOP-3
54.4
28.7
BOOLEFORCE
4
5
4.5
E
Model Size Comparison with NeuroSAT
In terms of the model architecture, both NeuRes and NeuroSAT models can be broken down to:
Embeeddigg/Represnttation Network: for both models, this network is LSTM-based GNN that embeds the formula graph by message-passing. We use the exact same architecture and model size ensure that our improved representations are result of our fully certificate- based learning objective as opposed to a tweak in the model architecture. This GNN has 429, 824 parameters in total.
Downstream Networks:
NeuroSAT: uses 3-layer MLP applied on the literal embeddings (width 128) to extract the literal votes to predict if the formula satisfiable or not. This MLP has 128 x 128 x 3 49, 152 parameters. NeuRes (Full-Attn): uses attention module to select clause pairs. This attention network composed of two 1-layer MLPs for the query and key transformations whole attention module has 128 x 128 2 = 32, 768 parameters. To decode the variable assignments, NeuRes uses 2- layer scalar MLP with 128 128 128 16, 512 parameters
the clauses embeddings (width 128). The
Total NeuroSAT size 429, 824 49, 152 478, 976 parameters
Total NeuRes size = 429, 824 + 49, 280 479, 104 parameters
All in all, NeuRes only learns 128 more parameters.
16

---

17.3
15.3
[-5.3] 31
1A
(4,,7)
[+)
(3.-3,30) 30)
(2.10]
F:0 -.
12.50
6-. 4)
4,
(3.7, 99
648
(5,
15. 100
c30.
G St
(a) Teacher Proof
6%
IK]
63.91
6.
18. .1
L6, 2,
65.4)
12 S1
1-5.-22
d5. 301
(b) NeuRes Proof
Figure 7: Teacher Proof Reduction Example
17

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
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 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 long is clear that these goals are not attained by the paper.
2. Limitations
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 the conclusion the paper (Section TO
Guidelines:
The answer NA means that the paper has 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 (c.g.. independence assumptions, noiseless settings, model sellsspeciiiationn 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 few datasets or with 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, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails 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 faimesss.
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 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
18

---

Answer:
[NA]
Justification:
The paper does not include any formal theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: We reference the data generation method in Section 5.1 A detailed math- ematical description of the architectures is given in Section Optimization details and hyperparameters are disclosed in Section 5.2 and Section 5.3
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reprodueibility may be tricky in some cases, in which authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
5. Open access to data and code
19

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
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.co cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (c.g., for a new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
//nips //ips.cc//pil wttpcccpppppppppeeeeeeeeeeeeeeee httae//ggiieee/eeeeebbissssssss /Cc////oddiiisssseeeeeee siwiissiiciiiyyyycc for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Question:
Answer: [Yes]
Justification: Training and test splits are specified at the beginning of Section and Section Optimization and hyperparameters 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 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, as supplemental material.
7. Experiment Statistical Significance
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, confi- dence intervals, statistical significance tests, 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 with given experimental conditions).
20

---

The method for calculating the error bars should be explained (closed form formula, call 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.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2 2-sigma error bar than state that they have 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 range (e.g. negative етrоr rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
The compute resources reported in Section 53
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU 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 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 failed experiments that didn't make into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics https: /ate:///niupppeee wwtpuuupssccppuuulieeeee htt.c///bbbcc/tthccccccieeell.l.
Answer: [Yes]
Justification: No harms were caused by the research process nor are harmful consequences expected from the propositional logie 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 cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader Impacts
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 this work to build hybrid SAT solvers. Such solvers are used in 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 detected easily, unlike in, e.g., mere satisfiability prediction.
Guidelines:
21

---

The answer NA means that there is no societal impact of the work performed.
If the authors answer NA No, they should explain why their work has societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious 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 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 intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (c.g., gated release models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms monitor how system learns from feedback over time, improving the efficiency and accessibility ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
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 challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
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?
Question:
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 dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
22

---

For scraped data from a particular source (e.g., website). the copyright and terms of service of that souree should be provided.
assets are released, the license, copyright information, and terms use in the package should be provided. For popular datasets, paperssi thood cww datasets has curated licenses for some datasets. Their licensing guide can help determine the license of 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 encouraged to reach out to the asset's 's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
We will make new assets publically available after the double-blind review ended.
Justification:
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model 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 anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. 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 details about compensation (if any)?
Answer: [NA]
Justification:
The paper does not involve crowdsoureing 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 contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurlPS 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.
15. 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 crowdsoureing nor research with human subjects.
23

---

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.
24


Reviews:
[{"review_id": "WXO63QS5sG", "reviewer": "Reviewer_MVHU", "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.", "questions": "1. Could you compare the learned resolution strategy with existing ones?\n2. Have you conducted ablation studies of the effect of the model architecture to proof length/success rate?", "limitations": "The paper discusses the scalability/efficiency limitation of the proposed method. I do not see the potential negative societal impact of their work.", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 1, "contribution": 3, "strengths": "- Instead of directly learning to predict satisfiability, this paper proposes to learn the strategy to apply the resolution rule. I like this general approach, as it can provide actual proofs of both satisfiability and unsatisfiability.\n- Breaking down the resolution strategy prediction task to two steps (i.e., choosing a variable and then choosing two clauses) is a nice optimization that reduces the computational cost.\n- The approaches are explained clearly and the paper is relatively self-contained.", "weaknesses": "- 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. \n - 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).\n- The paper only considers very simple SAT instances and it seems difficult to scale the presented approach to much larger real-world instances.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their comments, and we address their reservations below. \n\n> The comparison with NeuroSAT to me is quite apple-to-orange. \n\n> 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).\n\n- The learning objectives indeed differ, but the general task remains the same, i.e., propositional SAT. The difference is that our approach (more ideally) decides the problem by proof (resolution or assignment) not just by prediction, which cannot be easily verified. Reframing the learning objective is a major aspect of innovation in machine learning methods; in our case, we reframe it from prediction to certificate generation. Note that we also compare with NeuroSAT in terms of **prediction accuracy** and **assignment decoding success rate**, both of which are 1-to-1 comparisons.\n- \"Better\" and \"less\" in our context refer to two specific outcomes of our project:\n  - We claim better representations based on the fact that the same prediction network achieves notably higher accuracy when trained on our representations vs. the NeuroSAT representations.\n  - \"less data\" here directly refers to the fact that our model is trained on two orders of magnitude fewer data samples (formulas) than NeuroSAT (**16K** vs. **several millions**) and on the same data distribution $SR(U(10, 40))$.\n\n> Q1: Could you compare the learned resolution strategy with existing ones?\n\n- To the best of our knowledge, NeuRes is the first learning-based approach for propositional resolution in the literature. \n- The $\\\\text{p-Len}$ metric reflects a comparison with the BooleForce solver (used as a teacher) in terms of proof length. To get a numeric sense about the runtime, on $SR(40)$ formulas, it takes NeuRes an average of \\~45 ms (2.3 ms for sat and 88 ms for unsat) to solve an instance in our Python prototype implementation while it takes \\~4 ms to solve it on a C implementation of the BooleForce solver. Although NeuRes produces much shorter proofs than BooleForce in many cases, it still lags behind it in terms of pure runtime, as is generally the case for neural methods at the current state of the art.\n- We do not compare with more traditional solvers (other than BooleForce) since the objective of our paper is more towards improving the learning aspects of neural solvers as opposed to competing with traditional symbolic solvers. \n\n> Q2: Have you conducted ablation studies of the effect of the model architecture to proof length/success rate?\n\nOver the course of this project, we conducted numerous experiments that we intend to include in an appendix because they were not essential to the main findings except for the three main **attention mechanisms/architectures** (which we already ablate in the main paper). We are happy to include these in an appendix to the paper. Please find some of our other ablations below:\n\n**Further ablations:**\n\n- Important Notes: \n  - We decided to not modify the GNN architecture to ensure our improved performance is not a result of a mere architecture tweak on NeuroSAT by adopting the same network and mechanism to obtain the initial representations.\n  - Our downstream networks (assignment decoder and prediction head) are both simple and small MLPs to clearly highlight the impact of our certificate-driven learning setting/objective. This is a quite common approach towards assessing the quality of learned representation by how well a simple downstream model performs on them. Examples of this can be found in the representation probing literature \\[1\\] \\[2\\].\n- **Global Context Vector**: We experimented with using an LSTM **encoder-decoder network** that takes in the initial clause embeddings and produces a global summary/context vector (its last hidden state) to condition our downstream networks on. This was in fact our original architecture, but we later found out that it was unnecessary to (and even slightly hurts) our model performance since our dynamic embedding already captures the relevant state information locally in the clause embedding, and so conditioning our attention module on the global context vector did not add new information. We report the performance comparison between this variant and our simplified  model (w/o the encoder-decoder) on SR(40) test data below (total over both SAT and UNSAT):\n\n  | Variant                    | Proven (%) | Predicted (%) |\n  |----------------------------|------------|---------------|\n  | Global Context (Enc-Dec)   | 97.4       | 91.35         |\n  | Local Context (simplified) | **98.2**       | **91.65**         |\n- **Clause Pair Scoring (Full-Attn)**: the resolution operator is symmetric on clause order while attention is not. That is, for each clause pair $(c_1, c_2)$, their attention score on the upper triangle of the attention grid $S(c_1, c_2)$ is not necessarily the same as on the lower triangle $S(c_2, c_1)$. We experimented with different ways to combine both scores, and found that only taking the upper triangle score performs best (and is also faster).   \n\n| Scoring Scheme    | Proven (%) | Predicted (%) |\n|-------------------|------------|---------------|\n| Upper Triangle    | **98.2**       | **91.65**         |\n| Upper + Lower     | 97.25      | 91.35         |\n| Max(Upper, Lower) | 97.5       | 91.4          |\n| Min(Upper, Lower) | 51.1       | 86.15         |\n\n**References:**\n\n\\[1\\] Akhondzadeh, Mohammad Sadegh, Vijay Lingam, and Aleksandar Bojchevski. \"Probing graph representations.\" International Conference on Artificial Intelligence and Statistics. PMLR, 2023.\n\n\\[2\\] Alain, Guillaume, and Yoshua Bengio. \"Understanding intermediate layers using linear classifier probes.\" arXiv preprint arXiv:1610.01644 (2016).", "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": "", "extra_scores": {}}, {"review_id": "NnnxFneKlr", "reviewer": "Reviewer_R9jd", "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.", "questions": "- How easy do you think the approach can be combined with traditional SAT optimization?\n- Have you thought about extending the approach to anything beyond propositional SAT?", "limitations": "The authors discussed the limitation in section 9 and I agree with them.", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "+ The model learns to pick resolution pairs rather than naively predicts binary satisfiability, resulting in an overall elegant approach that combines classic symbolic reasoning and machine learning. An unsat \"prediction\" always comes with a valid proof, and a sat prediction is alway correct.\n+ Detailed attention mechanisms are presented in a progressive manner. Each attention mechanism is accompanied by proper motivation and explanation. The approach is clearly well thought-out and optimized carefully. Again, not applying pretrained language models blatantly stands out in the flooded submissions today.\n+ I like the idea of predicting additionally the truth assignment. Although in principle the assignment can be read off once the resolution is complete, it's always better to terminate early. And by learning to pick the resolution pairs and assigning truth values simultaneously, more semantics can hopefully be injected into the models. Well done!", "weaknesses": "- 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your feedback and questions; we're glad you enjoyed the paper!\n\nWe address your comments in the following.\n\n> Speed can potentially be an issue.. for large problems, the calls can be quite numerous.\n\n- It is true that speed is a limiting factor in scaling deep learning models to very large instances. Particularly, our model inherits the scaling laws of transformers (due to self-attention) which famously limits LLMs' ability to handle very long sequences. In our context, there are two ways to tackle this:\n\n  **(1) Reduce the cost of a single forward pass**: this can be done in numerous ways, but we want to highlight a particularly relevant one of reducing the size of the attention grid. We already showed an example of that in Anchored-Attention, but there are generally more ways to only compute attention scores on a subset of clauses. This subset of interest can either be determined by a heuristic or by a learned scoring model (e.g., MLP). Keeping a constant-sized attention window would drastically alleviate scaling constraints on our network at a certain expense of limiting exploration.\n\n  **(2) Reduce the total number of calls**: in our Full-Attention module, we compute $N^2$ scores and only take the top-score resolution step. This arguably underutilizes the attention grid. On that basis, we conducted a small ablation (over the course of these rebuttals) where we perform the top 3 resolutions instead of only the top 1. This led to notable gains across all our main metrics. We report our findings on $SR(40)$ test data in the table below. Proof length and #Model Calls are both normalized by the length of the teacher proof.\n\n| Variant | Proof Length (normalized) | #Model Calls (normalized) | Total Proven (%) |\n|---------|---------------------------|---------------------------|------------------|\n| Top-1   | 1.15                      | 1.15                      | 98.2             |\n| Top-3   | **0.57**                      | **0.49**                     | **99.9**             |\n\n> Q1: How easy do you think the approach can be combined with traditional SAT optimization?\n\n- One promising way to combine our approach with traditional CDCL-style SAT solvers is to use our models as variable selection heuristics (i.e., to decide which variable to branch on). NeuroCore \\[5\\] trained a simplified NeuroSAT model to assign scores to variables reflecting how likely they are to cause a conflict, which led to a significant boost to a traditional MiniSat solver where it solved 10% more problems within standard timeout on SATCOMP-2018. Since our approach produces better representations over NeuroSAT for SAT and UNSAT prediction, this suggests a natural way to combine and improve traditional solvers with our approach. It is worth mentioning that gathering training data for SATCOMP was a major challenge for the NeuroCore paper, so the data efficiency of NeuRes would be expected to pay off in that context.\n- Another way to create a hybrid solver would be periodically sampling resolution steps from NeuRes to augment a traditional CDCL solver. The rationale here is that the full resolution proof can be too costly, but intermediate resolution derivations could help find conflicts earlier during the branching which helps the solver save exploration time.\n\n> Q2: Have you thought about extending the approach to anything beyond propositional SAT?\n\n- At the moment, we are mainly interested in extending our approach to Quantified Boolean Formulas (QBF), for which a sound and complete resolution calculus exists \\[1\\]. QBF allows succinct expression of problems arising in AI planning \\[2\\] and verification \\[3\\], but is significantly less studied than propositional SAT. \n- QBF is a somewhat straightforward extension to NeuRes as it only requires the following modifications:\n  - Learning an extra variable embedding initialization: since in QBF, variables are either universally or existentially quantified, different initial embeddings should be learned to set both types of variables apart prior to message-passing.\n  - Encode quantification ordering over the variables to reflect the difference between $\\\\exists x \\\\: \\\\forall y$ and $\\\\forall y \\\\: \\\\exists x$. This can be done using positional encoding for instance.\n- In the long term, we are also interested in generalizing the insights from our resolution-based architectures to theorem proving in general, which is an area that has received significant attention from the machine-learning community. \\[4\\] gives a good overview. \n\n\n**References:**\n\n\\[1\\] Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. \"Resolution for Quantified Boolean Formulas.\" Information and Computation 117, 12-18 (1995).\n\n\\[2\\] Irfansha Shaik and Jaco van de Pol. \"Planning as QBF without Grounding.\" International Conference on Automated Planning and Scheduling, ICAPS 2022.\n\n\\[3\\] Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. \"Bounded Model Checking for Hyperproperties\". International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021.\n\n\\[4\\] Markus N. Rabe and Christian Szegedy. \"Towards the Automatic Mathematician\". International Conference on Automated Deduction, CADE 2021.\n\n\\[5\\] Selsam, Daniel, and Nikolaj Bjørner. \"Guiding high-performance SAT solvers with unsat-core predictions.\" Theory and Applications of Satisfiability Testing–SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019, Proceedings 22. Springer International Publishing, 2019.", "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": "", "extra_scores": {}}, {"review_id": "GmWPi7YGgB", "reviewer": "Reviewer_64Vk", "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.", "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?\n* 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": "The limitation about the performance of neural methods on SAT solving still lags behind symbolic solvers is discussed.", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "* The method is able to generate resolution proofs for UNSAT problems, which is a certificate for UNSAT problems, unlike previous methods such as NeuroSAT.\n* The method shows some generalizability to larger problems, which is a good sign for the method to be applied to larger problems.\n* The method is sometimes able to generate shorter resolution proofs than the teacher, and they propose a bootstrapping method to further improve the performance based on those shorter proofs.", "weaknesses": "* 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your review and comments. Please find your questions addressed below.\n\n> Q1: Could you explain how the method applies to SAT problems?\n\n- In the case of a satisfiable formula, NeuRes terminates when a satisfying truth assignment is found by the assignment decoder network. Initially the model doesn't know the SAT status of the formula, so at each step, it performs two operations: 1) derives a new clause by resolution, and 2) produces a candidate truth assignment. Track 1 guides the assignment search by making new inferences (clauses) on the formula. As you mentioned, track (1) proves UNSAT upon deriving the empty clause while track 2 terminates upon finding an assignment that satisfies all clauses.\n\n> Q2.1: How does the model size of NeuRes compare to the baseline NeuroSAT on the SAT problems?\n\n- In terms of the model architecture, both models can be broken down to:\n  - **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 certificate-based learning objective as opposed to a tweak in the model architecture. This GNN has 429,824 parameters in total.\n  - **Downstream Networks**:\n    - NeuroSAT: uses a 3-layer MLP applied on the literal embeddings (width=128) to extract the literal votes to predict if the formula is satisfiable or not. This MLP has 128\\*128\\*3 = 49,152 parameters.\n    - NeuRes (Full-Attn): uses an attention module to select clause pairs. This attention network is composed of two 1-layer MLPs for the query and key transformations on the clauses embeddings (width=128). The whole attention module has 128\\*128\\*2 = 32,768 parameters. To decode the variable assignments, NeuRes uses a 2-layer scalar MLP with 128\\*128 + 128 = 16,512 parameters\n\n       \n\nTotal NeuroSAT size = 429,824 + 49,152 = 478,976 parameters  \nTotal NeuRes size = 429,824 + 49,280 = 479,104 parameters\n\n(i.e., NeuRes only learns 128 more parameters)\n\n> Q2.2: How does the solving time compare between the two methods?\n\n- For **predicting** SAT status, both models have the same runtime as they use the same message-passing GNN to obtain formula embeddings and the same voting MLP to get the SAT prediction.\n- For **solving** SAT (i.e., with certificate/proof), the runtime depends on the instance size and SAT status as follows:\n  - **SAT**: the formula is solved when a satisfying truth assignment is found. In this case, the runtime is decided by two factors: \n    - #Attempts: Through our experiments, we show that NeuRes finds satisfying assignments to many more SAT instances after 1000 attempts. To see this, you can compare Figure 5 in our paper vs. Figure 5 in the NeuroSAT paper.\n    - The time cost of a single attempt: at any step, NeuRes extracts the full assignment in a single forward pass through a 2-Layer MLP over the literal embeddings. In contrast, NeuroSAT performs a k-means clustering on literal embeddings to separate them into two 2 clusters against a predicate. The latter is significantly more costly as it performs an iterative clustering process that could take hundreds of iterations to converge (the default limit is set to 300 iterations in the NeuroSAT implementation).\n  - **UNSAT**: the formula is solved when the model derives a full (resolution) proof of the empty clause (falsum) from it. Since NeuroSAT does not solve UNSAT formulas, a runtime comparison is not possible (UNSAT cores are not proofs). However, for a general idea, the NeuRes runtime in UNSAT cases depends on the number of resolution steps needed to derive the empty clause. In our evaluation, we've shown that NeuRes in many cases produces much shorter proofs than the teacher traditional solver, and on average to be around 1.15x in length. This is under our 1-step-per-forward-pass model. We thought that this arguably underutilizes our attention grid by only taking the top-1 clause pair, so we performed a side experiment in the rebuttals period to explore potential gains of taking the top 3 clause pairs at each step and perform them. The idea is to reduce the total number of forward passes to the model by performing more resolution steps per fwd pass. On SR(40) test data, this led to a 57.4% reduction in episode lengths (total number of forward passes), model proofs that are on average 43% shorter than the teacher's (p-Len = 0.57 vs the previous 1.15), in addition to a +1.7% total success/proof rate (99.9% vs the previous 98.2%). We will include this experiment in the main paper for the sheer performance boost it unlocked.", "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": "", "extra_scores": {}}, {"review_id": "2P0H0oPyGY", "reviewer": "Reviewer_tfEq", "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.", "questions": "* How big is the gap between the proposed approach and the highly-engineered SAT solvers?\n* What is $\\overline{E^L}$? How different is it from $E^L$?\n* 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?\n* 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?\n* What is the ratio between sat and unsat problems in the synthesized dataset? \n* 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?\n* (Minor) What is Res-Aided model (mentioned at the beginning of Section 8)? I find this terminology only there.", "limitations": "I think the limitations are discussed appropriately.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "+ The address problem, the unsatisfiability of propositional formulas, is a fundamental, important problem in computer science. \n+ Unifying resolution, a classic SAT solving algorithm, and attention-based neural networks.\n+ The paper considers extensive variants of the neural models and checks their experimental performance.\n+ It is experimentally demonstrated that the proposed approach outperforms the previous work, NeuroSat, and the expert iteration can shorten generated unsatisfiability proofs.", "weaknesses": "- 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.\n- Some aspects of the proposed approach and experiment design are unclear (see the below question).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your feedback and questions. Please find our responses to your questions below.\n\n> Q1: How big is the gap between the proposed approach and the highly-engineered SAT solvers?\n\n- Generally speaking, the main merit of our approach over traditional SAT solvers is its ability to capture deep insights into the underlying data distribution, which for instance, enables it to come up with far shorter proofs than the traditional solver with no extra supervision than the initial imperfect ground truth it. This is both an advantage over traditional solvers and traditional neural approaches that are limited by the quality of their initial labels. We mainly owe that to our sound-by-design resolution module that enables the network to safely (i.e., soundly) explore other viable solutions without distorting the semantics of the problem. That being said, these deep insights come at a cost of heavier computations involved in neural networks compared to traditional heuristic solvers.  For instance, on SR(40) data, it takes NeuRes an average of \\~45 ms (2.3 ms for sat and 88 ms for unsat) to solve an instance in our Python implementation while it takes \\~4 ms to solve it on a C implementation of the BooleForce solver. Different machinery (GPU for neural networks vs CPU for traditional solvers) make this comparison further complicated.\n\n> Q2: What is $\\overline{E^L}$? How different is it from $E^L$?\n\n- $\\overline{E^L}$ is mean of $E^L$ (i.e., mean literal embedding). $E^L$ is the matrix containing all literal embeddings of dimensions $m$x$d$ while $\\overline{E^L}$ is a vector of width $d$, where $m$ is the number of literals and $d$ is the embedding width.\n\n> Q3: 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?\n\n- We do not utilize this advantage in our implementation to get a direct comparison with the other two variants that only perform binary resolution. That being said, generalized resolution steps (involving a tuple of clauses) can always be easily broken into a sequence of binary resolution steps (involving pairs of clauses). However, we have not performed that experiment.\n\n> Q4: ...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..?\n\n- We previously performed several experiments in that direction where we tried supervising both positive and negative literals (and combining both losses with different aggregates: sum, min, & max) against the ground truth assignment. This surprisingly did not lead to an improvement compared to only supervising positive literals. At test time, however, we found using negative literals (in addition to the positive ones) sometimes produced satisfying assignments earlier. We do not have a precise account for this observation, but our best intuition attributed this result to the fact that the formula graph has no explicit notion of +ve and -ve literals per se, it's just a matter of which literal is connected/adjacent to which clauses (+ve and -ve literals are connected by a special edge). 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.\n\n> Q5: What is the ratio between sat and unsat problems in the synthesized dataset?\n\n- It's 50-50% across all training, validation, and test datasets to eliminate bias towards one class over the other.\n\n> Q6: What validation dataset is used?\n\n- For the UNSAT-only experiments (Section 6), we use a validation dataset containing 1K UNSAT formulas of the $SR(U(10, 40))$ distribution. For the full solver experiments (Section 7), we use a validation set of 2K formulas (1K SAT + 1K UNSAT) of the same distribution.\n\n> Q7: What is Res-Aided model?\n\n- The Res-Aided (i.e., Resolution-Aided) model refers to the full solver (SAT + UNSAT). The name is based on the rationale that the resolution head aids the assignment search for satisfiable formulas. (Res is usually used to refer to the resolution operator in the literature).", "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": "", "extra_scores": {}}, {"review_id": "pu0FYjiBGj", "reviewer": "Reviewer_hPQb", "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.", "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": "Yes, the authors adequately addressed the limitations and posed no negative societal impact.", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The approach proposed in the paper is novel, featuring a parallel mechanism for concurrently proving unsatisfiability and attempting to find a truth value assignment. This mechanism is expected to speed up the proving process significantly.\n- The three proposed attention variants each have distinct characteristics and are suitable for different situations. The expert iteration process effectively shortens the proof length.\n- The paper is well-written and easy to follow.", "weaknesses": "- 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.\n- 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your review and comments. Please find them addressed below.\n\n> 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.\n\n- It is true that in the paper, we focus on ablations regarding the clause-pair selection mechanisms (i.e., Casc-Attn, Full-Attn, Anch-Attn). The assignment decoder is kept simple on purpose: It is a small MLP, such that we can adequately assess the quality of the learned representations instead of the architecture. This is a quite common approach in the representation probing literature (e.g., \\[1\\], \\[2\\], \\[3\\]). Besides this, we preformed several ablation experiments that we are happy to include in an appendix to the final version of this paper. \n\n> Q1: Is there a comparison of the efficiency of the three different attention mechanisms as well as the baseline method (NeuroSAT)?\n\n- It depends on how you define efficiency. If you refer to the cost of a single forward pass through the model, then for a large enough problem size, Cascaded Attention should be the fastest followed by Anchored Attention then Full Attention. Our attention mechanisms do not directly compare to NeuroSAT since they are used for proving UNSAT which is not done by NeuroSAT (it's one of our contributions). \n- However, a more meaningful metric of efficiency should also take into account the number of steps (fwd passes) a clause selector needs to solve a given formula along with its success rate. As such, one way to compare the different attention mechanisms in terms of efficiency (on a formula distribution of size n) would be according to the following metric:\n  - $\\text{Efficiency} = (\\text{p-Len} \\* \\text{Success Rate}) / (\\text{time cost of a fwd pass})$\n  - For instance, on the $SR(U(10, 40))$ distribution, the efficiencies of our 3 attention mechanisms would be as follows:\n    - $E(\\text{Casc-Attn}) = (1.79 \\* 0.3733) / (1.5 ms) = 0.445$\n    - $E(\\text{Anch-Attn}) = (2.28 \\* 0.605) / (0.6 ms) = 2.299$\n    - $E(\\text{Full-Attn}) = (1.67 \\* 0.952) / (0.5 ms) = 3.1797$\n  - This means that for that particular distribution, Full-Attn is actually most efficient as the 2D attention grid is faster to compute than making two attention queries (as in Casc-Attn). However, that order of efficiency might vary for a different distribution.\n- For a general runtime breakdown comparison between NeuRes and NeuroSAT:\n  - For **predicting** SAT status, both models have the same runtime as they use the same message-passing GNN to obtain formula embeddings and the same voting MLP to get the SAT prediction.\n  - For **solving** SAT (i.e., with certificate/proof), the runtime depends on the instance size and SAT status as follows:\n    - **SAT**: the formula is solved when a satisfying truth assignment is found. In this case, the runtime is decided by two factors: \n      - #Attempts: Through our experiments, we show that NeuRes finds satisfying assignments to many more SAT instances after 1000 attempts. To see this, you can compare Figure 5 in our paper vs. Figure 5 in the NeuroSAT paper.\n      - The time cost of a single attempt: at any step, NeuRes extracts the full assignment in a single forward pass through a 2-Layer MLP over the literal embeddings. In contrast, NeuroSAT performs a k-means clustering on literal embeddings to separate them into two 2 clusters against a predicate. The latter is significantly more costly as it performs an iterative clustering process that could take hundreds of iterations to converge (the default limit is set to 300 iterations in the NeuroSAT implementation).\n    - **UNSAT**: the formula is solved when the model derives a full (resolution) proof of the empty clause (falsum) from it. Since NeuroSAT does not solve UNSAT formulas, a runtime comparison is not possible (UNSAT cores are not proofs). However, for a general idea, the NeuRes runtime in UNSAT cases depends on the number of resolution steps needed to derive the empty clause. In our evaluation, we've shown that NeuRes in many cases produces much shorter proofs than the teacher traditional solver, and on average to be around 1.15x in length. This is under our 1-step-per-forward-pass model. We thought that this arguably underutilizes our attention grid by only taking the top-1 clause pair, so we performed a side experiment in the rebuttals period to explore potential gains of taking the top 3 clause pairs at each step and perform them. The idea is to reduce the total number of forward passes to the model by performing more resolution steps per fwd pass. On SR(40) test data, this led to a 57.4% reduction in episode lengths (total number of forward passes), model proofs that are on average 43% shorter than the teacher's (p-Len = 0.57 vs the previous 1.15), in addition to a +1.7% total success/proof rate (99.9% vs the previous 98.2%). We intend to include this experiment in the main paper for the sheer performance boost it unlocks.\n\n**References:**\n\n\\[1\\] Akhondzadeh, Mohammad Sadegh, Vijay Lingam, and Aleksandar Bojchevski. \"Probing graph representations.\" International Conference on Artificial Intelligence and Statistics. PMLR, 2023.\n\n\\[2\\] Alain, Guillaume, and Yoshua Bengio. \"Understanding intermediate layers using linear classifier probes.\" arXiv preprint arXiv:1610.01644 (2016).\n\n\\[3\\] Pimentel, Tiago, et al. \"Information-theoretic probing for linguistic structure.\" arXiv preprint arXiv:2004.03061 (2020).", "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": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: 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.
Decision: Accept (spotlight)