Can Transformers Reason Logically? A Study in SAT Solving
Authors: Leyan Pan
Vijay Ganesh
Jacob Abernethy
Chris Esposo
Wenke Lee
Venue: ICML 2025 poster (2025)
Keywords: Transformers
Logical Reasoning
SAT-Solving
Primary area: theory->deep_learning
TL;DR: We theoretically show that Decoder-only Transformers can solve bounded 3-SAT instances with Chain-of-Thought

Abstract: We formally study the logical reasoning capabilities of decoder-only Transformers in the context of the boolean satisfiability (SAT) problem. 
First, we prove by construction that decoder-only Transformers can decide 3-SAT, in a non-uniform model of computation, using backtracking and deduction via Chain-of-Thought (CoT).
Second, we implement our construction as a PyTorch model with a tool (PARAT) that we designed to empirically demonstrate its correctness and investigate its properties.
Third, rather than \textit{programming} a transformer to reason, we evaluate empirically whether it can be \textit{trained} to do so by learning directly from algorithmic traces (``reasoning paths'') from our theoretical construction. The trained models demonstrate strong out-of-distribution generalization on problem sizes seen during training but has limited length generalization, which is consistent with the implications of our theoretical result.

Can Transformers Reason Logically? A Study in SAT Solving
Leyan Pan' Vijay Ganesh 1+
Jacob Abernethy
12* Chris Esposo' Wenke Lee
Abstract
This paper focuses on the deductive logical reasoning capa- bility of the Transformer model in restricted but simple and mathematically precise setting, namely, the Boolean sat- isfiability problem (SAT, Cook (1971)). We view deductive reasoning as the process of systematically drawing valid in- ferences from existing premises and assumptions. Boolean SAT solving captures the essence of deductive logical rea- soning because: 1) Boolean logic lies as the foundation of all logical reasoning, and 2) many modern SAT solvers are inherently formal deductive systems that implement the resolution proof system. Its NP-Completeness also necessi- tates multiple rounds of trial and error, which is critical for solving complex problems.
We formally study the logical reasoning capa- bilities of dlcoder-only Transformers in the con- text of the boolean satisfiability (SAT) problem. First, we prove by construction that decoder-only Transformers can decide 3-SAT, a non-uniform model of computation, using backtracking and de- duction via Chain-of- Thought (CoT). Second, we implement our construction a PyTorch model with tool (PARAT) that we designed to em- pirically demonstrate its correctness and inves- tigate its properties. Third, rather than program- ming transformer to reason, we evaluate em- pirically whether it can be trained do so by learning directly from algorithmic traces ("rea- soning paths") from our theoretical construction. The trained models demonstrate strong out-of- distribution generalization on problem sizes seen during training but have limited length generaliza- tion, which is consistent with the implications of our theoretical result.
We prove by construction that decoder-only Transformers can decide 3-SAT instances with CoT (in a non-uniform computational setting):
Theorem 1.1 (Informal version of Theorem 4.5), For any P.C E N there exists a decoder-onts Transformer with Olp²) parameters that can decide all 3-SAT' instances of at most p variables and clauses using Chain-of- Thoough......
The "non-uniform" nature of this result means that the Trans- former's parameters are dependent on the problem size (p), in contrast to single, universal model that handles arbi- trary input lengths. An insight from our construction is that this practical difficulty in achieving length generalization stems from numerically approximating precise attention pat- terns with softmax, where errors can compound on larger instances and affect performance (Figure 5). This provides theoretical explanation for the length generalization limi- tations observed when training L.MSs reasoning tasks.
1. Introduction
Transformer-basee large language models (LLMs, Vaswani et al. (2017)) have demonstrated strong performance on tasks that seem to demand complex reasoning, especially with Chain-of-Thought (Co'T, Wei al. (2022); OpenAl (2024); DeepSeek-AI et al. (2025)). However, they of- ten face challenges in reliable multi-step logical reasoning, hallucinating logically flawed or factually incorrect con- clusions. Consequently, many researchers reject the idea that LLMS can reason (Kambhampati et al., 2024), and re- searchers continue to disagree on the precise definition of "reasoning" in the context of LLMs. Furthermore, there is little understanding of the fundamental limitations of the reasoning capabilities of Transformer models.
We illustrate the CoT our construction uses to solve 3-SAT instances in Figure 1. The Transformer model simulates log- ical assumption, deduction, and backtracking by generating new tokens and ultimately outputs a SAT/UNSAT label as the result of the 3-SAT decision problem. Our theoretical construction shows that, for any chosen instance size, stan- dard softmax-attentinn Transformer with size-dependent parameters can decide 3-SAT, requiring only single for- ward pass to perform logical deduction over all clauses under the current variable assignments (see Lemma 4.8).
'Equal contribution 'College of Computing, Georgia Institute of Technology, Atlanta, GA, USA 'Google Research, Atlanta, USA. Correspondence to: Leyan Pan <leyanpan eaaaapaan@aatccccuuu..u. gatcch.edu>.
Proceedings of the 4nnd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).
To empirically verify and investigate our construction, we design tool (PARAT) that instantiates the weights of Trans-

---

Can Transformers Reason Logically? A Study in SAT Solving
Model Input (3-SAT formula)
(-2 V -4 V -
(T3 V J44 V -I1)
(-21 V J3 -22)
(0) V 22 x44)
(~244 V 82 21)
(x1 V x2 Vz4)
Transformer Chain-of- Thought from Theorem 4.5
Model Output typewri ter font
Assume 22
T
Assume 211
Deduce 244
Deduce 13
Conflict
Assume
Assume
4
BrckTrack
Keep 3/2
Learn 21
Deduce 24 =
Conflict Again
Assume 2
-1
-4
BackTrack
Learn W2 F
Assume w3
T
Assume 24 =
Deduce i1
T
Solved!
-2
Assume 3
Assume
SAT
Figure 1. Visualization of the Chain-of-Thoughl (CoT) process used by model solve example 3-SAT formula deseribed in Theorem 4.5. The model autonomously performs trial-and-emoo reasoning, making multiple attempts and backtracking upon encountering conflicts. Here, T represents True and represents False. Tokens in typewriter font denote the CoT generated by the model.
former models based on NumPy code specifying the desired behavior. With PARAT, we implemented the construction PyTorch Transformer model and empirically validated its correctness on random 3-SAT instances.
style code. We empirically demonstrate that the instantiated Transformer corresponding our theoretical construction can perfectly solve 3-SAT instances.
Finally, our supporting training experiments suggest that training on our theoretical CoT of 3-SAT reasoning traces allows Transformer models to achieve -fitt--diistibution generalization within the same input lengths, but fail to generalize to larger instances.
Additionally, we perform training experiments to demon- strate that Transformers can effectively learn from the de- ductive reasoning and backtracking process encoded as CoT. We show that trained Transformer models can generalize be- tween SAT instances generated from different distributions within the same number of variables p. However, LLMs trained on SAT instances with CoT still struggle to solve instances with an unseen number of variables, demonstrat- ing limitations in learning geggh-generalizblle reasoning. These experimental results support our theoretical predic- tions.
2. Related Work
Transformers and P and P/poly Problems. This line of research focuses on what types of computation can Trans- former models simulated by providing theoretical construc- tions of Transformer models that can solve well-defined computational problems. The seminal work of Liu al. simulate semiau-
Contributions First, prove by construction that in non-uniform model of computation, decoder-only Trans- formers can decide 3-SAT using backtracking and deduction via Chain-of-Thought (CoT)) We show that Transformers can perform logical deduction on all conditions (clauses) in parallel instead of checking each condition sequentially. Nevertheless, the construction requires exponentially many CoT steps in the worst case, implied by the NP-hardness of SAT, although it requires much fewer steps in most in- stances.
(2023a) showed that Transformers tomata using single pass over only logarithmic number of layers w.r.t. the number of states. Yao et al. (2021) demon- strated that transformers can perform parentheses matching of most & types of parentheses and D appearance of each (Dyck,, with + layers.
However, the computation power of pass of the Trans- former model is fundamentally limited (Merrill et al., 2021; Merrill & Sabharwal, 2023), and the success of Chain-of- Thought (CoT) reasoning has sparked research on how CoT can improve upon the expressiveness of Transformer models. Pérez et al. (2019) proved that Transformers can emulate
We design PARAT, a tool to instantiate Transformer model weights that implement specifications written in NumPy-
2

---

Can Transformers Reason Logically? A Study in SAT Solving
the execution of single-tape Turing machines. Giannou al. (2023) showed that Transformers can recurrently simulate arbitrary programs written in one-instruction-set language. Li et al. (2024) proved that Transformers can simulate arbi- trary boolean circuits using CoT by representing the circuit in the positional encoding. In particular, transformers can decide all problems in P/poly 2 P with polynomial steps of CO Merrill & Sabharwal (2024) showed that Transform- ers with saturated attention can decide all regular languages with a linear number of CoT tokens and decide all prob- lems in P with polynomial number of CoT tokens. (Feng et al., 2023) shows that Transformer CoT can perform inte- ger arithmetic, solve linear equations, and perform dynamic programming for the longest increasing subsequence and edit distance problems.
Hazra et al. (2024) investigates pretrained LLM's capabil- ity of solving SAT instances from the perspective of phase transitions.
A related line of work uses formal symbolic logic to enhance the capabilities of LLMs with Co'.. LogicIM (Pan et al., 2023) and SymbCoT (Xu et al., 2024) integrate symbolic expressions of first-order logic with CoT prompting and invoke solvers to provide feedback the LLM reasoner. Ryu et al. (2025) uses divide and conquer to improve upon the above works in terms of translation accuracy. Jha et al. (2024) uses symbolic logic solvers to provide reinforcement learning rewards to improve LLM reasoning. Beyond LLMs, NeuroSAT (Selsam et al., 2019), MatSAT (Sato & Kojima, 2021), and SATformer (Shi et al., 2022) train different neu- ral networks to learn SAT-solving.
How our work differs. We focus on 3-SAT, which is NP- NP-complete problem. It is widely believed that P is strict subset of NP, and it is not known whether NP is subset of P/po p/poly. In other words, our results are not comparable to these earlier results.
How our work differs. Our work focuses on the theoretical capabilities of Transformer models rather than practical pretrained LLMs and can be viewed as building a theoretical foundation for these results.
Compilation of Transformer Weights. Further, prior work on the theoretical construction of Transformer models rarely provides practical implementations. Notably, Giannou et al. (2023) provides implementation of their Transformer construction and demonstrates its execution on several pro- grams. However, the model is initialized "manually" us- ing prolonged sequences of array assignments. Lindner et al. (2023) released Tracr, which compiles RASP (Weiss et al., 2021) programs into decoder-only Transformer mod- els. RASP is human-readable representation of a subset of operations that Transformers can perform via self-attention and MLP layers. While having related functionalities, our tool has different goals than Tracr and bears multiple prac- tical advantages for implementing complex constructions, which we detail in Appendix D.2.
Turing Completeness of Transformers. Meanwhile, Pérez et al. (2019), Li al. (2024), and Merrill & Sabharwal (2024) also showed that Transformers can simulate single- tape Turing Machines (TM) with CoT and can theoretically be extended to arbitrary decidable languages. However, these constructions require at least one CoT token for every step of TM execution.
How our work differs. Our theoretical construction demon- strates that, for certain classes of formal reasoning problems, Transformers can simulate algorithmic reasoning traces at an abstract level with drastically reduced number of CoT tokens compared to step-wise emulation of a single-tape TM. At each CoT step, our construction performs deductive reasoning over the formula in parallel while any single-tape TM must process each input token sequentially. Further- more, the CoT produced by our theoretical construction abstractly represents the human reasoning process of trial and error, as demonstrated in Figure 1.
3. Preliminaries
This section reviews the Boolean Satisfiability (SAT) prob- lem, 3-SAT, and the classical DPLL search procedure. We provide a brief overview of the important notations used in this work. For a more detailed introduction to SAT-solving, we recommend to interested readers the first chapters of (Biere et al., 2009). We assume familiarity with the high- level components of Transformer models. For details on the mathematical model for Transformers used in our thcoretical results, please refer to Appendix C.I.
Formal Logical Reasoning with LLMS Several studies also evaluate pretrained LLMs' formal and algorithmic rea- soning abilities, finding that they perform well on few reasoning steps but struggle as the required steps increase. ProofWriter (Tafjord et al., 2021), ProntoQA (Saparov & He, 2023; Saparov et al., 2023). FOLIO (Han et al., 2024), Simplel (Zhang et al., 2023b), and RuleTaker (Clark et al., 2021) encodes formal logical reasoning as natural language problems to test general purpose LLMs on multi- step reasoning. NPHardEval (Fan et al., 2024) compiles a benchmark of P and NP-Hard problems and tests a variety of pre-trained LLMs. Liu et al. (2023b) evaluates code exe- cution capabilities, Chen et al. (2024) measures capabilities to solve propositional and first-order logic satisfiability, and
3.1. Boolean Satistiability (SAT) in Conjunctive Normal Form (CNF)
Let Var (#1,... vpp} be set of Boolean variables. A literal is either a variable x. or its negation ~wy The set of
3

---

Can Transformers Reason Logically? A Study in SAT Solving
all 2p literals is denoted
3.4. The DPLL Search Procedure
L = -2,, Tp. [.pp
The Devis-Putaan-Leggmann---ovvvdad
(DPLL) algo- rithm is complete, backtracking SAT-solving procedure, Starting from CNF formula F and the empty assignment 0, at any moment it maintains a partial assignment A and the reduced formula FlA. The main operations are
finite disjunction ("OR") literals, written C (&1 V ... V Ex). A formula in conjunctive normal form (CNF) is conjunction ("AND") of clauses
clause C' C
F = C GACCA.--AC.
Decision: Choose an unassigned variable zy and tentatively set it to either True or Fal se; record the choice so can be undone later.
An assignment C L is any set of literals that does not contain both 2y and -. Intuitively Iy E A means Ty True and -T A means 2e False. A clause C is satisfied by A (denoted A C) c + Ø; a CNF formula F' is satisfied by assignment A if every clause is satisfied by A. The SAT problem asks whether a satisfying assignment exists for a given F.
Unit Propagation: Repeatedly adds forced literals from unit clauses of A to A.
Conffict/Bactrack: an empty clause appears, undo deci- sions chronologically until a new value can be tried; none remain, the instance unsatisfiable.
3-SAT. In 3-SA7' each clause contains at most three literals. 3-SAT NP-complete; it is the canonical hard case for SAT and is the focus of our work.
The procedure terminates when either all clauses satis- fied (SAT) conflict arises at the root level (UNSAT).
3.2. DIMACS Encoding
3.5. Notation Used in Later Sections
To represent 3-SAT formulas as a sequence of tokens to Transformer models, adopt the standard DIMACS format. Each literal is encoded as integer: v for 2i, and -v for -.. Clauses are sequences of integers terminated by 0. For example
We summarise the symbols that re-appear in the theoretical part of the paper:
P G
{I.... .P), index set of variables.
i-th clause in a CNF formula.
(11 V -x2)
(-z1 V 12 V -33)
F - C.
CNF formula with c clauses.
is written
ACL
partial assignment (no complementary literals).
1
2
1 2 33
FlA
reduction of F by (definition above).
with an initial [BOS] and a closing [SEP] token in our model implementation.
A - F
A satisfies F.
F -A FAAHL
F contradicts A (empty clause in Fla).
l is forced by unit propagation.
3.3. Partial Assignments and Formula Reduction
These notations are used verbatim in Section 4.
SAT solving reason with partial assignments that leave some variables unassigned. Given a CNF and a partial assignment A, the reduction of by dedenoed Fla-is obtained in two steps:
4. Transformers and SAT: Logical Deduction and Backtracking
Delete satisfied clauses: remove any C, with C2 A * Ø.
This section presents and explains our main results Trans- formers' capability in deductive reasoning and backtracking with COT. To rigorously state our results, we first formally define decision problems, decision procedures, and what means for a model to "solve" a decision problem using CoT:
Delete falsified literals: from each remaining clause delete any literal that is false under A (e.g. delete - if Ir E A).
clause becomes empty, the entire formula unsatisfi- able under A. unit clause is a clause with exactly one literal after reduction; its lone literal must be true in every extension of A.
Definition 4.1 (Decision Problem). Let V be a vocabulary, > S V be an alphabet, L C > be set of valid input strings. We say that a mapping L - {0, 1) is decision problem defined on L.
Example. Let
F (xn V x22 A (-2n 22) A (x2V -a), A= (.)).
Definition 4.2 (Decision Procedure). We say that an algo- rithm A is a decision procedure for the decision problem f. if given any input string from L, A halts and outputs 1 if f(z) 1, and halts and outputs 0 if f(z) O.
After Step 1 the first clause is deleted (already true). Step 2 removes - from the second clause, giving the unit clause (xa). Hence FlA+ = (as) A (x2 V -xy) and 23 is forced true by unit propagation.
Definition 4.3 (Autoregressive Decision Procedure). For

---

Can Transformers Reason Logically? A Study in SAT Solving
any map M : V V. which we refer an aulo- regressive next-token prediction model, and {Eo,&) V. define procedure Aar,g follows: For any input 81m. run Algorithm 1 with M and stop tokens & AMrs outputs O if 81:: ends with Eg and AM,E output otherwise. We say M autoregressively decides decision problem f if there is
E, Emoc-talses Eassigned B R2p encodes B
F(B),, 1: EB
E(B) (-z.)EB-
foot- (B) == (-wx) Enot-false BB)bp= == 2.
Passigned B)v Fassiigne B B))pp= = BBEBV(T
some & C for which AM,E decides f.
Of the above encodings, E(B is calculated by using self- attention layers to sum up one-hot token representations within clause/partial assignment, while both faoe and Eussigned (B) can be computed via affine transforma- tion on E(B).
Definition 4.4 (3-SATp.c) p.c) Let DIMACS(p,c) denote the
set of valid DIMACS encodings of 3-SAT instances with at most variables and с clauses with a prepended [BOS] to- ken and an appended [SEP] token. Define 3-SAT p.c.
(IM + {0, 1} as the problem of deciding whether the 3-SAT formula, encoded via DIMACS(p. c), is satisfiable.
Step 2: Parallel logical operations over all clauses.
We now show that the core logical operations of DPLL SAT solving can be computed using vector operations on the en- coding the clauses [CI...., Ce} and a partial assignment A over all clauses in parallel, capability of Transformers that allows efficient logical reasoning over long contexts:
With the above definition, we present the formal statement of our main result:
Theorem 4.5 (Decoder-only Transformers solve SAT). For any p, E N+, there exists a Transformer model M V + V that autoregressively decides 3-SAT, p.c. in no more than 2 CoT iterations. M requires L = - layers, H = heads, demb= = (p), and O(p²) parameters.
Lemma 4.7. Let F Nieta C₁ be 3-SAT formula over p variables {ai...., Fpp and e clauses (Ci...., Cel- Let A C L be a partial assignment defined variables (Ii,-.., then the following properties hold:
Remarks Theorem 4.5
1. Satisfiability Checking:
A
min E(C,) E(A) 1.
Despite the high upper bound on CoT length, it's rarely reached in practice. In Figure we show that the CoT length is no greater than 8y 20.05p for most formulas
XE(c
2. Conflict Detection:
F F
min E(C:) Enox (A) = O. RE(0]
The worst-case CoT length is independent of the num- ber of clauses c, which is due to the parallel deduction over all clauses within the Transformer construction.
Deduction:
Let D = (1 E I F = 1} be the
literals deducible from F' given via unit propagation. Then can write E(D)
Positional encodings are not included in the number of parameters. The positional encoding at position is the numerical value at particular dimension.
max
min Σ
(E(C)) Ena (A)=1},
xE(c]
Each param. can be represented with O(p + loge) bits
Fmssigneal (A), 0).
Proof Sketch We show our full construction and proof via
where max and min are applied element-wise
simulation of the abstract DPLL (Nicuwenhuis et al., 2005) in Appendix C. The construction uses adapted versions of
Each of the above operations can be approximated by an attention head when given the clause and partial assignment encodings. We capture this idea in the following lemma:
lemmas from Feng et al. (2023) as basic building blocks. Here provide proof sketch of the core steps and opera- tions in our theoretical construction.
Lemma 4.8 (Parallel Processing of Clauses, Informal). Let F' be a 3-SAT formula over variables { vp with e clauses {CI,..., C.} and A partial assignment defined variahles (I1,...,22 Fpp. Let
Step I: Summarize clauses and assignments as binary vectors The Transformer first converts every clause C; and the evolving partial assignment A into the binary encodings of Definition 4.6 (see 2)..2). These vectors are obtained inside the model by summing the one-hot literal embed- dings between two separator tokens; wording inside the definition is changed.
E(C,)
X Xencoding
: :
((c+2))(2p+2)
E(C.)
0
E(A)
0 1
Definition 4.6 (Encoding of clauses and partial assign- ments, extending Sato & Kojima (2021)). The mappings
Then for any > given X as input, there exists:
5

---

Can Transformers Reason Logically? A Study in SAT Solving
Clause
Partial Assignment
(~I2 V D4 V -I
21
24
10
0
0
0
0
11
[1
1
0
0
0
0
1]
22
222
103
244
222
22
Figure Illustration of E(C) and E(A) with p
An attention head that outputs AA=F with approxima- tion error bounded by
A specification "program" in PARAT is composed of linear sequence of statements (i.e., no control flow such as loops or branching based on PARAT variable values is allowed), where each statement assigns the value of an expression variable. Let v_1, v_2, denote PARAT variable names. Each statement involving PARAT variables must be one of the following: (1) Binary operations such as v-1 + v-2, v-1 v-2, V-1 v.2; (2) Index opera- tions such as v_1 [v_2, :] or v_1[;, start: ), where st start, predefined library of functions that take PARAT variables as input.
An attention head that outputs 1 1rF with approxi- mation error bounded by
An attention head followed by an MLP layer that out- puts D(D as defined Lemma 4.7 with lloc error bounded by e, unless F -A
All weight values are independent of F and A and are bounded by ((poly(p.c, log((1))))
[d. or (3) Function calls from a
Step 3: Predicting the Next Token Fach of the above results is stored in the hidden state vectors (i.e., residual stream (Elhage et al., 2021)) of the Transformer model. In the final layer, the prediction of the next token is deter- mined by series of conditionals based on priority: If A }= F, then the next token is SAT. Otherwise, if F } -A, output UNSAT if A contains decision literals and output [BackTrack] otherwise, etc. Collectively, the token pre- dictions ensure that, when running Algorithm the result- ing transition from a1.t to 81.++11 every timestep emulates the abstract DPLL state transition system (Nieuwenhuis et al., 2005) and thus ensures that the procedure correctly decides 3-SAT. (See Appendix C.8.1 for details)
P PARAT takes in specification program well as variable out of dimension V (size of vocabulary) and outputs PyTorch Module object that implements a Transformer model as defined in Section 2. The following condition is satisfied: For any possible input sequence of tokens s in the vocabulary of length n, the token predicted by the Transformer model the same as the token corresponding to out [-1, : argmax () (i.e., the token prediction the last position) when interpreting the specification using the Python interpreter with the NumPy library. We provide more details on our tool and the supported operations in section Appendix D.
5.1. Analysis of the Transformer Construction
5. Implementing the Construction with PARAT
With our tool, we successfully implemented our theoretical construction Theorem 4.5 using the code in Appendix D as PyTorch model. We will refer to this model as the "compiled" model for the rest of the section. With concrete implementation of our theoretical construction in Py Torch, empirically investigate 3 questions (1) Does the compiled model correctly decide SAT instances? (2) How many steps does the model take to solve actual 3-SAT instances? (3) How does error induced by soft attention affect reasoning accuracy?
In the previous section, we presented theoretical construc- tion of Transformer capable of solving SAT instances. However, it can be difficult to gain insights and fully verify its correctness without experimental interactions with the construction. To help address this, we introduce PARAT (short for ArrametricTransfrmmet former weights based on high-level specifications written as NumPy code performing array operations.
which instantiates Trans-
Both PARAT and the specification it accepts based Python, and the syntax of the PARAT is restricted subset of Python with the NumPy library. Every variable i PARAT a 2-D NumPy array of shape n x d_v, where n denotes the input number tokens and d.v is the dimension of the PARAT variable v, which can be different for every variable.
Evaluation Datasets We evaluate our models on randomly sampled DIMACS encoding of 3-SAT formulas. We focus SAT formulas with exactly 3 literals in each clause, with the number of clauses e between 4.1p and 4.4p, where is
6

---

Can Transformers Reason Logically? A Study in SAT Solving
the number of variables.
degrade significantly on larger ones. This matches the com- monly observed limitation in length generalization when training on smaller problem instances.
It is well-known that the satisfiability of such random 3- SAT formulas highly depends on the clause/variable ratio, where formula is very likely satisfiable if c/p < 4.26
and unsatisfiable if c/p > 4.26 (Crawford & Auton, 1996). This potentially allows a model to obtain high accuracy just by observing the statistical properties such as the c/p ratio. To address this, we constrain this ratio for all formulas to be near the critical ratio 4.26. Furthermore, our "marginal" datasets contain pairs of SAT vs UNSAT formulas that differ from each other by only single literal. This means that the SAT and UNSAT formulas in the dataset have almost no statistical difference in terms of c/p ratio, variable dis- tribution, etc., ruling out the possibility of obtaining SAT vs UNSAT information solely via statistical properties. We also use 3 different sampling methods to generate formulas of different solving difficulties to evaluate our model:
6. Can Transformer Learn SAT Solving?
Our previous sections showed that Transformer and weights exist for solving SAT instances using CoT with backtrack- ing and deduction. However, it is unclear to what extent Transformers can learn such formal reasoning procedures by training on SAT formulas. Previously, Zhang et al. (2023a) showed that when using a single pass of a Transformer model (without CoT), Transformers fail to generalize to logical puzzles sampled from different distributions even when they have the same number of propositions.
This section provides proof-of-concept evidence that train- ing the CoT procedure with deduction and backtracking described in Figure can facilitate out-of of--distributiinn gen- eralization within the same number of variables.
Marginal: Composed of pairs of formulas that differ by only one token.
Datasets In Section 5.1 we introduced different distribu- tions over random 3-SAT formulas of varying difficulties. For training data, we use the same sampling methods, but in- stead of having a separate dataset for each variable number p. we pick 2 ranges p E [6, 10] and p E [11, 15), where for each sample random p value is picked uniformly random from the range. Each formula with p variables contains 16.4p to 17.6p tokens. This results in 2 x 3 training datasets, each containing 5 x 100 training samples', with balanced SAT vs UNSAT samples. For each formula, we generate the corresponding CoT in the same format as Figure using custom SAT Solver. The evaluation data is exactly the same as Section 5.1.
Random: Formulas are not paired by differing tokens and each clause is randomly generated.
Skewed: Formulas where polarity and variable sampling are not uniform; for each literal, one polarity is preferred over the other. Some literals are also preferred over others.
We generate the above 3 datasets for each variable number 4 S p S 20, resulting in 51 total datasets of 2000 samples each. Each sample with p variables contains 16.4p to 17.6p input tokens, which is at least 320 for p 20.
Model Unless otherwise stated, the model we experiment with is compiled from the code in D.4 using PARAT with max number of variables p = 20, max number of clauses c= 88, and exactness parameter 3 = 20. The model uses greedy decoding during generation.
Model and Training We use the LLaMa (Touvron et al., 2023) architecture with 70M and 160M parameters for the training experiments. We compute cross-entropy loss on every token in the CoT but not the DIMACS encoding in the prompt tokens. We provide further training details in Appendix A. We also permute the variable IDs for training samples to ensure that the model sees all possible input tokens for up to 20 variables.
Accuracy Our compiled model achieves perfect accuracy on all evaluation datasets described above. This provides empirical justification for our theoretical construction for Theorem 4.5 as well as PARAT. This result is included in Figure to compare with trained models.
How many steps? For all formulas we evaluated, the max- imum CoT length is bounded by 8p- 20.08p, which is sig- nificantly less than the theoretical bound of p 20++1), This indicates that the model can use deduction to reduce the search space significantly. See appendix Figure 4.
Evaluation Criteria We evaluate our model using two criteria: SAT/UNSAT accuracy and full trace correctness. SAT/UNSAT accuracy evaluates the model's binary predic- tion based on the first token in {SAT, UNSAT) generated by the model, compared against the ground truth satisfiability of the formula. If the model fails to generate (SAT, UNSAT} within the context length, the prediction is considered incor- rect, which can cause accuracy to drop significantly below 50%. Full trace correctness checks if every token gener-
Effect of Softmax Attention In our previous evaluations, we used a sufficiently large scaling factor 3 to ensure that the approximation error from the softmax is bounded and does not affect the final token output. In Figure 5 we show that, with an insufficient scaling factor, the compiled model would achieve perfect accuracy on smaller instances but
'The number of training samples is negligible compared to the total number of possible formulas. There are more than p 12p 3-SAT formulas with p variables, which is > 1006 for p 6
7

---

Can Transformers Reason Logically? A Study in SAT Solving
p E [6, 10]
E [11,
Marginal
Random
Skewed
Marginal
Random
Skewed
Marginal 99.88%
99.99%
99.99%
99. 99.82%
99.89%
99.81 %
SAT vs UNSAT
Random
99.96%
100.00%
100.00%
99.1 1%
99.75%
99.55%
Skewed
99.96%
100.00%
99.99%
99.41%
99.74%
99.48%
Marginal 98.50%
97.33%
88.72%
98.66%
97.57%
86.06%
Full Trace Correct
Random
99.40%
99.04%
93.12%
98.56%
97.99%
91.70%
Skewed
99.38%
99.16%
97.72%
97.02%
95.98%
91.51%
Table Average accuracics (%) of SAT/UNSAT prediction and full trace accuracy for models trained and tested different datasets in the training regime for number of variables [6, 10) and p E (11, 15). Columns denote train datasets, and rows denote test datascts. Each accuracy is computed over 10000 total samples.
Daraser
00
Triiiing Regine
Trshing Regine
0,10 Maawer UNGATT
20
mener (ST UESAT)
13 pooeet ESAT (ISSST)
16, raag
10 drowe (ul)
11 nunders Fall
Figure 3. Result of the Length generalization experiments, showing SAT/UNSAT prediction accuracy (solid) and full trace accuracy (opaque, dashed) Transformer models trained on the marginal, random, and skewed dataset with CoT on the marginal dataset over 4-20 variables. Left: model trained 6-10 variables. Right: model trained on 11-15 variables. Compiled refers the compiled model corresponding to our theoretical construction described in Section 5.1.
ated by the model adheres to the abstract DPLL procedure (Definition C.13) under our CoT definition. While strict, the "correct" CoT is not unique since the model may freely choose variable assignment and deduction orders.
experiments suggest that the LLM have very likely learned logical reasoning procedures using CoT that can be applied to all formulas with the same number variables as the data they are trained on.
6.1. Intra-length OOD Generalization
6.2. Limitations Length Generalization
Our first set of experiments evaluates the model's perfor- mance on SAT formulas sampled from different distribu- tions from training, but the number of variables in formulas remains the same (p [6, 10] and [11, 15] for both train and test datasets).
The second experiment evaluates the model's ability to gen- eralize to formulas with a different number of variables than seen during training. We use the model trained 3 data dis- tributions described in section 6. and evaluate the marginal dataset with 4-20 variables, with 2,000 samples each. For this experiment, we evaluate the accuracy of the binary SAT vs UNSAT prediction.
As shown in Section 5.1, our trained models achieve near- perfect SAT vs ANSAT prediction accuracy when tested on the same number of variables as the training data, even when on formulas sampled from different distributions. The model also strictly follows correct reasoning procedure for most samples. Recall that the "marginal" dataset has SAT vs UNSAT samples differing by single token (out of at least 16p tokens in the input formula), which minimizes statistical evidence that can be used for SAT/UNSAT prediction. Our
Results In Figure 3, our results indicate that performance degrades drastically beyond the training regime when the number of variables increases. This shows that the model unable learn general SAT-solving algorithm that works for all inputs of arbitrary lengths, which corroborates our theoretical result where the size of the Transformer for SAT. solving depends on the number of variables.
8

---

Can Transformers Reason Logically? A Study in SAT Solving
Acknowledgements
URL
http://wwww.cicccdddieeee com/ httpce//rr..ccceee////o///..
This material is based upon work supported by the National Science Foundation under grant no. 2229876 and is sup- ported in part by funds provided by the National Science Foundation, by the Department of Homeland Security, and by IBM. Any opinions, findings, and conclusions or rec- ommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation or its federal agency and in- dustry partners. This work is supported by NSF award CCF-2403391, The authors thank Hassan Naveed for his exploratory work on using RASP for SAT-solver implemen- tation, William Armstrong for suggesting the abstract DPLL paper and contributing code, and Jintong Jiang for providing suggestions on the paper's ' presentation and writing.
Frontiers in Problem Solving: Phase Transitions and Complexity.
DeepSeek-AI, Guo, D., Yang, D., Zhang, H., Song, J., Zhang, R., Xu, R., Zhu, Q. Ma, S., Wang, P. Bi, X., Zhang, X., Yu, X., Wu, Y., Wu, Z. F,, Gou, Z., Shao, Z., Li, Z., Gao, Z., Liu, A., Xue, B., Wang, B., Wu, B., Feng, B., Lu, C.,, Zhao, C., Deng. C., Zhang, C.,, Ruan, C., Dai, D., Chen, D., Ji, D., Li, E., Lin, F., Dai, F., Luo, F. Hao, G., Chen, G., Li, G., Zhang, H., Bao, H.,, Xu, H., Wang, H., Ding, H., Xin, H., Gao. H., Qu, H., Li, H., Guo, J., Li, J., Wang, J., Chen, J., Yuan, J., Qiu, J., Li, J., Cai, L., Ni, J., Liang, J., Chen, J., Dong, K., Hu, K., Gao, K., Guan, K., Huang, K., Yu, K., Wang. L.,, Zhang, L., Zhao, L.,, Wang, L.,, Zhang, L., Xu, L., Xia, L., Zhang, M., Zhang, M., Tang, M., Li, M., Wang. M., Li, M., Tian, N., Huang, P., Zhang, P.. Wang, Q. Chen, Q. Du, Q. Ge. R., Zhang, R., Pan, R., Wang, R., Chen, R. J., Jin, R. L., Chen, R., Lu, S., Zhou, S., Chen, S., Ye, S. Wang, S., Yu, S., Zhou, S., Pan. S., Li, S. S., Zhou, S. Wu, S., Ye, S., Yun, T., Pei, T., Sun, T., Wang, T, Zeng, W., Zhao, W., Liu, W., Liang, W., Gao, W., Yu, W., Zhang, W., Xiao, W. L., An, W., Liu, X., Wang, X., Chen, X., Nic, X., Cheng, X., Liu, X., Xie, X., Liu, X., Yang, X., Li, X., Su, X., Lin, X., Li, X. Q., Jin, X., Shen, X., Chen, X., Sun, X., Wang, X., Song, X., Zhou, X., Wang, X., Shan, X., Li, Y. K., Wang, Y. Q.. Wei, Y. X., Zhang, Y., Xu, Y., Li, Y., Zhao, Y., Sun, Y., Wang, Y., Yu, Y., Zhang, Y. Shi, Y., Xiong, Y., He, Y., Piao, Y., Wang. Y., Tan, Y., Ma, Y., Liu, Y., Guo, Y., Ou, Y., Wang. Y., Gong, Y., Zou, Y., He, Y., Xiong, Y., Luo, Y., You, Y., Liu, Y., Zhou, Y., Zhu, Y. X., Xu, Y., Huang, Y., Li, Y., Zheng, Y., Zhu, Y., Ma, Y., Tang, Y., Zha, Y., Yan, Y.. Ren, Z. Z., Ren, Z., Sha, Z., Fu, Z., Xu, Z., Xie, 2., Zhang, Z., Hao, Z. Ma. Z., Yan, Z., Wu, Z., Gu, Z., Zhu, Z., Liu, Z., Li,
Impact Statement
This paper presents work whose goal is advance the field of Machine Learning. There are many potential societal consequences of our work, none of which we feel must be specifically highlighted here
References
Biere, A., Heule, M., van Maaren, H., and Walsh, T. (eds.). Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applica- tions. IOS Press, 2009. ISBN 978-1-58603- 929-5. URL http: / http//apppppppttieeeeee uni-trier weriiirree/deee de/db/ series/faia/ fataaa/faaal85.. html.
Chen, M., Li, G., Wu, L.-I,, Liu, R., Su, Y., Chang, X., and Xue, J. Can language models pretend solvers? logic code simulation with 1lm.. In International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, pp. 102-121. Springer, 2024.
Z. Xie, Z., Song. Z., Pan, Z., Huang, Z., Xu, Z., Zhang, Z.,, and Zhang, 7. Deepseek-rl: Incentivizing reasoning capability in llms via reinforcement learning, 2025. URL https:/ / /aa/ariivvoooo .rg abs/ 2501 12948
Clark, P., Tafjord, O., and Richardson, K. Transformers as soft reasoners over language. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI'20, 20, 2021. ISBN 9780999241163 165.
Elhage, N., Nanda, N., Olsson, C., Henighan, T., Joseph, N., Mann, B., Askell, A., Bai, Y., Chen, A., Conerly, T., DasSarma, N., Drain, D., Ganguli, D., Hatfield- Dodds, Z., Hernandez, D., Jones, A., Kernion, J., Lovitt, L.. Ndousse, K., Amodei, D., Brown, T., Clark, J., Kaplan, J., McCandlish, S., and Olah, C. A math- ematical framework for transformer circuits. Trans- former Circuits Thread, 2021. https://tansformer
Cook, S. A. The complexity of aecorem-proving proce- dures. In Harrison, M. A., Banerji, R. B., and Ullman, J. D. (eds.), Proceedings of the 3rd Annual ACM Sympo- sium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA. pp. 151-158. ACM, 1971. doi: 10.11455800157.8000447 URL https: www..oorgg......ooo 10. 00044//800157 8C50047
Crawford, J. M. and Auton, L. D. Experimental results on the crossover point in random 3-sat. Artificial
Fan, L., Hua, W., Li, L.,, Ling, H., and Zhang, Y. NPHardE- val: Dynamic benchmark on reasoning ability of large lan- guage models via complexity classes. In Ku, L.- W., Mar-
Intelligence, 81(1):31-57, 1996. ISSN 0004-3702. doi: hutps///ooi.or//0. wttp:///ooo0000000000/0000000000

---

Can Transformers Reason Logically? A Study in SAT Solving
tins, A., and Srikumar, V. (eds.), Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 4092-41 14, Bangkok, Thailand, August 2024. Association for Com- putational Linguistics. doi: 10. 10.16653/w//20224a2-longg
Li, Z., Liu, H., Zhou, D., and Ma, T. Chain of thought em- powers transformers solve inherently serial problems. In The Twelfth International Conference Learning Representations, 2024. URL https: /ttp::://ppezevier. net/ forum? d= 3 9MTM.
225. URL https: http://aaaaoollooorrgg////////// acl 1ong.lon.... 225/.
Lindner, D., Kramar, J., Farquhar, S., Rahtz, M., McGrath, T., and Mikulik, V. Tracr: Compiled transformers as laboratory for interpretability. In Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., and Levine, S. (eds.), Advances in Neural Information Processing Sys- tems, volume 36, pp. 37876-37899, Curran Associates, Inc., 2023.
Feng. G., Zhang, B., Gu, Y., Ye, H., He, D., and Wang, L. Towards revealing the mystery behind chain of thought: A theoretical perspective. In Oh, A., Naumann, T., Glober- son, A., Saenko, K., Hardt, M., and Levine, S. (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurlPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023.
Liu, B., Ash, J. T., Goel, S., Krishnamurthy, A., and Zhang, C. Transformers learn shortcuts to automata. In The Eleventh International Conference on Learning Represen- lations, 2023a. URL https: / /ppnreview.e.eoeeoo net/ forum? DDrum?iddDeePYyiFEee
Giannou, A., Rajput, S., Sohn, J.-Y., Lec, K., Lec, J. D., and Papailiopoulos, D. Looped transformers as pro- grammable computers. In Krause, A., Brunskill, E., Cho, K., Engelhardt, B., Sabato, S., and Scarlett, J. (eds.), Proceedings of the 40th International Conference on Ma- chine Learning, volume 202 of Proceedings of Machine Learning Research, pp. 1 11398-11 1442. PMLR, 23-29 Jul 2023. URLhttps http::/eaa///ccceeeeeeeee www. p.rss/ v202 2200//iize 1tto0/giannnn22aaaiooo html.
Liu, C., Lu, S., Chen, W., Jiang, D., Svyatkovskiy, A., Fu, S., Sundaresan, N., and Duan, N. Code execution with pre-trained language models. In Rogers, A., Bryd-Graber, J., and Okazaki. N. (eds.), Findings of the Association for Computationaa Linguistics: ACL 2023, pp. Toronto, Canada, July 2023b. Association for Computa- tional Linguistics. doi:
Han, S., Schoelkopf, H., Zhao, Y., Qi, Z., Riddell, M., Zhou, W., Coady, J., Peng, D., Qiao, Y., Benson, L., Sun, L., Solano- A., Szabó, H., Zubova, E., Burtell, Fan, J., Liu, Y., Wong. B., Sailor, M., Ni, A., Nan, L., Kasai, J., Yu, T., Zhang, R., Fabbri, A., Kryscinski, W. M.. Yavuz, S., Liu, Y., Lin, X. V., Jory, S., Zhou, Y., Xiong, C., Ying, R., Cohan, A., and Radev, D. FO- LIO; Natural language reasoning with first-order logic. In Al-Onaizan, Y., Bansal, M., and Chen, Y.-N. (eds.), Proceedings of the 2024 Conference on Empirical Meth- ods in Natural Language Processing, Miami, Florida, USA, November 2024. Association for Computational Linguistics. URL https: aall awwaanhhalooyyyy. /rg/ 2024. www.eemmmm.m.1222222.
308. URL https: /ttlss:/allaaaaa //a//aaaaathhloco org/ 2023. f Findings-acl. 308/
Merrill, W. and Sabharwal, A. The parallelism tradcoff: Limitations of log- reg-precision transformers. Transactions of the Association for Computational I Linguisties, 11:531- 545, 2023. doi: 10.1162/tacl 00562. URL https: / //aclanthology wrg//023.3022 tacl-1.31.
Merrill, W. and Sabharwal, A. The expressive power of transformers with chain of thought. In The Twelfth International Conference on Learning Representations, 2024. URL https: hnttps://opensee /tpp///eee/eeeeeeeeee/pee. net/ forum? id NJNNNGGPPh.h
Hazra, R., Venturato, G., Martires, P. z. D., and Raedt, L. D. Can large language models reason? a characterization via 3-sat, 2024. URL https: /ttp:i//axivvvv//a org/ abs/
Merrill, W., Sabharwal, A., and Smith, N. A. Sat-
urated transformers are constant-depth threshold circuits. Transactions of the Association for Computa- tional Linguisties, 10:843-856, 2021. URL https:
2408. 07215.
Jha, P., Jana, P., Suresh, P., Arora, A., and Ganesh, V. RIsf: Reinforcement learning via symbolic feedback, 2024.
//api. www.aanniiiccoooooooooooooooooee 248085924.
URL httpt: http::///xxxvv..r...e abc///0bs/2255/ 16661.
Kambhampati, S., Valmeekam, K., Guan, L., Verma, M., Stechly, K. Bhambri, S., Saldyt, L. P., and Murthy, A. B. Position: LLMs can't 't plan, but can help planning in LLM-modulo frameworks. In Forty-first International Conference on Machine Learning, 2024. URL https: // //openrevi ew, www.wwww.eeeeeeeeeeeeee.eeeeeeee www//eeruunnmme i d= 8 4
Merrill, W., Sabharwal, A., and Smith, N. A. Sat- urated transformers are constant-depth threshold cir- cuits. Transactions of the Association for Computa- tional Linguistics, 10:843 856, 2022. doi: 10.1 a_00493. URL https: / aaclantooooggy....cccccooooollla www.ooooog.oooo.oo.ooooooo
10

---

Can Transformers Reason Logically? A Study in SAT Solving
Nieuwenhuis, R., Oliveras, A., and Tinelli, C. Abstract dpll and abstract dpll modulo theories. In Baader, F. and Voronkov, A. (eds.), Logic for Programming, Ar- rificial Intelligence, and Reasoning, pp. 36-50, Berlin, Heidelherg, 2005. Springer Berlin Heidelberg. ISBN 978-3-540-32275-7.
Conference on Learning Representations (ICLR 2019),
2019. URL https: https///opppeeeeeeeeeee net/ forum? 2D-HJMCCiA5te
Shi, Z., Li, M.. Khan, S., Zhen, H.-L., Yuan, M., and Xu, Q. Satformer: Transformer- based unsat core learning. in 2023 ieee. In ACM International Conference on Com- puter Aided Design (ICCAD), pp. 1-4, 2022.
OpenAL. Openai ol system card, 2024. URL https: //cdn.openai......mmooooo///o.
system-stemeem card. pdf.
Tafjord, O., Dalvi, B., and Clark, ProofWriter: Gen- erating implications, proofs, and abductive statements over natural language. In Zong, C., Xia, F., Li, W., and Navigli, R. (eds.), Findings of the Association for Com- putational Linguistics: ACL-IJCNLP 2021, pp. 3621- 3634, Online, August 2021. Association for Computa- tional Linguistics. doi: 10. 10.18653/112002..imdimm 317. URL https: http://aaaannttlyo.ooooo org/ 2021. f findings-ache .c1.31//1
Pan, L., Albalak, A., Wang. X., and Wang, W. Logic- LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Bouamor, H., Pino, J., and Bali, K. (eds.), Findings of the Association for Computational Linguistics: EMNLP 2023, Singa- pore, December 2023. Association for Computational Linguistics. doi: 10.18663//1/202333nmnnng
248. URL https:/ ac awwholoyhhooyy...oo org/2023. Sandings-emnip.2455
Touvron, H., Lavril, T., Izacard, G., Martinet, X., Lachaux, M.-A., Lacroix, T., Rozière, B., Goyal, N., Hambro, E., Azhar, F., Rodriguez, A., Joulin, A., Grave, E., and Lam- ple, G. Llama: Open and efficient foundation language models. ArXiv, 0es/2202.119711 2023.
Paszke, A., Gross, S., Chintala, S., Chanan, G., Yang, E., DeVito, Z., Lin, Z., Desmaison, A., Antiga, L., and Lerer, A. Automatic differentiation in pytorch. 2017.
Pérez, J., Marinković, J., and Barceló, On the turing completeness of modern neural network architectures. In International Conference on Learning Representations, 2019, URL https:://// wwwpeerrwweww.eeeeeeeee id-HyGBdo0gfhh
Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, L., and Polosukhin, I. Attention is all you need. In Guyon, I., von Luxburg, U., Bengio, S., Wallach, H. M., Fergus, R., Vishwanathan, S. V. N., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp.
Ryu, H., Kim, G., Lee, S., and Yang, E. Divide and trans- late: Compositional first-order logic translation and veri- fication for complex logical reasoning. In Proceedings of the 13th International Conference on Learning Represen- tations (ICLR 2025). OpenReview, 2025. URL https: //openreview net forrmm/oummm i - 0 9F NmvNMw.
2017.
Wei, J., Wang, X., Schuurmans, D., Bosma, M., ichter, b., Xia, F., Chi, E., Le, Q. V., and Zhou, D. Chain-of-thought prompting elicits reasoning in large language models. In Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., and Oh, A. (eds.), Advances in Neural Informa- tion Processing Systems, volume 35, pp. 24824-24837. Curran Associates, Inc., 2022.
Saparov, A. and He, H. Language models are greedy rea- soners: A systematic formal analysis of chain-of-thought. In The Eleventh International Conference Learning Representations, 2023, URL https: ppenreview. net/ fort/fooum?ii i d= (B00==GVVVBBB FWVB2XxX2V.
Saparov, A., Pang, R. Y., Padmakumar, V., Joshi, N., Kazemi, M., Kim, N., and He, H. Testing the general deductive reasoning capacity of large language models using ood examples. In Proceedings of the 37th Inter- national Conference on Neural Information Processing Systems, NIPS '23, Red Hook, NY, USA, 2023. Curran Associates Inc.
Weiss, G., Goldberg, Y., and Yahav, E. Thinking like transformers. In Meila, M. and Zhang, T. (eds.), Pro- ceedings of the 38th International Conference on Ma- chine Learning, volume 139 of Proceedings of Machine Learning Research, pp. 11080-1 1090. PMLR, 18-24 Jul 2021. URI. http://poooccceeee//o//oo ml .press/ v1 1339/ het//wiss221... html.
Sato, T. and Kojima, R. Matsat: naatrx--assdd differen- tiable sat solver. arXiv preprint arXiv:2108.066 064881 2021.
Xu, J., Fei, H., Pan, I., Liu, Q. Lee, M.-L., and Hsu, W. Faithful logical reasoning via symbolic chain-of- thought. In Ku, L.-W., Martins, A., and Srikumar, V. (,ds.), Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume I:
Selsam, D., Lamm, M., Bünz, B., Liang, P., de Moura, L., and Dill, D. L. Learning a sat solver from single- bit supervision. In Proceedings of the 7th International

---

Can Transformers Reason Logically? A Study in SAT Solving
Long Papers), Bangkok, Thailand, August 2024, Asso- ciation for Computational Linguistics. URL https:
//aclanthology 22tp:n/hwo.oog.oooo2222.24 aalalcllnnnn -ong. 720/.
Yao, S., Peng, B., Papadimitriou, C.,, and Narasimhan, K. Self-attention networks can process bounded hierarchical languages. In Association for Computational Linguistics (ACL), 2021.
Zhang. H., Li, H., Meng, T., Chang, K.-W., and Van Den Broeck, G. On the paradox of learning rea- from data. In Proceedings of the Thirty-Second In- ternational Joint Conference Artificial Intelligence, ICCAI '23, 2023a. ISBN 978-1-956792-03-44 doi: 00.24963/jccai URL https::/pp// orr/ 10. 111966//jcaa.2223///
Zhang, H., L. H., Meng, T.,, Chang, K.-W., and Van Den Broeck, G. On the paradox of learning to rea- son from data. In Proceedings of the Thirty-Second In- ternational Joint Conference on Artificial Intelligence, UCAI '23, 2023b. ISBN 978-1-956792-03-4. doi: 0M.24663/jcaai22223/777 URL https: /dri 10. 249634 202333333
12

---

Can Transformers Reason Logically? A Study in SAT Solving
Chain-ofThought Length vs Number of Variables (p)
Random Max CoT
Random Average CoT
107
Marginal
Marginal Average CoT
Skewed Max
Skowed Average CoT
104
2
Chain of Length
x 20000
204
10a
10a
10a
10
20
Number Variables (p)
Figure CoT Lengths generated by the compiled SAT-Solver Model the number of boolean variables in sampled SAT formulas, y-axis in log scale. Solid lines denote the maximum CoT length for each dataset while opaque, dashed lines denote the average CoT length. The empirical maximum CoT length our datasets bounded by 8p- 20008p
A. Training Details
We use Llama (Touvron et al., 2023) models the HuggingFace library. For the 70M model, we use models with 6 layers, 512 embedding dimensions, heads, 512 attention hidden dimensions, and 2048 MLP hidden dimensions. For the 140M model, use 12 layers, 768 embedding dimensions, 12 heads, 768 attention hidden dimensions, and 3072 MLP hidden dimensions. Both models have 850 context size. We trained for 5 epochs on both datasets using the Adam optimizer with scheduled cosine learning rate decaying from x 10-4 to 6 10-5 with 31 = 0.9 and A3 = 0.95.
B. Additional Experiment Results
Number CoT Tokens for Theoretical Construction In Figure 4 we provide results on the number of CoT tokens required solve randomly generated SAT instances. The number of CoT tokens required to decide 3-SAT instances below our theoretical bound for all instances
Effect Soft Attention In Figure 5 we provide results on how the SAT/UNSAT prediction accuracy affected by numerical errors introduced by softmax. In particular, when the 3 value that controls the "hardness" of attention is below the necessary threshold, the resulting models can only achieve perfect accuracy for formulas with smaller sizes.
Length Generalization Results on Additional Datasets In Figure we present results for length generalization (descrihed in Section 6.2) on the marginal and skewed datasets.
C. Proofs
C.1. Preliminaries on Transformers Models
The Transformer architecture (Vaswani et al., 2017) is foundational model in deep learning for sequence modeling tasks. In our work, we focus on the autoregressive decoder-only Transformer, which generates sequences by predicting the next token based on previously generated tokens. is a relatively complex architecture. and here we only give a precise but quite concise description, and we refer the reader (Vaswani al., 2017). among many others, for additional details. Given an
13

---

Can Transformers Reason Logically? A Study in SAT Solving
Accuracy vs Number Variables for Different Exactness Values
100.0
02.5
87.5
13.0
135
82.5
14.5
15.0
10
14
16
Number of Variables
Figure The impact of soft attention Transformer layers on the SAT/UNSAT prediction accuracy. is scaling factor that allows the soft attention operation to better simulate hard attention the cost of larger model parameter values in attention layers. The model achieves perfect accuracy on all "marginal" datasets starting at 15, and lower /3 values, the resulting models can achieve perfect accuracy for formulas with variables of smaller sizes.
Accuraiy don Dotaoct
Acouraty Rondom Dotacet
Taiiiing Regine
Branngg Rogine
(DD (inutr
11.3 Jewen ULRAA
merchal
0 mecer INE
15 marohell (LB)
Banec
Thaining Regine
Repine
1. meae (NN in (nnat)
11.1% waue ckat wireAn
slowed Well
Figure 6. Result of the Length generalization experiments on the random and skewed evaluation dataset. The meaning of different lines the same Figure
input sequence tokens s = ($1. s2....,
......,,, sn) V", where a vocabulary, a Transformer model M V~ - maps to an output token 8n+1 E V by composing a sequence of parameterized intermediate operations. These begin with token
14

---

Can Transformers Reason Logically? A Study in SAT Solving
embedding layer, following by L transformer blocks (layers), each block consisting of H attention heads, with embedding dimension demb, head dimension d,, and ML.P hidden dimension dmlp- Let
describe each of these maps in detail.
Token Embedding and Positional Encoding. Each input token is converted into a continuous vector representation Embed(s;) E R using fixed embedding map Emb(-). To incorporate positional information, a positional encoding vector P. E Rd is added to each token embedding. The initial input to the first Transformer block is
X (Emb(s1) + Pı...., Emb(s,.) P..) RRxd
Transformer Blocks. For - I..... L. each block of the transformer processes an embedded sequence X E R2xd to produce another embedded sequence (1), E Raadd Each block consists of a multi-head self-attention (MHA) mechanism and position-wise -iie fordafd network (MLP). We have set of parameter tensors that includes MLP parameters w Rd Xdip, (()) E Ri W!ll) IR xd and " Rdd self-attention parameters w.(.A), w w Rdddd for every l..... ........ H, and multi-head projection matrix w E (H,,))) We will collectively refer to all such parameters layer I I whereas the self-attention parameters for attention head h at layer will be referred as ((AA), We process the embedded sequence X (1-1) obtain ( in two stages:
H (1-11) MHA (x(==1;(0))
x + (0) + MLP (HW:Tw)
where
MHA (x:110) [Au(X: ALt(; r() W
XW(
(WiaM) X)
Au((x:1(h)))
Vah +
M
xw
MLP (H:T") act (HW(") bl)) W +
The n x n matrix M is used as a "mask" to ensure self-attention is only backward-looking, so we set M i 2 j and Mi. = 0 otherwise. a represents the softmax operation. We use the ReGLU(-)) 2d + Rdo activation function (-)(-) at each position. Given input u E R 2dul,, for each position we split u, into two halves u.u. U1 E Rd and, using @ denotes element-wise multiplication, we define
[i = -o for
ØRGGLU (u.) u,, ReLU (u.,2).
Output Layer, After the final Transformer block, the output representations are projected onto the vocabulary space to obtain score for each token. We assume that we're using the greedy decoding strategy, where the token with the highest score the last input position is the model output.
(L) W + Dout E B Sn+1 arg max On,o E V
where Wout VR Dout E R.V. V is the size of the vocabulary, On is the score for token v at the last input position n.
Autoregressive Decoding and Chain-of-Thought During generation, the Transformer model is repeatedly invoked to generate the next token and appended to the input tokens, described in Algorithm 1. In this paper, refer to the full generated sequence of tokens the Chain-of-Thought (CoT), and the number of hain-offthhough tokens in Algorithm 1 is 1 n.
Algorithm 1 Greedy Decoding
Require: Model M y* + V, stop tokens E C V. prompt 81.. (81, 82,.... .,))..,,n)). & <-
1: while f 4- ++11 do
2: 8; < ()
3: sf return 814
4: end while
15

---

Can Transformers Reason Logically? A Study in SAT Solving
C.2. 3-SAT
SAT The Boolean satisfiability problem (SAT) is the problem of determining whether there exists assignment A of the variables in Boolean formula F such that F is true under A.
3-SAT In this paper, only consider 3-SAT instances in conjunctive normal form (CNF), where groups of most 3 variables and their negations (literals) can be joined by OR operators into clauses, and these clauses can then be joined by AND operators. We use the well-known DIMACS encoding for CNF formulas where each literal is converted to a positive or negative integer corresponding to its index, and clauses are separated by a (which represents an A operation). SAT problems where the Boolean formula expressed in conjunctive normal form (CNF) with three literals per clause will be referred to as 3-SAT. formula in CNF is a conjunction (i.e. "AND") of clauses, a clause is disjunction (i.e. "OR") of several literals, and each literal is either variable its negation. In the case of 3-SAT, each clause contains at most three literals. An example 3-SAT formula with 4 variables and 6 clauses is:
(x1 -x2) (- V 22 V -x3) A (22 V I4 V -1))
(21 Eg 14) 02 V -g V I4) A (-44 v4 vn)
In the above formula, (z) V -x2) a clause, which contains the literals 2 and -2
The 3-SAT problem refers to determining if any assignment of truth values the variables allows the formula e to evaluate true. It well-known that 3-SAT NP-hard and is widely believed to be unsolvable in polynomial time.
DIMACS Encoding The DIMACS format is standardized encoding scheme for representing Boolean formulas in conjunctive normal form (CNF) for SAT problems. Each clause in the formula is represented as a sequence of integers followed by terminating "0" (i.e. "0" represents A symbols and parentheses). Positive integers correspond to variables, while negative integers represent the negations of variables. For instance, a clause includes the literals T1, -2, and 23, it would be represented as "1 -2 3 0" the DIMACS format.
For the 3-SAT example the previous paragraph. the corresponding DIMACS representation would be:
2- 0 - 2 -3 0
-1 0
-3
4
0
-2
-3
-4
0 4 -1
Reducing a Formula. Let
F
A C.
be a 3-SAT formula, where each C, is clause (i.e. disjunction of up to three literals). The reduction of F by A, denoted Fl. is defined by:
1. Remove (drop) any clause satisfied by A.
A clause C₁ is satisfied by A if there is literal & E C2 such that E A. In that case, C. is automatically True and can be omitted from the conjunction.
2. Delete (false) literals contradicting A.
For each remaining clause C,,, if it contains a literal that is false under A, remove that literal from C. Specifically:
If 2 A (so 2j is True), then any literal -ry in C2 becomes false and is removed. - E A (so x, Fal Fe) then any literal zy in C removed.
If clause loses all its literals through this process, it becomes empty clause and the formula is immediately False. Formally, for each clause C2 C J., define
Cdla
(G: E E Cs is forced false by A))
and keep CslA only it is not already satisfied by A. Then
FlA =
A (CAlA)-
Ct not salisfied
16

---

Can Transformers Reason Logically? A Study in SAT Solving
As an example, suppose
F (x) V -22) (-0n Vass) A (x2 -ma)-
Let A = {.1}. Then:
1. The first clause (x) -22) is satisfied by 21 A. Hence remove it from the formula.
2. In the second clause (-01 V 2z),, the literal = - is false (since Tı is set True). We remove -2n and are left with (rz).
3. The third clause (22 V -ar) is untouched: does not appear, so no literal is removed. However, it is not satisfied by 21, so we keep it.
Thus,
Fla (2a) A (x2 V -r3).
If a partial assignment forces a clause to become empty, the whole formula becomes unsatisfiable under that assignment. For instance, with
F (2) V22) (-x1 V x22),
and partial assignment A (22, we see:
The first clause (æ1 (2) is satisfied by æ1 and gets removed.
In the second clause (~wr V maz2), both -zn and mag contradict A, so both are removed. This leaves the second clause empty, which means A is an empty conjunction (i.e. False).
Hence no full extension of A can satisfy F.
Unit Propagation. An additional reduction step performed in SAT solving is unit propagation. After applying partial assignment A to formula F (obtaining FlA). some clauses may reduce to single literal (called a unit clause). Formally, clause C = f,,.... } is unit if k: = 1. If C is unit, its lone literal & must be assigned True in any extension of A that satisfies F. Concretely:
1. Identify unit clauses. Scan the reduced formula FlA- If there is clause C. with exactly one remaining literal &, then f is forced True.
2. Extend the partial assignment. Insert the forced literal e into A.
3. Re-reduce the formula. Remove any clauses satisfied by é, and remove -l from all remaining clauses.
This process may uncover additional unit clauses in subsequent steps, so unit propagation continues iteratively until there are no more clauses of size 1. If at any point clause becomes empty, we conclude that the current assignment A cannot be extended to a satisfying assignment.
Example.
Consider = (x) V -22) (x1 za) (r2 V -r3) and a partial assignment {-x1}.
First, Fl removes (now falsified) from (x) V xz), leaving the unit clause (æz). Thus T3 is forced True.
We add 43 A, giving A AU (13). Re-reducing the formula removes any literal -wg- If that step causes another clause to become unit, repeat.
This iterative assignment of forced literals often simplifies the problem significantly before any broader search is required.
C.3. Proof of Lemma 4.7
We prove each of the three statements in the lemma, showing that the vector-based definitions correspond to the logical operations described.
17

---

Can Transformers Reason Logically? A Study in SAT Solving
1. Satisfiability Checking
A AF F
min iE|d
E(C,) ((C)))((A) 2 1.
Logical Interpretation. The left-hand side, A F P. means that every clause C₁ in F is satisfied by A. This is equivalent to saying that, for every clause C₁ there exists at least one literal I E C2 such that E A.
Vector Translation. For a clause C₁ and a partial assignment A, the dot product E(C,) E(A) computes the number of literals in C₁ that are also in A:
E(C,) E(A) (a.ee..)) (z, + Σ 1 1-o. EC,) 1-2,EA = C; 0 A/.
If ((C) E(A) 2 1, this means there is at least one literal in C n A, and hence C; is satisfied. Taking the minimum over all clauses ensures that every clause C₁ is satisfied, which is precisely the condition for A - F.
2. Conflict Detection
F A
min ((CC)) sEle]
Emot-false (4)) O.
Logical Interpretation. The left-hand side, F - -A, means that contradicts A, i.e., there exists a clause C₁ in such that all literals in C2 are forced false by This happens if and only if no literal in C, "not-false" under A.
Vector Translation. For a clause C₁ the dot product E(C,) Eaote (A) computes the number of literals in C2 that are not forced false by A:
P Σ 1 (--. Σ 1 (-x.e... (mugA).
P
E(C+) Enot-false (A)
If (CC)) Fnot-falee (A) = 0, this means all literals in C₁ are forced false by A, and C₁ is a contradiction. Taking the minimum over all clauses ensures that this happens for at least one clause, which corresponds to F -A.
3. Deduction (Unit Propagation)
E(D) = max min Σ JE|e]
Baan)--E(CA E(C,), 1) Eassigned(A., o).
Logical Interpretation. A clause C; becomes unit clause under A if all but one of its literals are forced false by A. In this case, the remaining literal must be set to True in any extension of A. The set D) consists of all such literals deduced via unit propagation.
For each clause C₁ the condition E(C,) Enot-fatee (A) = identifies unit clauses after reduction, i.c., those with exactly one literal not forced false by A. For such clauses, E(C,)) encodes the remaining literal.
Vector Translation.
The summation
Σ ((ac))))) F((A))
sEle
computes a vector where each coordinate accumulates contributions from unit clauses identifying the corresponding literal. Taking min(:;) elementwise ensures that each coordinate is at most 1, avoiding overcounting. Finally, subtracting Enssigned A) removes literals that are already assigned by A, leaving only the newly deduced literals.
This matches the conditions for unit propagation as defined in Appendix C.2
18

---

Can Transformers Reason Logically? A Study in SAT Solving
C.4. Useful Lemmas for Transformers
In this section, several useful results on Transformer operations on their approximation capavilities. Specifically, MLP with ReGLU can exactly simulate ReLU, linear operations, and multiplication without error. For Self-attention lemmas, directly adapt from (Feng et al., 2023).
Lemmas for MLP with ReGLU activation This section shows several lemmas showing the capabilities of the self- attention operation and MLP layers to approximate high-level vector operations. These high-level operations are later used as building blocks for the Transformer SAT-solver. Specifically, with appropriate weight configurations, a 2-layer MLP with ReGLU activation (() = W2[(W,a a + b) @ velu(Var + e)] can approximate the following vector operations for arbitrary input æ:
Simulate a 2-layer MLP with ReI.U activation: W2 ReL.U(W/x b() b/2
Simulate any linear operation Wæ
Simulate element-wiss multiplication: æ 022
Lemma C.1 (Simulating a 2-ye ReLU MLP with ReGLU Activation). A 2-layer MLP with ReGLU activation uctucationfuucctionn can simulate any 2-layer MLP with ReLU activation function.
Proof. Let the ReLU MLP be defined as:
g W1 ReLU(W b₁1) +b2.
Set the weights and biases of the ReGLU MIP as follows:
Wi 0,
b 1,
V = W 1
b = b/:
W2 = W2 b = b'z.
Then, the ReGLU MLP computes:
f(x) = W2 [0- x + 1) @ ReLU((W(= + b,)] bz2
Simplifying:
f(x) = W2 [1 & ReLU( + b1) + b/2 W ReLU + =g(x).
Thus, the ReGLU MIP computes the same function as the ReLU MLP.
Lemma C.2 (Simulating Linear Operations with ReGLU MLP). A 2-layer MLP with ReGLU activation can simulate any linear operation fax Wa + b.
Proof. To compute a linear function using the ReGLU MLP, we can set the activation to act as scalar multiplier of one. Set the weights and biases as:
Wi = W b b,
= 0, b = 1,
W2 b 0.
Here, I is the identity matrix.
Since Vx + by = b2 = 1, we have:
ReLU(Vx + b²) = ReLU(1) 1.
Then, the ReGLU MLP computes:
f(x) = [( b) 8 1| = Wa x
Thus, any linear operation can be represented by appropriately setting Wi, b,, and Wz.
19

---

Can Transformers Reason Logically? A Study in SAT Solving
Lemma C.3 (Element-wise Multiplication via ReGLU MLP). A 2-layer MLP with ReGLU activation can compute the element-wise multiplication of two input vectors an and 2/2, that is,
f(z) = 21 @ 22
where a [x1; [22) denotes the concatenation of œ1 and T2
Proof. Let x [22] E R where 21, 22 E R
Set the weights and biases:
I
W1 =
bi 02n>
In
In
V =
b2 02n
-In
W2 = In 1
b 0,-
Compute:
21
Wi0+b +b =
31
Væ =
22
ReLU(Vx +b:) = RcLU(xx2)
ReLU
The wies product:
œ @ ReLU((x))
+ @ ReLUUVV++b)
x ReLU(-222)
Compute the output:
f(æ) = W2 [[ + @ RVL - b2)] +
τ @ ReLU(xx) - x1 @ ReLU(-=2)
21 & (ReI.((a2)) ReI.U(-x3))
2. 22
Thus, the ReGLU MLP computes f(x) = z @ xy without restrictions on Ø2.
Capabilities of the Self-Attention Layer In this subsection, we provide core lemmas on the capabilities of the self-attention layer from (Feng et al., 2023).
Let be an integer and let 21, ...... ..... ri E R. and M is large constant. Let K, Q. E Rdd (d+2) be any matrices with | loc and let 0 < < < M be
,, In be a sequence of vectors where x; (æ,, r,, M, M2 a, Rd.
any real numbers. Denote q: Qz, k = Kæ,, 8, Væj, and define the matching set S; {j $ i: qq k, s p). Equipped with these notations, we define two basic operations as follows:
COPY: The output is sequence of vectors U1,
with u; Upoe((), where pos(i) argmax Tj- MEAN: The output is a sequence of vectors u1, with meanjes, Uj.
Assumption C.4. [Assumption C.6 from (Feng et al., 2023)] The matrices Q, K, V and scalars p, satisfy that for all considered sequences ø1, Ø2. ... In. the following hold:
For any i,j E [n]. either lg: kyl S p or qi k2 S -8
20

---

Can Transformers Reason Logically? A Study in SAT Solving
For any i,j [n]] either i or |r ryl d.
Assumption C.4 says that there are sufficient gaps between the attended position (e.g., pos(i)) and other positions. The two lemmas below show that the attention layer with casual mask can implement both COPY operation and MEAN operation
efficiently.
8 For any > there Lemma C.5 (Lemma C.7 from (Feng al., 2023)). Assume Assumption C.4 holds with p 8M exists attention layer with embedding size ((d) and one causal attention head that can approximate the COPY operation defined above. Formally, for any considered sequence of vectors 1 22.,..... .... En, denote the corresponding attention output as 01, .2.....00 .On- Then, we have ||o; - u.lloo I cfr all [n] with St + M. Moreover, the fox norm of attention parameters is bounded by (pooly (M, 1/6,
Lemma C.6 (Lemma C.8 from (Feng et al., 2023)). Assume Assumption C.4 holds with p 16M In( " For any
bc
O <e S. M, there exists an attention layer with embedding size O(d) and one causal atlention head that can approximate the MEAN operation defined above. Formally, for any considered sequence of vectors B1 .D....., Dn, denote the attention
output as 01, O2..... ,, Then, we have 0, - uilloo S for all E [n] with S; + 0. Moreover, the foo norm of attention parameters is bounded by ((poly(M,1)) log(n), log(//))).
C.5. Saturated Attention
To introduce our construction of Transformer layers and attention head, we first introduce saturated self-attention, which is an idealization of the usual softmax attention head that allows for sparse and uniform attention (i.e. "hard" attention):
Definition C.7 (Saturated Masked Attention, Merrill al. (2022)). A saturated attention head with hidden dimension da, embedding dimension demb and weight r, (Wq. WK, Wv) is a function Saturated Attn (;r,) Ruxddu - IR d. that satisfy the following:
A XW Q (W K x E
M₁ (j E [i] Aij max A
SaturatedAttt((:I15 Σjem, X,Wr
M
Intuitively, while softmax attention computes a distribution of attention over all previous positions and computes weighted average, saturated attention only attends to the previous positions with the highest attention value and computes uniform average over these positions.
We now show that Saturated Attention can approximated by normal softmax attention:
Corollary C.8 (Softmax Attention Can Approximate Saturated Attention, implied by Lemma C.6). Let E N. Consider any input sequence X E Rax qdam,, and let SaturatedAAtnl I,) be a saturated attention head with a causal mask and parameter norm bounded by O(1) ) that produces outputs . On E Rdd.
Suppose further that, for each row i, the maximum atlention score maxjsi Si (Atz) of the saturated head exceeds all other scores by a margin of at least 8 O, i.e. i e M, (the set of maximizing indices) and of Mi, then Aij - Aik 2 8.
Then for any 0, there exists standard single-heat softmax attention function Attn(X:I) with parameter norms bounded by poly(M, (M, log(n), log(1) such that its outputs oi,..., Ön E IR satisfy
6 oilla S for all 1 isisn
In other words, if saturated attention head has strict dot-product margin among the top positions, il can be approximated arbitrarily closely by an ordinary causal softmax attention mechanism, using parameter magnitudes that grow at most polynomially 1/8, M, log(n), and log(1/E).
C.6. Proof of Lemma 4.8
We proof a version of Lemma 4.8 that uses saturated attention. Lemma 4.8 is immediately implied by the following lemma and Corollary C.8
21

---

Can Transformers Reason Logically? A Study in SAT Solving
Lemma C.9 (Saturated Masked Attention version of Lemma 4.8). Let F be a 3-SAT formula over variables (x1.-..;;pp) with clauses {C1,-... Cet and A partial assignment defined variables (-1,.-- Fp.. Let
0
1
1
E(C1)
0
1
X encodinng
:
E [2(+2))(2p+22)
E(C.)
1
E(A)
0
1
Then given X as input, there exists:
An saturated attention head with parameters 1AAF and hidden dimension 1 that satisfies
AaturatedAAtu(X:114]]
)et2 Pe44 LA=F
saturated attention head with parameters D and hidden dimension 1 that satisfies
AaturatedAAtt(X:1gg 'A) "A)+2 1F=
An saturated attention head with parameters 1.2 with hidden dimension 2p and MLP layer with parameters 1' MLP satisfy:
M MTP[[SaturateelAttt(XXXX X|: = F(D)
unless F -= -A, where E(D) is as defined in 4.7
Proof. We prove each of the three constructions in turn, using the definition of saturated attention (Definition C.7) and standard reductions from the logical semanties dot-product comparisons.
We explain how construct parameter matrices (WQ, WK. Wv) such that the resulting saturated attention head imple- ments:
1. check for L (i.e. whether A satisfies F),
2. check for 1 F==A (i.e. whether A contradicts F),
3. step of unit propagation that yields E(D), provided F' Fا -A.
Within the following proof of Lemma C.9, we shorten X Kencoding X.
1. Checking Satisfiability ( F)
We construct the matrices
Wa E (222+2)x(()+1) WAFFF E 2))22))
W. E (2++2)x1
follows (with block-wise coordinate-wise O and Ozp denoting matrices/vectors of all zeros of dimension 2p where the dimension subscript is omitted if they can be inferred from other entries, and Ipp the 2p x 2p identity matrix).
Ipp
0
Igp
0
O2p
WAFF
WAFFF
W
0.5
1
0
0
0
0
Then
22

---

Can Transformers Reason Logically? A Study in SAT Solving
O2p
02p
0.5
E(C1)
E(C1)
X 1FF
XW AFF
XW, AFF
E(C))
-ECC)
E(A)
E(A)
0
-05
0
0
0.5
-E(C) E(C,)
- E(C2)
E(C1) E(A) E(C2) E(A)
A = XW (W x)=
A AFF AFF
=
-0.5
-E(C2) B(C))
-E(C,) -((2))
0.5
-E(A) E(C))
-E(A) E(C2)
-E(A) E(A)
Since we want to output 1A=F at the last position c + 2 corresponding to E(A) in X Xencoding we focus on the last row of A:
Act2 = 0-5
- -E(A)
E(A) E(C,) - -E(A) -E(A)
Now consider MM-2 = {j E Ic + 2] (ct2)))
max; ( Note that vi E [c] E(A) E(C,) e N and since
A (o+2),1 = 00.5 there is:
Met2 [1} =
min F(C;) F(A)21 1.
xE(c
Mc42 C 22,
min E(C)) E(A) 0.
sE|c
which are the only possibilities for nonnegative integers E(C,) EA). Also, since (XWAFF) [100 ... 0] we have that
X, X,WAFF
if j
0 otherwise
EjeMors X,W W,WA
SaturatedAAta (X; (s)2))++2
[M+22
1 if M {1}
(0 if C 2
IMe2=((1)
minneete E(C)))
LAFF
where the last step is by Lemma 4.7. This concludes our proof for satisfiability checking.
Defecting Conflict (F -= -A)
Note that for B we have
0 pxp
- Ip
Enot-Lalse (B)
E(B) + 1p
p
0pxp
Define
0
pxp
Ip
O,
0p
I
0 pxp
0,
0
P False
RR
(2++)))
0
0
1
0
1
1
0
1
23

---

Can Transformers Reason Logically? A Study in SAT Solving
Then
1
1
Enot-false
0
1
X P not False
:
E
fnot-false (Ce)
0
1
false (A)
0 1
We now construct the matrices
W 8 F=
WF == E (222))))((=11)
W
E (2(2)))((2+1))
w ===A E ((2+2))x1
Q
as follows:
02p
W PF-AA Q
P not. false
WAFFF
W==
WAF
Then
O2p Fmot- false (1)
O2p
0.5
0
F((1))
0
XW F- Q
XW F
:
XW
F
K
V
Enot-false (Ce)
E(C))
0
Unot-Tabse (A)
E(A)
0
Recall from Lemma 4.7 that:
F
min
E((C.)
Emot- (A)) O.
sE(c]
The remaining argument is very similar to satisfiability checking and omit the full proof.
3. Unit Propagation (D)
Recall that D (1 T. FFFAFA Fi 0} and
E(D) = max min
Σ (E(c)
Enssigned (A),
A), 0].
(2)
To address unit propagation with saturated attention, we use a slightly different formulation than the formula Lemma 4.7:
Proposition C.10. Let 1 be arbitrary constant, then
Σ
1 (EEC))) Em (A)= E(C;)
E(D) = ReLU Esssigned - ReLU(mz - 1)
Proof. We start from the expression in equation 2,
E(D) max min(z z, 1) Exsigned (A), 0]. where = ((( E(C)).
sE(c]
Because Eussigned (A) E {0, each coordinate of Esssigned (A) is either 0 or 1. A straightforward elementwise check shows the identity
max min(a, 1) b, 0) ReLUUma b) ReLU(ma - 1),
whenever E {0, 13. Indeed:
24

---

Can Transformers Reason Logically? A Study in SAT Solving
If 0, then the left side is max(min(a, 1), 0); the right side, ReLUU(m)) ---LReU-maa- -
exactly matches max(min(ma,, 1), 0) max(min(a, 0) for any 2 (this a standard piecewise identity).
If 1, then min(a, 1) - hence the left side is always On the right side.
ReLU(ma- - 1) ReLU(ma - 1) 0.
Applying this identity coordinatewise, we obtain max min(mz 1) Eassigned ()). o] ReLU Eassigned ReLU(mz - 1),
which matches the stated expression for E(D).
We now construct the matrices
Wo ((2222)x(2)))
W E (2
w E (R(+2)))(22))
as follows:
1pp
0
I
w = W Wh
FI-A
W =
-.55
wP = c
0
0
0
Then
O2p
02p
-1.5
O,
Fnct false (C1)
FF(C))
E(C1)
XW =
XW
XW =c
Enot-talse (Ce)
1
E((C.)
E(A)
Emot-faise ( (A)
1
E(A)
We focus on the last row of A = XW
Aot2 = 1-5 - -E(A) Fooo-falls (C1) E(()) Fnoo-false (C2)
E(A) Fnot-false (C.) -((A) Emot-false ( (A)]
Also, recall that assume here F # -A, so Vi, E(A) integers.
Enst-taise (Ci) 2 1 and therefore E(A) Enoot-fase (C,) positive
Mct2 {1} +
min E(C,) E(A) 2 2.
sefe
Mo+2 C c22,c+2)
+ min D(C;)-E((4 = 1.
iE|c
In particular:
{1}
if minzeja E(C,) Enssigned (A) 2 2
Mo+2
{ E F(C.)) Fassignnd (A) =1
otherwise
25

---

Can Transformers Reason Logically? A Study in SAT Solving
As result:
SaturatedAttn(X; (x: (244)4422 = EjEM.13 XjW
MM+22
O2p
Mc+2 {1} Eiele) (((CC))) B(C,)
if Mo+2 C c2
Mc+2
m
Σ
(E(()) (E((. Fmm E(C;)
iE[c]
for m [Mo+al 1.
We now construct the weights for the ReGLU MLP layer. By Lemma C.I we know that ReGLU MLP can simulate ReLU Ms.ss. Therefore, we only need to construct WP, W b
by such that
W ReLUUWP (mm;; X x b by ReLU(mz (assigned(A))
ReLU(mz 1).
Note that X = (EA)
1]. therefore [mz; X xo+2 E IR 2p4
Also,
I Ip I
Eassigned (A)
E(A)
p_
Therefore, define
Ip
WP
12p
O2px2p
I,
In
02px2
12p
02px2p
O 0ppx2p
02px2
O2p
6
112
W
T2p
-2p
6 02p
It be easily verified that this satisfies the desired equality.
C.7. Theoretical Construction (Theorem 4.5)
Notations
denotes the number of variables
t denotes the token at position i
T purs denotes the set of tokens that denote variables and their negations. i.e.
"2', '2',..... 'n', f-1', 1-2", "-2",..,,'-5 '-n"
denotes boolean variables
Proof. We first describe the encoding format of the formulas and the solution trace format before going into the details of model construction.
26

---

Can Transformers Reason Logically? A Study in SAT Solving
Imput Format. We consider 3-CNE-SAT formulas in the DIMACS representation, with initial [BOS] token and an ending [SEP] token. Each variable z; for i [x]] has 2 associated tokens: and -i (e.g.. and -1), where the positive token indicates that the i-th variable appears in the clause while the negative token indicates that the negation of the i-th variable appears in the clause. Clauses are separated using the 0 token. For example, the formula
(- V -44 V -11) (a3 V (-01 V Dy V -22)
A111 V -22 V - A - V.2 Vx1) (2) V m22 V vx4
would be represented as:
[BOS] -2 -4
4 -1 -3 -2 0 -2 4 -4 2 1 -2 0 [SEP]
Solution Trace Format. The trace keeps track of the order the assignments made and whether each assignment decision (assumption) or a unit propagation (deduction). Literals with a preceding token are decision literals while other literals are from unit propagation. When the model encounters conflict between the current assignment and the formula, it performs backtrack operation denoted by [BT] and performs another attempt with the last decision lit- eral negated. In particular, compared to Figure 1, we used D to abbreviate As and use [BT] to abbreviate Backtrack
As an example, the solution trace for the above SAT formula would be:
[SEP] D 2 D -4 [BT] -1 -4 [BT] -2 D 4 1 SAT use simplified versions of the tokens compared Figure 1. In particular, we use [BT] shorthand for BackTrack and for Deduce.
Implementation of Integer Arithmetic, Comparison, and Logical Operations In this paragraph, we show how basic arithmetic and comparison operations can be implemented as MLP layers. For simplicity, when describing the construction, directly specify the arithmetic and comparison operations performed each layer when applicable. In all descriptions below, we assume that we are given a vector of input parameters
a1
b1
a2
b2
X
Qn
bn
and describe the required MLP parameters implement element-wise integer arithmetic between a; and each position i E [n]. For simplicity of expression, since the operations element- assume wlog that the input is simply [a; 11x
Addition a + b: Let
1
0 -
W
bt
W
b = [0]
Then Wi ba; + = [a + b; 1]. ReG + b; 1]) + b. W ReGLU((a 1]) + b = a
Subtraction b: Implemented + (-b):
Wi 1
0
bj
W = [1]
bj 00]
Multiplication x b: Apply Lemma C.3 with 21 and 022 b
Comparison 1 Let
0
0
W comp
b
comp
W comp
-1]
b
[0]
1
27

---

Can Transformers Reason Logically? A Study in SAT Solving
Then for input (a, b), we have
1
W (1; b] + b
b
6
which is split into value part
and gate part
- 1
Applying the ReGLU activation
1
1 ReLU - a)
ReLU - a) ReLLU(b 10]
ReGLU
ReLU(b - -1)
and finally
W comp ReGLU(.) + b2 comp ReLU((- a) - ReLU(b - a Lasb.
Logical AND a A where a, b E {0, 1]: This is equal to a x
Equivalence This takes MLP layers to compute (a b)
Embedding Layer. Our token set consists of one token for each variable and its negation, the separator token 0, and special token D to denote where decisions made. The positional encoding occupies single dimension and contains the numerical value of the position of the token in the string. (i.e. there exists dimension pos such that the position embedding of position is epos)
The first layer prepares for finding the nearest separator token and D token. Let i denote the position index of tokens. Only MLP layers are used
Layer 1.
1. Compute ssp where isep if the corresponding token t; E {*0', '[SEP]', '[BT]') and ise 0 otherwise. This is computed as isep i (Rea(o) + (SE(()EP)) + (sd((BT1))
2. Similarly, compute ip where ip = i the corresponding token t; = and ssp = otherwise. This is computed as
i = X (sd(D)
3. Compute (i - 1)2, i2 for index equality comparison
Layer This layer uses 2 heads to perform the following tasks:
1. Copy the index and type of the last separator token and stores
p. sep' max [j S i,t, e f'0r, '[SEP]', '[BT]')
by (t; '0')
sase (t; '[SEP]')
Laald = (t, = =[BT]')
for j p. seps
2. (Backtrack) Compute the position of the nearest D token Df max{j :.j Sit,, 'D'}
3. Compute ppre for index operation
Task can be achieved via the COPY operation from Lemma C.5 with qi = 1, k; iscp. Vj = (i,lltz = '0'].1[t, = "[SEP]']. = [UP] I[, = [[ackTrrcc]"]] ']).
Task 2 highly similar task and can be achieved using COPY with qi 1, k; = ig. Ui (j)
28

---

Can Transformers Reason Logically? A Study in SAT Solving
Layer 3 This layer uses head to copy the several values from the previous token the current token. Specifically, this layer computes:
1. The position of the previous separator token, not including the current position:
P; pp" = max 1 < i,t, (''', *[SEP]', 1, [UP]', [BackTrack]"]
2. Dermine if the previous token is D: ddecission = (f:-1 = 'D') i.e, whether the current token is a decision variable
3. (Induction) Compute the offset of the current token to the previous separator token d = =i- Pi sep
4. Compute (,, for equality comparison at the next layer.
Task 1 and 2 is done by copying p; p and Lltt: = 'D'] from the previous token. Specifially, we use the COPY operation from
Lemma C.5 with qi = ((i 1)², i - 1, 1) and k = (-1,2) 2j. -²2) which determines - 1 = j via - ((( 1) - j)² = 0
and ;2 = (v; sep II[;; = D'I)..
Layer 4.
This layer uses 2 heads to perform the following tasks:
1. Compute
F(BB.)
Σ Odd(t)
Σ
edd(t,)
SPPEEM,TTT... ETOora
" M,
Recall that E(B.) is binary encoding of the literals in a clause or partial assignment. Since each literal is represented in the DIMACS encoding single token, summing up the one-hot token embedding of each literal in a clause/partial assignment is equivalent to computing its encoding E(B) value. The above operator finds the previous separator and sums up all the embedding dimensions corresponding to literal one-hot embeddings. Therefore, the above computation satisfied:
For input DIMACS encoding: Suppose that the separator 0 token following clause k is at position in the DIMACS encoding tokens, then E(B,) E(Cs). where t; = *0"
For the current position: For the final position I, for which we're we're predicting the next token, E(B,) = E(A), where A is the current partial assignment.
2. (Induction) Compute the position of the second-to-last separator P p- sep ('0', '[SEP]', '[BackTrack]'] }} pp.- and the corresponding current position in the previous state p;
max(j
P sep tt
P; p: + As special case for the first state, we also add 4 to p; if Iseet is true, i.e. Pi = p, p0a0 + + +4 4-b [sxe]
The additional 4 is the number of variables per clause + ensure that we don't consider the last clause as assign- ment.
3. (Backtrack) Compute the position of the nearest token to the last separator token pf PR.
4. Compute bewoeed= = (p, > P. + 1). this denotes whether we're beyond the last decision of the previous state.
5. Compare (pp p. for bIT finisee at the next layer.
6. Compare if p.. = p. for the bbacktrack operator.
7. Compute V'oopy (pf <
Pi sept 1)
Task is achieved using a MEAN operation with qi ((p)e)) PPPP 1), k, = ((-1,2p, -() v, Caa(t)) for
1 E Tours. This attention operations results in i-p.er The MLP layer then uses Lemma C.3 multiply the mean result by
i pe to obtain the r;-
Task 2 is achieved using the COPY operation with qi = ((p (2
P. sep 1). k, = (-1,2j -)²) and Dj P. sepr The MLP
layer then performs the addition operation the computes P. by Lemma C.2
Similarly, Task is achieved using the COPY operation with qi
((x sEpy )2 PP, sep 1)) ky = (-1,2j, -j²) and v, = pp-
29

---

Can Transformers Reason Logically? A Study in SAT Solving
Layer 5. The third layer uses 5 heads to perform the following tasks:
1. Compute LAFF, 1F E(D) where : from the previous layer.
= fle FAAFI according to Lemma 4.7 with the E(B,) values
2. Compute Dfinal = bexceed Odecisson
3. Compare nno decisson (pp S P), which denotes whether the current state contains no decision variables
4. Compute dii.iinssbed = (pp S p; ) A [[ackTrack]
5. Compare P with pi_ by storing P; S Pf- 1 and Pj 2 pT_ 1 (to check for equality at the next layer)
6. Compare bbacktrack (p
1)
Layer This layer does the remaining boolean operators required for the output. In particular,
bunsat
Dno decision A beont
b(DT)= beont -tt [BT])
Compute a vector that is equal to bbacktrack CBT, which is equal to egr if bbacktrack is True and 0 otherwise. This is to allow the operation at the output layer for backtracking
Note that can be implemented as single ReLU operation for tasks and that can be implemented with Lemma C.I, and task 3 is multiplication operation implemented with Lemma C.3
Layer This layer performs a single operation with the ML.P layer: Compute beopy Peopy, which gates whether Ceopy should be predicted based on beopg. This enables condition 5 the output layer.
Output Projection The final layer is responsible for producing the output of the model based on the computed output of the pervious layers. We constructed prioritized conditional outputs, where the model outputs the token according to the first satisfied condition in the order below:
1. If beat output SAT
2. If beant A Uno.decision output UNSAT
3. If beont A -tt; [BackTrack]] output [[aakKTrak]"'
4. (BackTrack) If bbacktrack, output the negation of the token from position pf +
5. (Induction) If beopy, copy token from position p; 1 as output (Ecopy)
6. output unit propagation variable, if any.
7. output D if the current token is not D
8. output unassigned variable
For the output layer, we use [ToXRN] to denote the output logit [TOKEN]. Since the final output of the model is the token with the highest logit, we can implement output priority by assigning outputs higher priority rules with higher logits than lower priority rules. Specifically, compute the output logits vector using the output layer linear transformation as:
27 beat Csar + 26 boont G[uackTrack] + 25 buneat CUNSAT
+21 bbacktrack Cgr + 23 Beopy Ccopy 2 ConstPropvas +2 (1 l[t, 'D')) es + + (T,TT(00000 0), (0. 0), (1,1))r
30

---

Can Transformers Reason Logically? A Study in SAT Solving
Composing the Transformer In the above construction, we demonstrate how each operation be approximated by Self-attention MLP layer. We set the embedding dimension the of dimensions of all the intermediate values and allocate for every intermediate values a range of dimensions that's equal to the dimension of the variables. All dimensions are initialized to 0 in the positional encoding of the transformer except for the dimensions assigned to the positional index i. Similarly, only the dimensions assigned to the one-hot token representation are initialized the token embeddings. At each layer, the self-attention heads and MLP layers extract the variable values from the residual stream and perform the operations assigned to them at each layer.
Proposition C.11. There exists a transformer with 7 layers, 5 heads, O(p) embedding dimension, and O(p²) weights that, on all imputs
DIMACS(p, c), predicts the same token the output the above operations. Furthermore, let letz = 4c + p. 2 be the worst-case maximum context length required to complete SAT-solving, then all weights within poly(Icaa) and can be represented within Olp + log c) bils.
We only argue from high level why this is true due to the complexity of the construction.
The only intermediate values whose dimensions are dependent on are the vectors for one-hot encodings and storing binary encodings of clauses and assignments. They all have size 2p. Therefore, the number of total allocated embedding sizes is also O(p).
Furthermore, Appendix C.4 shows that all parameter values are polynomial with respect the context length and the inverse of approximation errors. Note that need only guarantee the final error is less than to prevent affecting the output token. Furthermore, poly(kata) and can be represented by O(log(ectz) O(p + log
choose all parameter values that they multiples of 0.5. As such, all parameters are within
C.8. Correctness of Construction (Theorem 4.5)
Note: This section assumes prior knowledge in propositional logic and SAT solving, including understanding of the DPLL algorithm. For a brief explanation of the notations in this section, please refer to ((Nieuwenhuis et al., 2005)). For more general knowledge, please refer to ((Biere et al., 2009)).
We prove that the above model autoregressive solves 3-SAT,,c p.e by showing that it uses the CoT to simulate the "Abstract DPLL Procedure".
C.8.1. ABSTRACT DPLL
In this section, provide description of abstract DPLL. Since the focus of this paper is not to show the correctness of the DPLL algorithm but rather how our model's CoT is equivalent to it, we only present the main results from (Nieuwenhuis et al., 2005) and refer readers to the original work for proof of the theorems.
Let M be an ordered trace of variable assignments with information on whether each assignment is an decision literal (i.e. assumption) or an unit propugation (i.e., deduction).
For example, the ordered trace 3d 12 4d 5 denotes the following sequence of operations:
Assume v33 = T - Deduce T1 T Deduce T22 F - Assume x. =
T - Deduce 2i T.
Let F' denote a SAT formula in CNF format (which includes 3-SAT), C denote a clause (e.g., V -x2 V 23), / denote a single literal (e.g., -22), and 1d denote a decision literal. Let M }= F denote that the assignment in M satisfies the formula F.
Definition C.12 (State the DPLL. Transition System). A state S E S in the DPLL transition system either:
The special states SAT, UNSAT, indicating that the formula satisfiable or unsatisfiable
A pair M F, where:
F' is finite set of clauses C₁ A C2 C. (a conjunctive normal form (CNF) formula), and
- .M is sequence of annotated literals I o l..... ... o 4 for some i e [n] representing variable assignments, where denotes concatenation. Annotations indicate whether literal decision literal (denoted by Id) or derived
31

---

Can Transformers Reason Logically? A Study in SAT Solving
through unit propagation.
We denote the empty sequence of literals by 0, unit sequences by their only literal, and the concatenation of two sequences by simple juxtaposition. While M is sequence, it can also be viewed as set of variable assignments by ignoring annotations and order.
Definition C.13 (Adapted from Definition 1 of (Nieuwenhuis al., 2005)). The Basic DPLL system consists of the following transition rules S + S:
UnitPropagate:
M is undefined in M.
MIFA(CCV))
Mol]IFA(CV])
if
Decide:
I or -l occurs in clause of F, | is undefined in M.
M|
Mor
if
Backjump
There is some clause C.V I' s.t. F FFCVI M --C, is undefined in M, 1' or -l' occurs in clause of F.
Mor . F
Moll
if
Fail:
M } F-C, M contains decision literals.
FIC
UNSAT
if
Success:
M
SAT
if M F
We also use S = St
denote that there exist S1, .g...., S such that S = S = - St. Also = S
denote that = 5' and S' is final state (SAT UNSAT).
Explanation of the Backjump Operation:
The Backjump operation allows the DPLL algorithm to backtrack to previous decision and learn new literal. In particular, F C V means that, for some clause C, every assignment that satisfies F must either satisfy (i.e., contain the negation of each literal in C') or contain l' an assignment. However, M }= -C, which means that M conflicts with and thus contains the negation of each literal in C, then if we want some assignment containing M to still satisfy F, then the assignment must also include the literal I' as assignment ensure that it satisfies C' v L', requirement for satisfying F.
In our construction, only consider the narrower set of BackTrack operations that find the last decision and negate it:
Lemma C.14. |Corrollary of Lemma 6 from (Niewwenhuis et al., 2005)] Assume that || = M ld N || F, the BackTrack operation:
There exists clause C in F such that M o 1d o N =
MoroN
Mo-
if
Ncontains no decision literals
always a valid Backjump operation in Definition C.13.
Definition C.15 (Run of the DPLL Algorithm). run of the DPLL algorithm on formula F a sequence of states So S ST such that:
SS is the initial state F
32

---

Can Transformers Reason Logically? A Study in SAT Solving
For each 0, ..... n 1, the transition S, = S41 is valid according the transition rules of the DPLL system in Definition C.13 (e.g., PropProp,,,t,, Decide, Backjump, or Fail);
Sy is final state that is either SAT or UNSAT
Note that the above definition simply the expansion of 0 == ST-
The following theorem states that the DPLL procedure always decides the satisfiability of CNF formulas: Lemma C.16. [Theorem 5 and Theorem 9 Combined from (Nieuwenhuis et al., 2005)] The Basic DPLL system provides a decision procedure for the satisfiability of CNF CNF formulas F. Specifically:
1. 0.01 1 F = UNSAT if and only if F is unsatisfiable.
2. 0 = SAT if and only if F is satisfiable.
3. There exist no infinite sequences of the form 0 F - S =
C.8.2. TRACE EQUIVALENCE AND INDUCTIVE PROOF
To prove that Transformer indeed simulates abstract DPLL algorithm, we argument of refinement: view Transformer construction with CoT state transition system and show that that transitions of this system "refines" that of the abstract DPLL state transition system:
Definition C.17. A transition system a tuple (S, T, 5o) where is the set of states, T S x S is the transition relation, and 8o is the start state. (s1, 52) E T, we say that there a transition from 81 to 82 and denote 81 = 82. Definition C.18. A run of transition system (S, T, sa) is (potentially infinite) sequence (so, s1,...) such that:
The sequence starts with Sp
At each step 2 0, (st, 1141) E T
The rum r halts it's finite sequence such that (so. $1, s.....,s)) such that s does not have any next transitions, ie.. There's no state s such that 88) E T
Definition C.19 (Refinement). Given two transition systems A (SA, (SA.TA TA. and B (Sp, TB. so)). Transition system A refines B if there is refinement mapping R C SA SB such that:
1. maps the initial state of the initial state of B: (8 8B0) R.
2. For every (R) E R, and every run r that contains 8A, r' (SA....) the suffix of starting from 84. There exists S SA s'3 E SB such that s'A r' and s')) TB.
Here, +4A denotes the reflexive transitive closure of =A
Proposition C.20. Given two transition systems = (S TA, 8 Ao) and B = (SB, BB0). If transition system A refines
B, and every run of B halts and ends in state sy.. then every run of A contains on 8 such that R(s)A) = Sgg.
To proceed with this argument, we first need to define the refinement mapping between our model's CoT and the states of abstract DPLL. Consider the following model input and CoT trace:
[BCS] -2 -4 -1 3 4 -1 0 -1 -3 -2 0 1 -2 -4
- 2
-2 4 0 [SEP]
D 1 -4
[BT] D 2 -1
Recall that [BT] denotes backtracking and D denotes that the next token is decision literal.
Note that the prompt input ends at [SEP] and the rest is the CoT produced by the model.
We want to convert this trace to state S = M F such that F' is the CNF formula in the DIAMCS encoding in the prompt input and M is the "assignment trace" at the last attempt (i.e., after the last [BT] token.). As such, M correspond to the
2 D -1 -4 portion of the trace and thus M 2d id 4 as described in Appendix C.8.1. We formalize this process as follows:
33

---

Can Transformers Reason Logically? A Study in SAT Solving
Definition C.21 (Translating CoT Abstract DPLL State. For any number of variables p N+, let V be the set of tokens:
V = { -i, i e [p] (D,, [SEP], [BOS), [BT), O, SAT, UNSAT }.
Define mapping fs V* - S [error} that converts sequence of tokens R V into abstract DPLL state follows:
1. If R ends with SAT UNSAT, then set MR(R) to SAT UNSAT accordingly.
2. Else R contains exactly one [SEP] token, split [SEP] into ADIMACS and Riace
3. Parse PDIMACS as a DIMACS representation of CNF formula F, assuming it starts with [BOS] and ends with C. parsing fails, set Ms(R)= = fail.
4. Find the last [BT] in Rirace and let Reureat be the part of Rirace after the last [BT]. If there's none, set Reurrent to R
5. Initialize an empty sequence M to represent variable assignments and set a flag isDecision t- False.
6. Process each token t in Reureett sequentially:
If t = D, set isDecision <- True.
Else if 7 is a literal, append I to M, annotated as decision literal if isDecision True, or as a unit propagation otherwise.
Reset isDecision False.
Else, set Mg = error.
7. Return the state M || F.
With the above mapping, we can specify the following properties of our Transformer construction based on logical relations between A and F:
Proposition C.22. Given input sequence 81:n E V such that [s(8)m) = M || F for which F is a valid 3-SAT formula and M is sequence of annotated literals. Let be the partial assignment corresponding M (i.e., removing annotation and order). Let D = (I E L F FAAA + 1} be the of literals that can be deduced through unit propagation. Let be the set of literals corresponding variables not assigned in A. Let Snt1 be the output of the Transformer model defined in Appendix C.7 when given 81sa input, then 8nt1 satisfy the following:
= = 8nt1 SAT
(M contains decision literals)
(F -A)
= 8n+1 UNSAT
(M contains decision literals)
A (F == -A]
= 8n+1 (BackTrack)
F) / -A) A (D + 0)
= 8nt1 E D
A (FE-))A 0) (sp #D)
= 8n+1 = D
(F A)A = 0) A (sp =
= 8n+1 E
We now present the inductive lemma:
Lemma C.23 (Inductive Lemma), For any P. N for any input FDIMACS E DIMACS(p, c) of length n, let F be the boolean formula in CNF form encoded in FDIMACS- Let be the model described in section C.7 with parameters p. c. the trace of when running the Greedy Decoding Algorithm with model A and input prompt 81.m FDIMACS- For every i E N+, if [s(81a44)) S and S & (SAT, UNSAT, error), then there exist j E N+ and S' such that S = S' and fs($1n4it1) S¹.
Let (8 $1m+1s....)
We now show trace equivalence between the model A and some instantiating of the abstract DPLL with a specific heuristic: Definition C.24. For any heuristic h S + L where L is the set of literals, let DPLL, denote an instantiation of the abstract DPLL algorithm that selects h(S) as the decision literal when performing Decide and only performs the Back Track operation for Backjump. ((S) is a valid heuristic DPIII, always abides by the Decide transition.
Lemma C.25, (Trace Simulation) There exists a valid heuristic S + for which the Transformer model A is trace equivalent to DPLL,, on all inputs DIMACS(p.
34

---

Can Transformers Reason Logically? A Study in SAT Solving
D. PARAT and Compiled Theoretical Construction
D.1. Supported Features and Operations
Our tool is designed to provide an intuitive syntax resembling standard numerical array manipulation, akin to NumPy, while supporting a diverse and extensible set of abstract operations. PARAT is capable of implementing
NumPy-like Array Syntax for indexing. arithmetic, and comparison.
Multi-Level Abstraction to enable low-level customization.
Multi-stage Evaluation Mechanisms to facilitate debugging and error localization
High Extensibility through structured class inheritance, promoting the addition of new features and operations.
Each intermediate "variable" an instance of the SOp hase class (name adapted from (Lindner et al., 2023)), and each instance sop of sOp is assigned a dimension daop E N and can be viewed as an abstract representation of an xx array where is the number of tokens in the input to the Transformer model. PARAT "program" basically a sequence SOps.
of array operations
Throughout this section, we refer to the indices along the first dimension of an sOp as "position" and refer indices along the second dimension as "dimension".
The "inputs" to a program are arbitrary positional encoding and token embedding variables, represented by the base class names PosEncSOp and TokEmbSOp respectively. For example, the Oneiott class represents the one-hot embedding of tokens and Indices represents the numerical value of index each position.
The rest of the program performs various operations that compute S0ps based existing ones. We provide implementations of basic building block operations including (but not limited to) the following:
Mean (g, k, v) Represents the "Averaging Hard Attention" operation. At each position i, this operation identifies all target positions j with the maximal value of g, k3 for I and computes the average of the corresponding V values.
sop [idx, :] Performs indexing using a one-dimensional index array idx, producing an sOp out such that out[i,j] = sop[idx([],]] for i [n] and e [dsop]. This mirrors NumPy's array indexing semantics.
sop[:, [ start: end] Extracts a slice of dimensions from sop, where start, end E [dsapl. resulting in new S0p of dimension end - start. This operation is analogous to NumPy slicing.
Element-wise operations such as sop1 + sop2, sop1 - sop2, sop1 * sop2, logical operations (& for AND, for OR), and comparison operations 2. <), following standard broadcasting rules.
As illustrative example, the following function returns one-dimensional sOp representing the position index of the closest token within set of target tokens:
def nearest_token
OneHot'okkmm vocab: List targets: List [str], indices: andices-indices Get the token ids of the target tokens target_tok ids [vocab. index (target) for target in targets] Get whether the current token is of the target tokens by summing the one-hot embedding target_token_embb
7
Concat ([tok_omb[:, target_tok_ice for target_tok_id in target_tokkidss)
In in_targets target_token embe sum (axis=1)
Pilter the indices to only include the target tokens siteere__indes indices in_targets return filtered_n indei.dex.. max ()
12
We present our full code implementing our construction for Theorem 4.5 using PARAT Appendix D.4.
35

---

Can Transformers Reason Logically? A Study in SAT Solving
D.2. Comparison with Tracr (Lindner al., 2023)
While Tracr also compiles RASP programs into Transformer weights, the RASP language is designed to provide concise description of the class of functions that Transformers easily learn As such, RASP has minimal syntax and is designed to represent relatively simple sequence operations such counting, sorting, etc. In contrast, our tool is designed to help construct theoretical constructions that implement relatively more complex algorithms.
In our preliminary attempt to implement our SAT solver model with Tracr, we identified several implementation inconve- niences and limitations of Tracr when scaling to more complex algorithms, which motivated the development of our tool. In particular:
Every "variable" (termed sop in (Lindner et al., 2023)) in Tracr must be either a one-hot categorical encoding or single numerical value. This constraint makes representing more complex vector structures highly inconvenient. Furthermore, each select operation (i.e., self-attention) accepts only single sop as the query and key vectors, whereas our theoretical construction often requires incorporating multiple variables as queries and keys.
In contrast, each variable in PARAT represents a 2-D array, which facilitates the implementation vector-based operations such as performing logical deductions as described in Lemma 4.7
In terms of parameter complexity, Tracr represents position indices and many other discrete sops with a one-hot encoding, allocating residual stream dimension for each possible value of the sop. In particular, compiling models with a context length of n requires ((n) additional embedding dimensions for each SOp that represents a position index. For each binary operation between one-hot encoded sops (such as position indices), Tracr creates an MLP layer that first creates a lookup table of all possible value combinations of the input sops. This results in an MLPP layer of (n )) parameters.
In contrast, our tool directly represents numerical values rather than working with token representations. For example, positional encodings only take up dimension of the residual stream, which drastically reduces the number of parameters for longer context lengths.
We would like to emphasize that our goal is not to replace Tracr or RASP, which have unparalleled simplicity and interpretability in describing well-studied sequence operations. The goal of our tool is to assist with creating implementations of theoretical constructions help verify its behaviors and investigate internal properties.
D.3. The Compilation Process
PARAT takes in an out variable that contains the computational graph the algorithm and outputs a PyTorch ((Paszke al., 2017)) model. The compilation process follows stages similar to those of Tracr:
1. Computational Graph Construction: When a user writes sop operations, each operation automatically creates dependency tree of all operations required for computing the resulting sop value.
2. Reduction to Base Operations: Each sop operation is reduced to one of 5 base classes: SelfAttention for operation that requires information from other token positions, GLUMLP for non-linear local operations, Linear for linear local operations, PosEncSOp for positional encodings, or TokEmbSOp for token embeddings. Sequential Linear operations reduced single operation through matrix multiplication and dependency merging.
3. Allocation of Layers and Residual Stream: appears later than its dependencies. This sorting is then used to assign SelfAttent and GLUMLP sops to Transformer layer numbers that comply with dependency constraints. Furthermore, each non-Linear sop is also allocated a portion of the residual stream equal their dgop size.
The computational graph is topologically sorted such that each sop
4. Model Construction and Weight Assignment: A PyTorch model is initialized based on the number of required layers, hidden size, and embedding size inferred from the previous steps. The computed weights for each sop are assigned to different model components based on their types. Notably, each Sel salffttentti ion sop corresponds to an attention head, and each GLJMLP sops corresponds to part of MLP layer with ReGLU activation.
36

---

Can Transformers Reason Logically? A Study in SAT Solving
Soft Hard Attention The reduction of Mean Sel induces inevitable numerical errors due Mean representing averaging strict subset of previous positions while Sel fättent on computes weighted average all previous positions via softmax. This error also affects other operations based Mean such position indexing, We control this error via an "exactness" parameter 3 that scales the attention logits, and Lemma C.6 shows that the error decreases exponentially w.r.t. 3.
Multi-Stage Evaluation To facilitate debugging, PARAT allows types of evaluations for every sop different stages of compilation.
sop- ract eval (tokens) evaluates sop on a sequence of input tokens without any numerical errors. This can be used to validate the correctness of the algorithm implementation as sop operations.
sop sop.come wwwcreteceee...ooo Leval (tokens) evaluates sop on an input sequence after reducing to the base classes at step 2 of the compilation process. This helps localize errors stemming from incorrect reduction of high-level operations to base classes.
Model evaluation This corresponds evaluating the Pytorch model after the full compilation process.
D.4. Code for Theoretical Construction
The following code is used to construct the Transformer specification passed as input to PARAT. To facilitate easier implementation, we interleave PARAT statements with Python and Numpy operations when appropriate. PARAT takes the return variable out as input and produces the theoretical construction discussed Section 5.1
def hearest_toke (tok_enb: One vocab: st [str], targets: (str), v: S0p List [S0p],
indices: PosEncSOp = indices)
if not isinstance list):
v [v]
target_tok_ide (vocab.index (target) for target in targets] cakent_tokens Concat aitok_embl:: target_tok_id] for target_tok_id target_tok_ids]) in_targets Linear on. (11, len )) fEltered_index (indices in_targets)
12
new_v
for vii in v:
15
if isinstance (v_i, s0p):
new_v.append
elif v_i =- 'target' v_i 'targets';
new
else:
raise ValueError UUnsupprrted value type')
return Mean (ones, filtered new_v, bos_weight=1)
26
def t (encodings: 50p, rum_vars, true_vec-(( (1, 0),
Salse_vec=fe (0, 1),
none_vec= (0, 0),
30
ones: Ones = ones):
mat np. zeros ((2 num_vars, num_vars))
true_vec_off- [tr]e_vec[0] none_vec[0], true_vec[1] none_vec[1]
false_vec_off [false_vec[0] none_vec[0], false_vec [1] none_vec[1])
for range (num_vars).
35
true_id =
false_id = num vars
mat [trueeii_a id, id] true_vec_off [0]
37

---

Can Transformers Reason Logically? A Study in SAT Solving
mat [true_id, false_id] _alse_vecooff[0
mat (false_id, _id, true_id] true_vect ve____ee_offffoo
mat [false_id] false_id] = =alse_vec_off[[]
blas zeroeros
num_vars)
bias inum_varsl vars] += rone_vecl0] bias Iun vars: = [one_vec|l]
44
return Linear [[encodings, onesl, np.hstack [mmat.,, bias. reshaps (-1, 1))))
49
def dpl1 (num_ vars, classes context_len, maan_cxactness=2,, nonsep_pente ponaapppppnalyy-2,,, zeturn_logs=False) -> Tuple1
53
S0p, List, Dict|str, s0pll:
vocab: List - ([str(i) for i in range num_vars + 1)]
[str(-i) for i in range (1, num_vars 1}] ['C', '[SRP] '[8T]', '[BOS]', 'D', 'SAT', "NNSAT')) idx: Dietlstr, intl (token: idx for idx, token enumerate (vocab) sop sop_logs: Dict/sta s0pl ()
cops.config "aaaaeeeaaaaaaeeeeee exactnesss] mean exactesss Initialize Base 50ps
tok_emb OnetootokkBmb (idx) named ("tok_emb")
62
nearest_sep nearest_
(tok_embttok_emb,
vocab-vocab,
targets-('0', '[SP]] '[ (iniicces, 'target (]) nnaedd
"nearest_sep")
The nearest (including seif) separator token and whether the previous separator token is '0', '[SK]]', [[UP]' '[87]' P_i_sep_P, b_0, b_SMP, b_HackTrack -
nearest_sepl;; named n ("p_i_sep_p"), nearest_sepp
named ("b_0")
nearest sep 2] na ("b_SEP)), hearest_sepi I,, 3] ("Maaddrk""a
76
The nearest 'D' token, which denotes the next token is decision P_i_ ncarest_token (tok_emb=tok_enb, vocab-vocab, targets=('D'), v=indices) .naeed ("p_i_D""
prev_pos = Id [d( tok_emb[:, (DDIIl] [indices 1]
p_i_spp The previcus (exciuding self) separator token p sep (prev_posl:, 0| is_bos) named("p) ("p_i_sep")
b decision: whether the current position is a decision literal b_decision prev_pos[:, 1] named ("b_deciiooo"""
The distance the nearest separator, i.e., the length of the current state d i sep = (indices -p_i_sep_p) (am__("d_i_sep""
90
Attention operation for representing the current ciause/assigument as bitvector of dimension P_i_sep_2 (p_i_se) + P_i_sep) ("p___ppp__se__"" vava tok_embl:, : num_ [rum_vars]... . _na
__i_pre Mean (p_sope-[p_i_sep__, P_i_sep, ones],
k_sops=[-ones: *ppip______ p_i_sep, -p -p_i_sep_21
v_sops=e_var i pree))
99
ii (r i pre
(indices p sep) .named i"r
100
The position of the previous (excluding self) separator roken
38

---

Can Transformers Reason Logically? A Study in SAT Solving
102
p_i_scp_min ____eppp____c__p) named
103
104
The same position in the previous state. This is used for copying from the previous state
min min sp_i_sep_nt min sep num_ b_SEP) ("p_ min")
107
108
The position of the Last decision in the previous state P_i_t_min P_i_ptp_i_sep__l named ("p_i___min")
109
I1I
Is the next token the literal resulting from backtracking?
112
b_ D. min (p_i min p min + 1) (ab___
113
Check if the current assignment satisfies the formula (See Theorem Precf for justification)
116
sat_q [r_i, ones]
117
sat_k [-r_i, (-ronsep_penaltyy
(1 tob_ idx (d'
118
sat_v is_bos
sat (saan sat_k, sat_y,
bos_wey wew.ighh-nossspeeeeea
0.5) named ("b_sat")
121
122
Check if the current assignment contracdicts the formula (See Theorem Proof for justification) unsat_q (r_i, num_vars, true_vec- (1, 0), false_vec= (0, 1), none_vec=(1. (1, 1)), ones]
126
unsat_k sat_k
127
unsat_v = 1 is_bos b p_cont
(Mean (unsat_q, unsat_k, unsat_V,
0.5) named ("b_edd""ccoor ("b_cont") b_copy_p (p_i_min (p_i_sep_p 1)) named ("b_copy_p")
bos_we weeightt-oosse_peneeee
130
131
132
Unit Propagation
135
up_q unsat_q
136
up_k - unsat_k
up num clauses i
up Mean (up_g, kp up_,, bos wes.eiiht-nomeeppenalle 1.5)
139
140
141
up =
GLUMLP (act_sops= uo_up (rrii num_vars,
true_vec- (1, false_vec-(( (1, 1),
144
145
noce_vec= (0, )))))
146
GLUMLF (act_sops= up_up namedd "re_up_new")
11)
148
149
150
Heuristic for decision literal selection: Pind the most common literal in remaining clauses heuristic_q (r num vars, true_ vee-vee= 1),
153
false_vec= -10), none vone_vec=(0) (0, 01), ones]
154
heuristic_k = [r_i, "moosse_ppnnatty houristic_y = r_i heuristic_o SelfAttention (herisstie,,, heuristic_k, heuristic_v)
(1 tok_embl:, idx('O'II)
155
157
158
Whether the current essignment contains no decision literal no decisionn (p_i_D <= P_i_sep) named ("b_no_decision")
159
Whether Backtracking is finished BT finish ((p i min piimin b BackTrack)
162
163
164
The negation of the last decision literal in the previous state BT - ( 11, num_vars-num_vrre
39

---

Can Transformers Reason Logically? A Study in SAT Solving
true_vec- (C, 1), false_vec- (1, 0), none_vec= (0, о))
167
168
The next index in the previous state for copying index""
169
p_i_min mii_min_ddexx index = (p_i_min + 1)
The token in the previous state for copying e_cop tok_emb ip_i_min_indees named (*e_copy")
172
173
Whtther we 'vee decided that the formula is UMSAT unsat (b_no_ deediccioonn b_cont) named (*b unsat")
176
177
Whether we ro nogativing the last decision literal for backtracking b b_bccktrack = (b_D_min & b_BackIrack) named ("b_backtrack")
178
Whether we we' copying tokens from the previous state copoy (b_copy_p (1 b_Br_finish) named ("b_copy")
181
182
183
b_ BT Boken (b_cont (1 tok_embli, idxl ' [BT] 111)) not D
tok embl i;, id'I'D'Il named ("b_net_"""_" _ot__") unassigned t (r (r_i, num vars, true vec= (0, 0), false_vec- (0, C), none_vec- (1, ) named ("e_unassigned")
185
186
187
out CPOutput (len (vocab),
(b__at, idx [SAT'), 16), (b_unsat, idx['UNSAT'), 1 15), (b_ (b_BT_token, (b_backtrack, Fad(c_BT, (vocab),,, [dx('1)), 12),
190
191
'1, 14),
192
(b_copy, e_copy, 6),
(None, Pad(e_up, len (vocabl, (d'(' 4), (b_not_D, id'I, 3), (None, Pad (e_urassii + heuristic_o, out_dim-len (vocab), start_dimmicx(""1)) 1)1)
195
196
199
return out
40


Reviews:
[{"review_id": "0L5MBbdBBx", "reviewer": "Reviewer_y8ew", "summary": "The authors present a theoretical foundation and proof that it is always possible to construct an optimal decoder-only transformer that is capable of exactly simulating the DPLL search and solving any 3-SAT task with greedy decoding that uses CoT reasoning steps and backtracking. The authors show that given any 3-SAT input with p variables, it is possible to create a set of modules (all of which are separate parts/layers and together comprise a complete transformer) with each simulating a portion of the DPLL search process. This reveals that transformers are capable of optimally solving any 3-SAT task (which is NP). The paper also shows that for p variables and c clauses, there exists a transformer that can optimally solve the 3-sat problem with no more than p*(2p+1) CoT iterations for a model with L = 7 layers, 5 heads and O(p^2) parameters. Additionally, the authors show that even pretrained transformers can be trained to solve 3-SAT tasks where the number of variables is close to the amount of variables seen during the training. Although, out of distribution generalization w.r.t. the amount of variable in a 3-SAT problem is still non-trivial for transformers.", "questions": "", "limitations": "", "rating": 5, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We’re very grateful for your devoted time and careful review of both the main paper and the appendix. We’re also very glad that you liked the contributions of our paper and consider the proof and description in the appendix rigorous and helpful. \nWe would like to address your comments regarding the difficulty of understanding the proof sketch and your opinion of possible improvements to its clarity, suggested below:\n## Clarity Improvements to the Proof Sketch\n**Swapping Preliminary Section on Transformers with Appendix C.1 on 3-SAT** (also suggested by reviewer sNWz): From your reviews as well as suggestions from reviewer sNWz, we believe that the most unclear part in the main paper is likely regarding 3-SAT operations and DPLL. As such, we will swap out the detailed mathematical definitions of the Transformer architecture in section 2 with descriptions of 3-SAT in Appendix C.1\n\n\n**Organize Proof Sketch around Major Steps in the Construction:** For Section 4, we would like to organize the sketch around the multiple major steps of the Transformer model? i.e., we organize into the following paragraphs:\n\n Step 1: Summarize Clauses and Assignments as Binary Vectors: where we introduce definition 4.6 and explain how the binary encodings can be computed by summing up one-hot encodings in each clause using the attention mechanism of the Transformer\n\n Step 2: Perform Parallel Logical Operations over Clauses: where we introduce Lemmas 4.7 and 4.8 and explain how to determine Satisfiability, Conflict, and Unit Propagation\n\n Step 3: Next Token Prediction: where we have a description on how the final token is decided based on the results calculated in the previous layers\n\n\n## Example on line 1355\nThank you for your careful reading of the appendix. After careful checking, the example is indeed wrong. The correct solution should be:\n`[SEP] D 2 D 1 -4 3 [BT] D 2 -1 -4 [BT] -2 D 3 D 4 1 SAT`\nWe will also update this in the paper.\n## Questions\n> Can the authors provide insights into the characteristics of SAT instances where the model’s CoT length approaches this worst-case behaviour and how often such instances can occur realistically?\n\nWe expect all instances to be lower than this bound, but we do not know of tighter upper bounds that are strictly proven. The number of CoT steps required is dependent on many factors, including the heuristic used to select the next decision (assumption) at each iteration, etc. Providing tighter theoretical upper bounds on solving different types of SAT formulas is an active direction of research in the SAT solving community (e.g., see [1] Section 1.5). We instead used a large upper bound that is guaranteed to be true on all instances and heuristics.\n\n> Can it be assumed that having more compute during test-time would allow the models better generalization w.r..t. the number of variables? \n\nWe do believe this to be true according to relevant literature on practical LLMs, where longer CoT leads to better reasoning performance. However, it’s difficult to empirically test this hypothesis in our setting since there isn’t a reliable way to increase test-time computation for custom-trained 3-SAT models. In particular, our models are deterministic and do not support additional prompts to elicit longer reasoning chains. Your suggestion is indeed an insightful and promising direction for future work.\n> What happens as the CoT gets longer? Do the models collapse and start repeating explored patterns? Do they hallucinate?\n\nYes. We can investigate this phenomenon by observing how models trained on large (11-15) instances behave on smaller instances. For example, on a 3-SAT problem with 5 variables, the model outputs: (recall that D represents “Assume” and [BT] represents “BackTrack” according to Appendix C.1)\n\n`D -4 D -1 -5 2 3 D [BT] D -4 D -1 -5 2 3 D -4 D [BT] D -4 D -1 -5 2 3 D -4 D -5 SAT`\n\nThe model can be considered to be hallucinating since the final D at the end of the first attempt should never occur. Similarly, at the final assignment before SAT, both -4 ($x_4=F$) and -5 ($x_5=F$) occurred 2 times, which shows that the model starts repeating explored patterns. Both of these phenomena are quite common when the CoT is longer than normal.\n\nIn another test sample of 5 variables, the model outputs:\n\n`D -4 D -3 1 2 -5 -4 -18 17 -26 SAT`\n\nWhich hallucinates variables that do not exist in the formula (and also outputs -4 twice).\n\nWhat’s more interesting is that the models still have high SAT vs UNSAT accuracy even when these hallucinations/repetitions occur and our test data explicitly removes statistical evidence on SAT vs UNSAT. This can be seen from Figure 3 (right) where the SAT vs UNSAT accuracy remains high even when the Full Trace Correct accuracy falls off significantly. It seems that the trained model still has ways to “guess” the correct SAT vs UNSAT even with a CoT that’s not fully correct and longer than normal.\n\n[1] On The Unreasonable Effectiveness of SAT Solvers", "claims_and_evidence": "All of the claims are valid and theoretically proven or empirically evaluated. The theoretical background given for the paper is rather extensive and covers a broad spectrum of non-trivial decoder-only transformer decompositions into modules that can be viewed as a deterministic component of the DPLL (PARAT).", "methods_and_evaluation_criteria": "The only empirical components of the paper explore trying to train a pre-trained decoder only Transformer to solve the 3-SAT task. The evaluation is straightforward by looking at the explicit accuracy of the SAT/UNSAT labels produced after CoT and Backtracking.", "theoretical_claims": "The theoretical claims of the paper are rather extensive, maintaining that given a set of variables p, it is always possible to construct a decoder-only transformer that would be able to exactly and optimally solve any 3-SAT problem akin to DPLL while using CoT reasoning and backtracking. All of the claims are adequately supported, albeit It must be mentioned that without reading the complete appendix it is impossible to understand the main idea and components of the paper. My only problem with the paper is the way that the idea is presented in the main part of the paper.", "experimental_designs_or_analyses": "The experimental design is straightforward and tries to validate whether arbitrary pre-trained decoder-only transformers can learn to solve 3-SAT problems. The accuracy for SAT/UNSAT final outputs shows that learning the task is feasible, but generalization outside of the number of variables present in the training set is non-trivial and complicated.", "relation_to_broader_scientific_literature": "The paper explores a fundamental transformer capability, revealing that transformers are able to solve the 3-SAT task, which falls in line with research exploring the theoretical limitations and expressiveness of the transformer architecture.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "The main weakness is the way that the method is explained in Section 4. Most of the explanations and flow seem handwavy and not rigorous. However, their counterparts in the Appendix more than cover the need for rigour. I would still maintain that changing the way the explanation flows in favour of more strict but understandable transitions would be easier for the reader to understand.", "other_comments_or_suggestions": "I think the solution for the example on page 25, line 1355 in the appendix for the proposed 3-SAT example is wrong.", "questions_for_authors": "1) The compiled model (constructed) achieves perfect accuracy on 3‑SAT instances. Given that the worst-case CoT length is theoretically exponential (because 3-SAT is NP), can the authors provide insights into the characteristics of SAT instances where the model’s CoT length approaches this worst-case behaviour and how often such instances can occur realistically?\n\n2) Given that the amount of chain of thought tokens is massively lower than the theoretical bound, can it be assumed that having more compute during test-time would allow the models better generalization w.r..t. the number of variables? What happens as the CoT gets longer? Do the models collapse and start repeating explored patterns? Do they hallucinate?\n\n### Post rebuttal comments\n\nI feel all of my concerns have been addressed after the rebuttal. Increasing the score.", "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": "g4aBIKw8bP", "reviewer": "Reviewer_Q1EZ", "summary": "This paper investigates the deductive logical reasoning capabilities of decoder-only Transformers. The author(s) opt for 3-SAT problem as a representative example of logic reasoning task and use Transformer model to achieve reasoning via Chain-of-Thought (CoT).", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We greatly thank you for the detailed comments and feedback. We appreciate the reviewer’s careful reading and insightful concerns. \nWe seek to clarify certain potential logical misunderstandings, hoping to address your identified concerns regarding the theoretical results. Most importantly, **the correctness of Theorem 4.5 is justified by the proof in Appendix C, rather than the experimental results.**\n\n> Theorem 4.5 and Theorem 1.1 cannot hold based on the experimental results, where the Transformer models fail to generalize to instances with more than 12 variables.\n\n> Mismatch between theorem and empirical results. Theorem 4.5 claims …\n\nWe fully appreciate the reviewer’s detailed review. However, we kindly clarify that Theorem 4.5, which shows the existence of a Transformer model that solves SAT, refers explicitly to the Transformer weight configuration rigorously defined in Appendix C. The empirical models, which showed limited generalization beyond 12 variables, were trained from data and thus had fundamentally different weight configurations. \nThe configuration corresponding to Theorem 4.5 and described in Appendix C.6 is also implemented and corresponds to the \"Compiled\" results presented in Figure 3 and Section 5, achieving perfect accuracy on all tested instances. Again, we note that while such perfect accuracy is implied by Theorem 4.5, no amount of empirical tests can justify the correctness of Theorem 4.5. The experiment results for the compiled model only serve as a “sanity check” on smaller instances. Instead, the correctness depends on the Proof presented in Appendix C.\nThus, the empirical limitations in generalization of the trained models and the number of variables in the tested formulas do not contradict our theoretical claims.\n\n> Lack of formal justification for model hyperparameters (L=7, H=5). It seems that Appendix C.6 is the corresponding proof…\n\nWe would like to clarify that these hyperparameters are indeed rigorously justified through the theoretical construction explicitly presented in Appendix C.6. Specifically, the configuration of the theoretical construction is provided between lines 1363 and 1469, detailing how each of the 7 layers explicitly contributes to achieving the theoretical result. The 5 heads stem from the fact that the operations in layer 5 require 5 attention heads to complete, and the number of attention heads must be the same across all layers by definition of the Transformer architecture. The operations are described at a high-level, and each individual operations have a corresponding lemma in previous sections on how the operations can be represented as attention or MLP layers. Also, we do not claim that the 7 layers and 5 heads are minimal for SAT solving, but rather an upper bound on the number of layers and heads required to solve 3-SAT.\n\nLine 1358 mentioned in your review describes the “embedding layer” of the construction, which converts each token to input vectors before layer 1. \n\nOn the possibilities of ablation studies, while ablation studies are typically valuable in empirical research contexts for determining the influence of each component of a machine learning model, they are not applicable to theoretical proofs.\n\n>  while Appendix C.6 appears to provide a detailed analysis of Theorem 4.5, this link is not explicitly stated in the main text.\n\nIn lines 238-239 of the main text, we mentioned that the proof of Theorem 4.5 is in Appendix C, and Appendix C.6 is not only a “detailed analysis” of Theorem 4.5 but a part of its proof that describes the construction. \n\n> The additional experiments in Appendix B are not clear.\n\nThank you for pointing out the missing references to the Figures from the main paper! For the experimental result in the appendix, Figure 5 corresponds to question 3, “How does error induced by soft attention affect reasoning accuracy?” on lines 322-323 (right), while Figure 6 adds the experimental results on the 2 remaining evaluation datasets, Random and Skewed, compared to Figure 3 in the main text. Thank you for pointing out the missing references to these figures in the main text. We will update the paper to clarify and add references to the additional experiment results.\n\n> Does it suggest that self-attention-based models are inherently limited in practical scenarios?\n\nOur work focuses on advancing our theoretical understanding of the capabilities of Transformers in logical reasoning rather than how Transformers can be used for practical SAT solving. Our results show that given the number of variables and clauses, it’s possible to construct a Transformer model that solves 3-SAT. These models indeed have efficiency limitations compared to traditional SAT-solvers like CDCL and DPLL. Having that said, it might be possible to design for efficient SAT-solving mechanisms by exploiting the parallelism introduced in Lemma 4.8 and GPU architectures.", "claims_and_evidence": "Yes.", "methods_and_evaluation_criteria": "Yes.", "theoretical_claims": "Theorem 4.5 and Theorem 1.1 cannot hold based on the experimental results, where the Transformer models fail to generalize to instances with more than 12 variables.", "experimental_designs_or_analyses": "All experiments are conducted on very small-scale instances, where the number of variables in the 3-SAT problems is fewer than 20.", "relation_to_broader_scientific_literature": "This paper is the first work to theoretically analyze the ability of Transformer models to solve 3-SAT problems. It is related to the literatures about AI/LLM reasoning.", "essential_references_not_discussed": "No", "other_strengths_and_weaknesses": "Strengths:\n1.\tThe paper provides a thorough theoretical analysis of the ability of Transformer models to solve 3-SAT problems, offering valuable insights into their logical reasoning capabilities. \n2.\tThe approach of tokenizing 3-SAT problems and employing a decoder-only Transformer to solve them is novel.\n\nWeaknesses:\n1.\tLack of formal justification for model hyperparameters (L=7, H=5)\nTheorem 4.5 asserts the existence of a decoder-only Transformer with L=7 layers and H=5 heads capable of solving 3-SAT. It seems that Appendix C.6 is the corresponding proof. However, Line 1358 seems like a hypothesis of the function of the embedding layers. Is there any theoretical proof of this model configuration or even ablation study of each layer?\n\n2.\tMismatch between theorem and empirical results. \nTheorem 4.5 claims universality (\"for any p, c ∈ N+\"), but the experiments only validate the construction on small instances (p ≤ 20 variables). The results show that Transformer models cannot be generalized to the instances with more than 12 variables.", "other_comments_or_suggestions": "The main body of this paper is well-organized, but the appendix is not clear. For example, while Appendix C.6 appears to provide a detailed analysis of Theorem 4.5, this link is not explicitly stated in the main text. The additional experiments in Appendix B are not clear.", "questions_for_authors": "1.\tplease clarify weakness 1 and 2 \n2.\tThe Transformer model also fails to achieve 100% accuracy on small instances (p ≤ 20), whereas traditional SAT solvers (e.g., DPLL, CDCL) solve such problems with perfect accuracy. Does it suggest that self-attention-based models are inherently limited in practical scenarios?", "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": {"ethical_review_concerns": "N.A."}}, {"review_id": "rSYDw0XaaU", "reviewer": "Reviewer_KAAL", "summary": "This paper studies the deductive logical reasoning capabilities of decoder-only Transformers. As claimed by the authors, many researchers reject the idea that LLMs are capable of reasoning, and there is little understanding of the fundamental limitations in the reasoning abilities of Transformer models. In this work, the authors claim that they prove by construction that decoder-only Transformers can solve 3-SAT in a non-uniform model of computation, and the instantiated Transformer corresponding to the theoretical construction can perfectly solve 3-SAT instances. The authors conduct experiments to evaluates the model’s performance and ability to generalize to formulas with a different number of variables than seen during training.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your devoted time in reviewing the paper. We're glad that you found the writing and experimental results of our work satisfactory.\n\n> To verify the logical reasoning capabilities of decoder-only Transformers, It would be good to add research on other types of SAT problems.\n\nThe suggestion is highly insightful! Including more complicated SAT instance structures beyond CNF formulas may reveal further insights into more complicated Transformer reasoning, especially when processing hierarchical data. This is currently beyond the scope of this work, and we would certainly look into these directions in future work. For the present work, since it’s well known that all SAT formulas can be converted into 3-SAT in polynomial time, and we are the first theoretical work investigating the capacity of Transformers in formal logical reasoning, we believe that our current contributions are sufficient for the current manuscript.\n\n> Beides random instances, how does the method perform on industrial instances (e.g., those instances from SAT Competitions)?\n\nRegarding your question, we fully acknowledge the importance and impact of practical SAT solving, but we would like to clarify that **our goal is to advance our theoretical understanding of the reasoning capability of Transformer models. Practical SAT solving is orthogonal to this work and our goal.** We chose 3-SAT as the theoretical basis for our study because it’s a fundamental NP-complete problem in complexity theory that represents deductive logical reasoning. It is unlikely that our model will have any practical advantage over traditional SAT solvers. The DIMACS encoding and CoT of practical instances are significantly longer than the context lengths of our models. Therefore, we did not use any practical SAT benchmarks for evaluation.\n\nWe’re happy to answer any additional questions you may have regarding our work. We also sincerely hope that you can evaluate the theoretical aspects of contributions in more detail if possible.", "claims_and_evidence": "The claims made in the submission are supported by clear and convincing evidence.", "methods_and_evaluation_criteria": "Proposed method make sense for the problem. But for the instances in the experiment, the number of variables is small.", "theoretical_claims": "Yes.", "experimental_designs_or_analyses": "The experimental design to evaluate the effectiveness and generalizability of the method is reasonable.", "relation_to_broader_scientific_literature": "The paper discusses and proves the logical reasoning capabilities of decoder-only Transformers in the 3-SAT problem, which provides reference for the view that \"LLM can reason\".", "essential_references_not_discussed": "N/A.", "other_strengths_and_weaknesses": "## Strengths:\n1. The paper is generally well-written, with clear explanations.\n2. The code of the method is available.\n3. Experimental results are satisfactory.\n\n## Weaknesses:\n1. To verify the logical reasoning capabilities of decoder-only Transformers, It would be good to add research on other types of SAT problems.", "other_comments_or_suggestions": "N/A.", "questions_for_authors": "Actually, SAT is so facinating because of its usefulness in real-world applications. Hence, it is more important to adopt industrial instances  (e.g., those instances from SAT Competitions) in your study, rather than random instances. This significantly reduces the signficance of this work. Beides random instances, how does the method perform on industrial instances (e.g., those instances from SAT Competitions)?", "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": "f75yacGQXI", "reviewer": "Reviewer_sNWz", "summary": "This paper investigates whether transformers can solve 3-SAT problems by using COT reasoning to simulate backtracking-based search algorithms like DPLL. The authors theoretically demonstrate that this approach is feasible. Empirical evaluations show that: 1) language models using COT can be trained on reasoning paths to perform deductive reasoning effectively, and 2) the trained models struggle to generalize to problems with unseen sizes, such as different numbers of variables.\n\n### Update after Rebuttal\n\nThank you to the authors for the response and clarifications.\n\nDespite the rebuttal, I still share the concerns of other reviewers regarding the lack of convincing evidence for the method's applicability in industry-scale settings. This limitation currently narrows the work's potential impact.\n\nConsequently, I am maintaining my initial score.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their detailed feedback. We’re grateful for your acknowledgment of the soundness of our construction and the relevance of the experiments. We would like to focus on your primary concern regarding novelty compared to Turing Completeness (TC) results.\n\nWhile we agree that TC of Transformers with CoT implies that, in principle, simulating algorithms like DPLL is possible, we believe this perspective overlooks the core contributions and significance of our work. Allow us to elaborate:\n\n## Beyond Turing Completeness: The \"How\" Matters\nOur work, like previous works on Transformer expressiveness, aims at advancing our understanding of the capabilities and mechanisms of Transformer models in reasoning. Previous TC results rely on step-by-step simulations of single-tape Turing Machines (TM), which are theoretically foundational but don't well-explain how logical reasoning is performed internally in Transformers. I.e., Many reasoning phenomena of LLMs remain poorly explained by TC alone.\n\nConsider an analogy: Mathematical theorem proving (e.g., solving IMO problems) can be framed as search problems over LEAN proofs. If LLMs are TC, does this make their success on math benchmarks unsurprising or non-novel? We argue no. The interest lies in how LLMs solve these problems – potentially using more efficient, structured reasoning mechanisms than TM simulation.\nOur work moves beyond TC by asking how a Transformer can efficiently simulate a specific, non-trivial logical reasoning procedure (DPLL for 3-SAT) using its inherent architectural features. We provide an explicit construction and demonstrate a concrete CoT mechanism.\n\n## Novelty in Parallelism via Attention\n\nAs highlighted in your review, a key novelty is demonstrating how Transformers use parallelism effectively. **We provide the first theoretical evidence that the attention mechanisms in Transformers can support parallelism for logical reasoning.** This suggests that the Transformer models can be particularly suitable for deductive logical reasoning in large contexts. In particular, Lemma 4.8 shows that a single Transformer head can perform satisfiability checking, conflict detection, and unit propagation, respectively overall all clauses in parallel. \n\n## Novelty in CoT Efficiency and Structure\n\nWhile the reduction in CoT tokens compared to TM simulations might seem “reasonably expected”, anticipated theoretical results still significantly benefit from formal proofs—analogous to widely believed mathematical conjectures (e.g., P ≠ NP).\n \nOur CoT simulates DPLL at an abstraction level higher than TM emulation, explicitly representing logical reasoning steps of assumption, deduction, and backtracking. \n\nFurthermore, we formally provide an explicit upper bound (p·2^(p+1)) on CoT length (Theorem 4.5), a contribution extending beyond mere TC results. In particular, such upper bounds for TC results are unknow for 3-SAT.\n\n## Preliminary Section Clarity\nRegarding your suggestion on swapping the preliminaries section for background on 3-SAT and DPLL, this is indeed a greatly helpful suggestion for readability, and we will certainly do that during revision. In particular, we will swap the preliminary section on transformers with Appendix C.1 on 3-SAT after rewriting for brevity.\n\n## Questions\n\nThe main connection between the experimental results is the shared Chain-of-Thought design. Our theoretical construction provides a specific CoT structure. The experiments then investigate whether Transformers can learn this structure from data. The strong intra-length OOD generalization (Table 1) suggests that training on this theoretically-grounded CoT does allow the model to learn a robust reasoning procedure applicable across different data distributions, overcoming limitations seen in prior work where models trained with CoT relied on statistical shortcuts [1].\n\nWe agree that additionally investigating the accuracy of models of different sizes trained on 3-SAT problems with Chain-of-Thought is an interesting and insightful direction of experimental investigation according to the $O(p^2)$ scaling of our theorems and aligns with the “scaling law” line of research. However, such experiments are computationally beyond our theoretical focus and available resources.\n\nAs you mentioned in the review, Transformer models would introduce significant overheads compared to modern SAT-solvers. \nHaving that said, it may be possible to develop efficient parallelized SAT-solver operations such as unit propagation, satisfiability checking, and conflict detection on GPU architectures using the insights from Lemmas 4.7 and 4.8. Our construction may also be used as a differentiable SAT-solving component that allows LLMs to formulate the underlying logic within natural language reasoning traces as SAT formulas and use traditional SAT solvers to perform more reliable reasoning. \n\n[1] Zhang, et al. On the paradox of learning to reason from data. IJCAI '23", "claims_and_evidence": "The claims are generally well-described within the context and supported by both theoretical and empirical evidence. The authors provide a formal proof that transformers can solve 3-SAT via COT reasoning, and demonstrate its correctness empirically. Their experiments show strong in-distribution generalization but limited generalization to different input lengths.\n\nHowever, the authors could elaborate on the relationship between their theoretical construction and how LLMs learn in real-world environments, as their construction requires specific weight configurations that may not naturally emerge during training procedures.", "methods_and_evaluation_criteria": "The experimental setup suitable for the research questions. While the Turing completeness of chain-of-thought reasoning guarantees that a model can be constructed (likely with predefined parameters) to simulate DPLL, the more practical question is whether a model can learn to perform such operations from data (i.e., reasoning paths). The authors effectively designed and conducted experiments to investigate this question.", "theoretical_claims": "While I have reviewed but not verified the proofs in detail, their construction appears sound. \n\nIt's noteworthy that the authors managed to introduce parallelism into the standard backtracking procedure, which is a key difference between COT and traditional rule-based reasoners. The parallel processing capability inherent in LLMs offers potential advantages over sequential rule-based systems.", "experimental_designs_or_analyses": "They are relevant to the research problem. The authors designed their evaluation datasets to avoid statistical shortcuts, enhancing the credibility of their results.", "relation_to_broader_scientific_literature": "However, in my opinion, the ideas and findings have limited novelty, as they are, in some ways, a straightforward implication of existing literature. Since the Turing completeness of COT has been well discussed in previous research, it is not surprising for the community to see that COT can simulate a backtracking procedure like DPLL. From this perspective, I doubt whether this paper can contribute significantly to the research community.\n\nIn Section 2, the authors argue that their method requires a \"drastically reduced number of COT tokens.\" It seems not to be a fair comparison, as existing literature focuses on single-tap TMs, which are typically used as a basis for theoretical analysis rather than actual tine-grained complexity analysis. Theoretically, it is reasonable to expect that the numbers can be reduced when considering the properties of COT, the 3-SAT problem, and DPLL. However, this advantage is unlikely to extend to practical use cases, as using COT to simulate DPLL would introduce much overhead compared to standard rule-based reasoners.\n\nThe experiments design largely overlap with other \"learning to reason\" experiments in previous literature, and the results are generally intuitive. The authors fail to provide an in-depth analysis of how the learned model relates to their theoretical construction.", "essential_references_not_discussed": "No.", "other_strengths_and_weaknesses": "None", "other_comments_or_suggestions": "In my opinion, the preliminary section could be rearranged, as readers at ICML are likely to be relatively familiar with transformers and can easily find additional materials if needed. Most of the content, particularly the formulas related to transformer blocks, is not utilized in subsequent sections. Instead, I recommend including a brief introduction to backtracking-based search algorithms, such as DPLL, which is used in the paper, to enhance readers' familiarity with the topic. The authors may also consider elaborating on the COT aspect as well.", "questions_for_authors": "1. For the results presented in Section 6.2, the authors argue that the failure to generalize to arbitrary lengths is consistent with their theoretical result, which states that the size of the transformer depends on the number of variables. However, this does not align well with the experimental design. The authors only experimented with varying problem sizes, rather than varying the sizes of the transformers themselves. Could the authors clarify this discrepancy?\n\n2. How does the efficiency of the transformer-based SAT solver compare to specialized SAT solvers in terms of computational resources and solving time? Or, how might the proposed method collaborate with existing SAT solvers to enhance SAT solving?", "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": {"ethical_review_concerns": "N/A"}}]

Author rebuttal:

Meta-review: A subset of reviewers and the AC agree that the paper makes interesting and novel contributions to the theoretical study of Transformer-based reasoning for 3-SAT.  Two reviewers request experimentation on larger scale problems, but I agree with the authors that such requests are orthogonal to their key claims and contributions that are focused on theoretical understanding and validating its reduction to practice.  

While the techniques and results are perhaps not surprising, the results themselves are novel and the quality of the discussion and presentation coupled with some critical insights (e.g., soft vs. hard attention differences) make this paper a solid and timely contribution on the topic of logical reasoning and Transformers.  

During revision, the authors should make an effort to incorporate clarifications and helpful rebuttal discussion in their reviews.  I also include below some critical feedback that the authors should consider as they prepare their final version:

1. The paper has two divided parts: first, a hand-crafted compiled model that does perfect inference on tiny SATs, utilizing CoT as a “tape” for arbitrary memory size ( which grows O($p \times 2^{p+1}$), which is actually $\approx$ inference speed). In the end, it’s basically a manually written matrix program construction running in exponential efficiency, which does not seem to be a surprising result for 3-SAT although bounding the number of layers, heads, and parameters is a useful technical contribution.  The authors' current discussion of contributions focuses more on what they technically achieve and less on what parts are surprising and likely to impact downstream use of these results.
2. The authors claim that the compiled model is a standard Transformer, but it uses hard attention. In the appendix, they actually show that softer attention doesn’t really work, so their other claim that their study reveals “LLM + CoT can learn SAT” requires some qualification in my view.
3. The authors' second approach to train a model (soft attn Llama) obviously yields a different algorithm than their compiled version.
4. Overall, the theoretical approach (compiled model) isn't new, but the domain-specific insights and bounds for 3-SAT are interesting, the attention discussion is important and useful, and hence the paper should generally be informative for the community interested in SAT-oriented logical reasoning with Transformers.
Decision: Accept (poster)