Can Transformers Reason Logically? A Study in SAT Solving

## Abstract

Abstract We theoretically and empirically study the logical reasoning capabilities of LLMs in the context of the Boolean satisfiability (SAT) problem.
First, we construct a decoder-only Transformer that can solve SAT using backtracking and deduction via Chain-of-Thought (CoT). We prove its correctness by showing trace equivalence to the well-known DPLL SAT-solving algorithm. Second, to support the implementation of this abstract construction, we design a compiler PARAT that takes as input a procedural specification and outputs a transformer model implementing this specification. Third, rather than programming a transformer to reason, we evaluate empirically whether it can be trained to do so by learning directly from algorithmic traces (“reasoning paths”) of the DPLL algorithm.

## 1 Introduction

Transformer-based Language Models (LLMs, Vaswani et al. ()) have demonstrated remarkable success in a wide range of tasks framed in natural language, especially when using prompting techniques such as Chain-of-Thought (CoT, Wei et al. ()). On the other hand, even the most advanced LLMs face challenges in reliable multi-step reasoning, frequently hallucinating towards nonsensical conclusions (Kambhampati et al. ()). Evaluating progress on logical deduction in language models remains an ongoing challenge as researchers have continued to disagree on even a reasonable definition of what constitutes “reasoning.”

This paper focuses on the question of LLM reasoning capability in what we believe is the simplest and most mathematically precise setting: the Boolean satisfiability problem (SAT, Cook ()). SAT problems provide an excellent starting point for studying the reasoning ability of LLMs given that (a) natural language often encodes Boolean logic, and (b) we already have many useful algorithms that implement logical deduction to solve SAT problems Biere et al. (). Notably, notwithstanding the NP-completeness of SAT, humans implicitly solve simple boolean satisfaction problems in their daily lives; scheduling a multi-person meeting across time zones, for example.

In this work we aim to rigorously investigate Transformers’ multi-step reasoning and backtracking capability in solving formal logical reasoning problems, and we demonstrate through a theoretical construction that decoder-only Transformers can reliably decide SAT instances.

###### Theorem 1.1 (Informal version of Theorem 4.5 ) .

For any $p,c\in{\mathbb{N}}^{+}$, there exist a decoder-only Transformer with $O(p^{2})$ parameters that can decide all 3-SAT instances of at most $p$ variables and $c$ clauses using Chain-of-Thought reasoning.

Figure: Figure 1: Visualization of the Chain-of-Thought (CoT) process used by our model to solve the SAT formula described in [Theorem 4.5](#S4.Thmtheorem5). The model autonomously performs trial-and-error reasoning, making multiple attempts and backtracking upon encountering conflicts. Here, $T$ represents True and $F$ represents False. Tokens in typewriter font denote the CoT generated by the model.

To investigate the properties of our construction empirically, we design a compiler that converts computational graphs of abstract sequence operations used in our construction into Transformer model weights. We implemented the construction in PyTorch and empirically validated its correctness on random 3-SAT instances. We also investigated its empirical properties such as the number of generated CoT tokens.

Additionally, we perform training experiments to demonstrate that Transformers can effectively learn from deductive reasoning and the backtracking process of the DPLL algorithm encoded as Chain-of-Thought. We show that Transformers equipped with CoT can generalize between 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 unseen number of variables, demonstrating challenges in learning length-generalizable reasoning and opportunities to incorporate compiled reasoning components in Transformer LLMs to improve reasoning capabilities.

Contributions
We prove by theoretical construction that decoder-only Transformers can solve 3-SAT, a fundamental NP-Complete logical reasoning problem, by performing logical deduction and backtracking using 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, although it is much faster on most typical examples.

We design PARAT, a compiler of high-level sequence operations written in Numpy-like syntax into Transformer model weights, to empirically validate and analyze theoretical constructions of Transformer algorithms.

We empirically demonstrate that the compiled SAT-solver model can solve SAT formulas up to 20 propositions and 88 clauses with perfect accuracy. Note that our goal is not to compete with modern state-of-the-art SAT solvers. Rather, we answer a fundamental question about whether LLMs can perform propositional reasoning. Finally, our training experiments suggest that Chain-of-Thought allows Transformer-LLMs to achieve out-of-distribution generalization for the same input lengths.

###### Theorem 1.1 (Informal version of Theorem 4.5 ) .

## 2 Related Work

Theoretical Expressiveness of Transformers and Chain-of-Thought (CoT): Owing to the empirical success of Transformer-based models, many researchers have investigated the capabilities of the Transformer architecture from a theoretical perspective. This line of research focuses on what types of computation can Transformer models simulate by providing theoretical constructions of Transformer models with idealized assumptions.
The seminal work of Liu et al. () showed that Transformers can simulate automata using a single pass over only a logarithmic number of layers w.r.t. the number of states.
Yao et al. () demonstrated that transformers can perform parentheses matching of at most $k$ types of parentheses and $D$ appearance of each ($\operatorname{Dyck}_{k,D}$) with $D+1$ layers.

However, the computation power of one pass of the Transformer model is fundamentally limited (Merrill & Sabharwal ()), and the success of Chain-of-Thought (CoT) reasoning (Wei et al. ()) has sparked more recent research on how CoT can improve upon the expressiveness of Transformer models.
Pérez et al. () proved that Transformers can emulate the execution of single-tape Turing machines if each output vector is appended to the input vector sequence at the next iteration. Giannou et al. () showed that Transformers can recurrently simulate arbitrary programs written in a one-instruction-set language if the output vector at every position of the Transformer is passed as input to the model at the next iteration.
Li et al. () proved that Transformers can simulate arbitrary boolean circuits using CoT by representing the circuit in the positional encoding and is commonly perceived to have shown that Transformers with CoT can “solve all problems”. In particular, transformers can decide all problems in $\operatorname{P/poly}\supseteq\operatorname{P}$ with polynomial steps of CoT.
Merrill & Sabharwal () showed that Transformers with averaging hard attention can decide all regular languages with a linear number of CoT tokens and decide all problems in P with a polynomial number of CoT tokens. Feng et al. () shows that Transformer CoT can perform integer arithmetic, solve linear equations, and perform dynamic programming for the longest increasing subsequence and edit distance problems. These seminal works profoundly advanced our understanding of the capabilities of Transformer models from a theoretical perspective.

How our work differs from the above-mentioned results: Many of the above papers are focused on problems in $\operatorname{P}$ or $\operatorname{P/poly}$, while 3-SAT is an NP-complete problem. It is widely believed that $\operatorname{P}$ is a strict subset of $\operatorname{NP}$, and it is not known whether $\operatorname{NP}$ is a subset of $\operatorname{P/poly}$. In other words, our results are not comparable to these earlier results.

Meanwhile, Pérez et al. (), Li et al. (), and Merrill & Sabharwal () also show 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. By contrast, our theoretical construction demonstrates 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 full input in parallel while any single-tape TM must process each input token sequentially. Furthermore, the CoT produced by our theoretical construction abstractly represents the human reasoning process of trial and error, as demonstrated in [Figure 1](#S1.F1).

Compilation of Transformer Weights. Further, prior work on the theoretical construction of Transformer models rarely provide practical implementations. Notably, Giannou et al. () provide an implementation of their construction and demonstrate its execution on several programs. However, the model is initialized “manually” using prolonged sequences of array assignments, limiting its extensibility to other theoretical frameworks.

More recently, Lindner et al. () released Tracr, which compiles RASP (Weiss et al. ()) programs into decoder-only Transformer models. The “Restricted Access Sequence Processing Language” (RASP, Weiss et al. ()) is a human-readable representation of a subset of operations that Transformers can perform via self-attention and MLP layers. In our preliminary attempt to implement a SAT solver model with Tracr, we identified several implementation inconveniences and limitations of Tracr when scaling to more complex algorithms, which motivated the development of our compiler. In particular: (1) Every “variable” (termed sop in Lindner et al. ()) in Tracr must be either a one-hot categorical encoding or a single numerical value. This constraint makes representing more complex vector structures highly inconvenient. Furthermore, each select operation (i.e., self-attention) accepts only a single sop as the query and key vectors, whereas our theoretical construction often requires incorporating multiple sops as queries and keys. (2) Tracr represents position indices and many other discrete sops with a one-hot encoding, allocating a residual stream dimension for each possible value of the sop. In particular, compiling models with a context length of $n$ requires $O(n)$ additional embedding dimensions for each SOp that represents a position index. (3) 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 MLP layer of $O(n^{3})$ parameters.

## 3 Preliminaries

The Boolean satisfiability problem (SAT) is the problem of determining whether there exists an assignment $A$ of the variables in a Boolean formula $F$ such that $F$ is true under $A$. In this paper we only consider 3-SAT instances in conjunctive normal form (CNF), where groups of at 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. In our implementations we use the well-known DIMACS encoding for CNF formulae whereby each literal is converted to a positive or negative integer corresponding to its index, and clauses are separated by a 0 .

### 3.1 Autoregressive Decoder-Only Transformer Architecture

The Transformer architecture Vaswani et al. () is a 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. It is a relatively complex architecture, and here we only give a precise but quite concise description, and we refer the reader Vaswani et al. () among many others for additional details. Given an input sequence of tokens $\mathbf{s}=(s_{1},s_{2},\dots,s_{n})\in{\mathcal{V}}^{n}$, where ${\mathcal{V}}$ is a vocabulary, a Transformer model $M:{\mathcal{V}}^{*}\rightarrow\Delta({\mathcal{V}})$ maps $\mathbf{s}$ to a distribution ${\bm{p}}_{n+1}\in\Delta({\mathcal{V}})$ by composing a sequence of parameterized intermediate operations. These begin with a token embedding layer, following by $L$ transformer blocks (layers), each block consisting of $H$ attention heads, with embedding dimension $d_{\text{emb}}$, head dimension $d_{h}$, and MLP hidden dimension $d_{\text{mlp}}$. Let us now describe each of these maps in detail.

Token Embedding and Positional Encoding

Each input token $s_{i}$ is converted into a continuous vector representation $\operatorname{Embed}(s_{i})\in{\mathbb{R}}^{d}$ using a fixed embedding map $\operatorname{Embed}(\cdot)$. To incorporate positional information, a positional encoding vector ${\bm{p}}_{i}\in{\mathbb{R}}^{d}$ is added to each token embedding. The initial input to the first Transformer block is

$$ ${\bm{x}}^{(0)}\leftarrow\left(\operatorname{Embed}(s_{1})+{\bm{p}}_{1},\ \operatorname{Embed}(s_{2})+{\bm{p}}_{2},\ \dots,\ \operatorname{Embed}(s_{n})+{\bm{p}}_{n}\right)\in{\mathbb{R}}^{n\times d}.$ $$

##### Transformer Blocks.

For $l=1,\ldots,L$, each block $l$ of the transformer processes an embedded sequence ${\bm{x}}^{(l-1)}\in{\mathbb{R}}^{n\times d}$ to produce another embedded sequence ${\bm{x}}^{(l)}\in{\mathbb{R}}^{n\times d}$. Each block consists of a multi-head self-attention (MHA) mechanism and a position-wise feed-forward network (MLP). We have a set of parameter tensors that includes MLP parameters ${\bm{W}}_{1}^{(l)}\in{\mathbb{R}}^{d_{\text{emb}}\times d_{\text{mlp}}^{*}}$, ${\bm{b}}_{1}^{(l)}\in{\mathbb{R}}^{d_{\text{mlp}}^{*}}$, ${\bm{W}}_{2}^{(l)}\in{\mathbb{R}}^{d_{\text{mlp}}\times d}$, and ${\bm{b}}_{2}^{(l)}\in{\mathbb{R}}^{d}$, self-attention parameters ${\bm{W}}_{Q}^{(l,h)},\ {\bm{W}}_{K}^{(l,h)},\ {\bm{W}}_{V}^{(l,h)}\in{\mathbb{R}}^{d\times d_{h}}$ for every $h=1,\ldots,H$, and multi-head projection matrix ${\bm{W}}_{O}^{(l)}\in{\mathbb{R}}^{(Hd_{h})\times d_{\text{emb}}}$. We will collectively refer to all such parameters at layer $l$ as $\Gamma^{(l)}$, whereas the self-attention parameters for attention head $h$ at layer $l$ will be referred to as $\Gamma^{(l,h)}$. We can now process the embedded sequence ${\bm{x}}^{(l-1)}$ to obtain ${\bm{x}}^{(l)}$ in two stages:

$$ $\displaystyle{\bm{h}}^{(l)}\leftarrow{\bm{x}}^{(l-1)}+\operatorname{MHA}\left({\bm{x}}^{(l-1)};\Gamma^{(l)}\right),\qquad\text{ and }\qquad{\bm{x}}^{(l)}\leftarrow{\bm{h}}^{(l)}+\operatorname{MLP}\left({\bm{h}}^{(l)};\Gamma^{(l)}\right),$ $$

where

$$ $\displaystyle\operatorname{MHA}\left({\bm{x}};\Gamma^{(l)}\right)$ $\displaystyle:=\operatorname{Concat}\left(\operatorname{Attention}({\bm{x}};\Gamma^{(l,1)}),\ldots,\operatorname{Attention}({\bm{x}};\Gamma^{(l,H)})\right){\bm{W}}_{O}^{(l)}$ $\displaystyle\operatorname{Attention}({\bm{x}};\Gamma^{(l,h)})$ $\displaystyle:=\operatorname{softmax}\left(d_{h}^{-1/2}{\bm{x}}{\bm{W}}_{Q}^{(l,h)}({\bm{W}}_{K}^{(l,h)}{\bm{x}})^{\top}+{\bm{M}}\right){\bm{x}}{\bm{W}}_{V}^{(l,h)}$ $\displaystyle\operatorname{MLP}\left({\bm{h}};\Gamma^{(l)}\right)$ $\displaystyle:=\sigma\left({\bm{h}}{\bm{W}}_{1}^{(l)}+{\bm{b}}_{1}^{(l)}\right){\bm{W}}_{2}^{(l)}+{\bm{b}}_{2}^{(l)}.$ $$

The $n\times n$ matrix ${\bm{M}}$ is used as a “mask” to ensure self-attention is only backward looking, so we set ${\bm{M}}[i,j]=\infty$ for $i\geq j$ and ${\bm{M}}[i,j]=0$ otherwise. Finally, we use the $\operatorname{ReGLU}(\cdot):{\mathbb{R}}^{2d_{\text{mlp}}}\rightarrow{\mathbb{R}}^{d_{\text{mlp}}}$ activation function $\sigma(\cdot)$ at each position. Tiven input ${\bm{u}}\in{\mathbb{R}}^{n\times 2d_{\text{mlp}}}$, for each position $i$ we split ${\bm{u}}_{i}$ into two halves ${\bm{u}}_{i,1},\ {\bm{u}}_{i,2}\in{\mathbb{R}}^{d}$ and, using $\otimes$ denotes element-wise multiplication, we define

$$ $\sigma_{\text{ReGLU}}\left({\bm{u}}_{i}\right)={\bm{u}}_{i,1}\otimes\operatorname{ReLU}\left({\bm{u}}_{i,2}\right).$ (1) $$

Figure: Algorithm 1 Greedy Decoding

Output Layer

After the final Transformer block, the output representations are projected onto the vocabulary space, and the output vector at the final position is converted to a probability distribution over the vocabulary via the softmax function:

$$ ${\bm{o}}={\bm{x}}^{(L)}{\bm{W}}_{\text{out}}+{\bm{b}}_{\text{out}}\in{\mathbb{R}}^{n\times V},{\bm{p}}_{n+1}=\operatorname{softmax}(\lambda{\bm{o}}_{n})\in\Delta({\mathcal{V}})$ (2) $$

where ${\bm{W}}_{\text{out}}\in{\mathbb{R}}^{d\times V}$, ${\bm{b}}_{\text{out}}\in{\mathbb{R}}^{V}$, $V$ is the size of the vocabulary, ${\bm{o}}_{n}\in{\mathbb{R}}^{V}$ is the output vector at the last position, and $\lambda\in{\mathbb{R}}$ is the temperature.

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. When using the greedy seconding strategy, the highest probability token is always selected and the generation process is described in [Algorithm 1](#alg1).

In probabilistic decoding, the next token is instead selected based on the probability distribution $s_{t+1}\sim{\bm{p}}_{t+1}(v)$ using temperature $\lambda$ in [Equation 2](#S3.E2). In this paper, we refer to the full generated sequence of tokens as the Chain-of-Thought, and the number of chain-of-thought tokens in [Algorithm 1](#alg1) is $t-n$.

## 4 Transformers and SAT: logical deduction and backtracking

This section presents and explains our main results on Transformers’ capability in deductive reasoning and backtracking with CoT. To rigorously state our results, we first formally define decision problems, decision procedures, and what it means for a model to “solve” a decision problem using CoT:

###### Definition 4.1 (Decision Problem) .

Let ${\mathcal{V}}$ be a vocabulary, $\Sigma\subseteq{\mathcal{V}}$ be an alphabet, $L\subseteq\Sigma^{*}$ be a set of valid input strings. We say that a mapping $f:L\rightarrow\{0,1\}$ is a decision problem defined on $L$.

###### Definition 4.2 (Decision Procedure) .

We say that an algorithm $\mathcal{A}$ is a decision procedure for the decision problem $f$, if given any input string $x$ from $L$, $\mathcal{A}$ outputs $1$ if $f(x)=1$, and 0 0 otherwise.

###### Definition 4.3 (Autoregressive Decision Procedure) .

For any map $M:{\mathcal{V}}^{*}\rightarrow\Delta({\mathcal{V}})$, which we refer to as an auto-regressive next-token prediction model, and $\mathcal{E}=\{\mathcal{E}_{0},\mathcal{E}_{1}\}\subset{\mathcal{V}}$, define decision procedure $\mathcal{A}_{M,\mathcal{E}}$ as follows: For any input $s_{1:n}$, run Algorithm [1](#alg1) with stop tokens $\mathcal{E}$. $\mathcal{A}_{M,\mathcal{E}}$ outputs 0 if $s_{1:t}$ ends with $\mathcal{E}_{0}$ and $\mathcal{A}_{M,\mathcal{E}}$ output 1 otherwise. We say $M$ autoregressively decides decision problem $f$ if there is some ${\mathcal{E}}\subset{\mathcal{V}}$ for which $\mathcal{A}_{M,{\mathcal{E}}}$ decides $f$.

###### Definition 4.4 ( $\operatorname{3-SAT}_{p,c}$ ) .

Let $\operatorname{DIMACS}(p,c)$ denote the set of valid DIMACS encodings of 3-SAT instances with at most $p$ variables and $c$ clauses with a prepended [BOS] token and an appended [SEP] token. Define $\operatorname{3-SAT}_{p,c}:\operatorname{DIMACS}(p,c)\rightarrow\{0,1\}$ as the problem of deciding whether the 3-SAT formula encoded in the input in $\operatorname{DIMACS}(p,c)$ encoding is satisfiable.

With the above definition, we’re ready to present a formal statement of our theoretical construction of a Transformer model that performs SAT Solving:

###### Theorem 4.5 (Decoder-only Transformers can solve SAT) .

For any $p,c\in{\mathbb{N}}^{+}$,
there exists a Transformer model $M:{\mathcal{V}}^{*}\rightarrow\Delta({\mathcal{V}})$ that autoregressively decides $\operatorname{3-SAT}_{p,c}$ in no more than $p\cdot 2^{p+1}$ CoT iterations. $M$ requires $L=7$ layers, $H=5$ heads, $d_{\text{emb}}=O(p)$, and $O(p^{2})$ parameters.

Remarks on [Theorem 4.5](#S4.Thmtheorem5)

- •
The upper bound on the CoT length $p\cdot 2^{p+1}$ is a worst-case upper bound which assumes that the model is unable to make any logical deductions have to try all $2^{p}$ assignments. However, this upper bound is never reached in practice, and in [Figure 3](#A2.F3) we show that the number of CoT tokens is no greater than $8p\cdot 2^{0.08p}$ for most formulas. If the number of backtracking steps is bounded by $T$ then the CoT is no longer than $(2p+1)(T+1)$
- •
The worst-case CoT length is independent of the number of clauses $c$, which is due to the parallel deduction over all clauses within the Transformer construction. Otherwise, sequentially processing each clause would take at least $c\cdot 2^{O(p)}$ number of steps.
- •
Positional encodings are not included in the number of parameters. The positional encoding at position $i$ is the numerical value $i$ at a particular dimension.
- •
Each parameter can be represented with $O(p+\log c)$ bits

We show our full proof via trace equivalence with DPLL in [Appendix C](#A3). The construction uses adapted versions of lemmas from Feng et al. () as basic building blocks.

Here we describe our design of the algorithm and CoT process for SAT-Solving and a high-level description on the internal mechanisms of the Transformer model.

Logical Deduction and Backtracking in CoT.
In [Figure 1](#S1.F1), we illustrate the Chain-of-Thought of our model when solving SAT instances. The model performs SAT-solving through trial-and-error reasoning by iteratively exploring different solution paths while “learning” lessons from failed attempts, inspired by the “abstract DPLL” algorithm (Nieuwenhuis et al. ()). Specifically, at each step, the model: (1) attempts a solving direction by assigning a truth value to a variable; (2) deduces new variable assignments based on the clauses and current assignments; and (3) backtracks and negates the last assumed assignment if a conflict arises. The chain of thought keeps track of the current “assignment trace”, which includes the order of current assignments and whether each assignment is an assumption or a deduction. This iterative process continues until a satisfying assignment is found, which mirrors the human problem-solving process of trying different possible solutions before reaching an answer.

###### Definition 4.1 (Decision Problem) .

###### Definition 4.2 (Decision Procedure) .

###### Definition 4.3 (Autoregressive Decision Procedure) .

###### Definition 4.4 ( 3 − SAT p , c subscript 3 SAT 𝑝 𝑐 \operatorname{3-SAT}_{p,c} ) .

###### Theorem 4.5 (Decoder-only Transformers can solve SAT) .

##### Parallel Processing of Constraints.

In our construction, we demonstrate that Transformers can process all clauses in parallel when checking for satisfaction, conflicts, and finding possible deductions.

Essentially, each clause in the input formula as well as the current state can be “summarized” as a single binary vector, and the query and key transformations ensure that the dot product between the current state (assignment) and each clause provides information on whether deduction is possible between them. The attention operation averages over clauses where deductions are possible and the following MLP layer filters out the result of deductions.

## 5 Compiler for Complex Transformer Algorithms

In the previous section, we presented a theoretical construction of a Transformer capable of solving SAT instances through backtracking and parallel deduction. However, relying solely on theorems and proofs can make it challenging to gain practical insights and verify correctness. To address this, we introduce ParametricTransformer (PARAT), which provides a framework for converting theoretical constructions of Transformers into practical models to facilitate empirical analysis and validation.

### 5.1 Supported Features and Operations

Our compiler 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” is an instance of the SOp base class (name adapted from Lindner et al. ()), and each instance sop of SOp is assigned a dimension $d_{\texttt{sop}}\in{\mathbb{N}}^{+}$ and can be viewed as an abstract representation of an $\mathbf{{\mathbb{R}}}^{n\times d_{\texttt{sop}}}$ array where $n$ is the number of tokens in the input to the Transformer model. A PARAT “program” is basically a sequence of array operations over SOps.

Throughout this section, we refer to the indices along the first dimension of an SOp as “position” and refer to indices along the second dimension as “dimension”.

The “inputs” to a program are arbitrary positional encoding and token embedding SOps, represented by the base class names PosEncSOp and TokEmbSOp respectively. For example, the OneHotTokEmb class represents the one-hot embedding of tokens and Indices represents the numerical value of the index of each position.

The rest of the program performs various operations that compute new SOps based on existing ones. We provide implementations of basic building block operations including (but not limited to) the following:

- •
Mean(q, k, v) Represents the “Averaging Hard Attention” operation. At each position $i$, this operation identifies all target positions $j$ with the maximal value of $q_{i}^{\top}k_{j}$ for $j\leq i$ and computes the average of the corresponding $v_{j}$ values.
- •
sop[idx, :] Performs indexing using a one-dimensional index array idx, producing an SOp out such that $\texttt{out}[i,j]=\texttt{sop}[\texttt{idx}[i],j]$ for $i\in[n]$ and $j\in[d_{\texttt{sop}}]$. This mirrors NumPy’s array indexing semantics.
- •
sop[:, start:end] Extracts a slice of dimensions from sop, where start, end $\in[d_{\texttt{sop}}]$, resulting in a new SOp of dimension $\texttt{end}-\texttt{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 ($\geq$, $\leq$, $>$, $<$), following standard broadcasting rules.

As an illustrative example, the following function returns a one-dimensional SOp representing the position index of the closest token within a set of target tokens:

We present our full code implementing our construction for [Theorem 4.5](#S4.Thmtheorem5) using PARAT in [Appendix D](#A4).

### 5.2 The Compilation Process

PARAT takes in a SOp that contains the computational graph of the algorithm and outputs a PyTorch (Paszke et al. ()) 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 a 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 are reduced to a single operation through matrix multiplication and dependency merging.
- 3.
Allocation of Layers and Residual Stream: The computational graph is topologically sorted such that each sop appears later than its dependencies. This sorting is then used to assign SelfAttention 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 to their $d_{\texttt{sop}}$ size.
- 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 SelfAttention sop corresponds to an attention head, and each GLUMLP sops corresponds to part of a MLP layer with ReGLU activation.

Soft vs Hard Attention The reduction of Mean to SelfAttention induces inevitable numerical errors due to Mean representing averaging a strict subset of previous positions while SelfAttention computes a weighted average over all previous positions via $\operatorname{softmax}$. This error also affects other operations based on Mean such as position indexing. We control this error via an “exactness” parameter $\beta$ that scales the attention logits, and [Lemma C.6](#A3.Thmtheorem6) shows that the error decreases exponentially w.r.t. $\beta$.

Multi-Stage Evaluation To facilitate debugging, PARAT allows 3 types of evaluations for every sop at different stages of compilation.

- •
sop.abstract_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.concrete_eval(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 to evaluating the Pytorch model after the full compilation process.

### 5.3 Analysis of the Compiled SAT-Solving Model

With PARAT, we successfully compiled our theoretical construction in [Theorem 4.5](#S4.Thmtheorem5) using the code in [Appendix D](#A4). For $p=20$ number of variables, the resulting Transformer has 7 layers, 5 attention heads, 502 embedding dimensions, and 5011862 parameters. With a concrete implementation of our theoretical construction in PyTorch, we 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? These questions reveal further insights that are not available by observing the theoretical constructions alone and demonstrate the additional values provided by PARAT.

Evaluation Datasets We evaluate our models on randomly sampled DIMACS encoding of 3-SAT formulas. We focus on SAT formulas with exactly 3 literals in each clause, with the number of clauses $c$ between $4.1p$ and $4.4p$, where $p$ is the number of variables.

It is well-known that the satisfiability of such random 3-SAT formulas highly depends on the clause/variable ratio, where a formula is very likely satisfiable if $c/p\ll 4.26$ and unsatisfiable if $c/p\gg 4.26$ (Crawford & Auton ()). 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 a 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 distribution, 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:

- •
Marginal: Composed of pairs of formulas that differ by only one token.
- •
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\leq p\leq 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](#A4) using PARAT with max number of variables $p=20$, max number of clauses $c=88$, and exactness parameter $\beta=20$. The model uses greedy decoding during generation.

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](#S4.Thmtheorem5) as well as PARAT. This result is included in [Figure 2](#S6.F2) to compare with trained models.

How many steps? We perform experiments to measure the empirical Chain-of-Thought length required for solving SAT formulas of different sizes. For all formulas we evaluated, the maximum CoT length is bounded by $8p\cdot 2^{0.08p}$, which is significantly less than the theoretical bound of $p\cdot 2^{(p+1)}$. This indicates that the model can use deduction to reduce the search space significantly. The figure illustrating the results is in Appendix [Figure 3](#A2.F3).

Effect of Soft Attention In our previous evaluations, we used a sufficiently large ”exactness” value $\beta$ to ensure that the error from MEAN based operations does not affect the final output of greedy sampling. The use of ”Averaging Hard Attention” is prevalent in previous works on theoretical construction. However, how exactly does soft-attention affect the final reasoning output?

In [Figure 4](#A2.F4) we present the SAT/UNSAT prediction accuracy for models under 8 different “mean exactness” $\beta$ values on our “marginal” datasets ranging from $2.5$ to $20$. Recall that $\beta$ controls how the well soft attention approximates ”hard” attention in each self-attention layer. Our results demonstrate that longer inputs generally require larger $\beta$ values to achieve high accuracy. This may explain why Transformers fail to learn generalizable algorithmic procedures, as the attention learned on smaller formulas may be too ”soft” to generalize to larger inputs.

## 6 Can Transformer Learn SAT Solving from Data?

Our previous sections showed that Transformer and weights exist for solving SAT instances using CoT with backtracking 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. () 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 training on the Chain-of-Thought procedure with deduction and backtracking described in [Figure 1](#S1.F1) can facilitate Out-of-Distribution generalization within the same number of variables.

Datasets In [Section 5.3](#S5.SS3) we introduced 3 different distributions over random 3-SAT formulas of varying difficulties. For training data, we use the same sampling methods, but instead of having a separate dataset for each variable number $p$, we pick 2 ranges $p\in[6,10]$ and $p\in[11,15]$, where for each sample a 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\times 3$ training datasets, each containing $5\times 10^{5}$ training samples(^1^11The number of training samples is negligible compared to the total number of possible formulas. Note that the number of clauses is at least $4p$, each clause contains 3 literals and each literal has at least $p$ choices. This results in $p^{12p}$ possibilities, which is $>10^{56}$ for $p=6$), with balanced SAT vs UNSAT samples. For each formula, we generate the corresponding chain of thought in the same format as [Figure 1](#S1.F1) using a custom SAT Solver.
The evaluation data is exactly the same as [Section 5.3](#S5.SS3).

Model and Training We use the LLaMa (Touvron et al. ()) architecture with 70M and 160M parameters for the training experiments, which uses Rotary Positional Encodings (RoPE) and SwiGLU as the activation function for MLP layers. Following prior works (Feng et al. ()), 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](#A1). We also permute the variable IDs for training samples to ensure that the model sees all possible input tokens for up to 20 variables.

### 6.1 Intra-length OOD Generalization

**Table 1: Average accuracies (%) of SAT/UNSAT prediction for models trained and tested on different datasets in the training regime for number of variables $p\in[6,10]$ and $p\in[11,15]$. Columns denote train datasets, and rows denote test datasets. Each accuracy is computed over $10000$ total samples.**
|  | $p\in[6,10]$ | $p\in[11,15]$ |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- |
|  | Marginal | Random | Skewed | Marginal | Random | Skewed |
| Marginal | 99.88% | 99.99% | 99.99% | 98.66% | 99.70% | 99.57% |
| Random | 99.96% | 100.00% | 100.00% | 99.11% | 99.75% | 99.55% |
| Skewed | 99.96% | 100.00% | 99.99% | 99.41% | 99.74% | 99.48% |

Our first set of experiments evaluates the model’s performance on SAT formulas sampled from different distributions from training, but the number of variables in formulas remains the same ($p\in[6,10]$ and $p\in[11,15]$ for both train and test datasets).

As shown in [Table 1](#S6.T1), our trained models achieve near-perfect SAT vs UNSAT prediction accuracy when tested on the same number of variables as the training data, even when on formulas sampled from different distributions. Recall that the “marginal” dataset has SAT vs UNSAT samples differing by a 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 experiments suggest that the LLM have very likely learned general reasoning procedures using CoT that can be applied to all formulas with the same number of variables as the data they are trained on.

### 6.2 Limitations in Length Generalization

Figure: Figure 2: Result of the Length generalization experiments, showing SAT/UNSAT prediction accuracy of Transformer-LLM trained on the marginal, random, and skewed dataset on the marginal dataset over 4-20 variables. Left: model trained on 6-10 variables. Right: model trained on 11-15 variables.
Refer to caption: /html/2410.07432/assets/imgs/trained_6_10_marginal.png

The second experiment evaluates the model’s ability to generalize to formulas with a different number of variables than seen during training. We use the model trained on the Marginal dataset from section [1](#S6.T1) and evaluate datasets with 4-20 variables, generated using the three methods described, with 2,000 samples each. For this experiment, we evaluate the binary SAT vs UNSAT prediction accuracy.

Results
In Figure [2](#S6.F2), our results indicate that performance degrades drastically beyond the training regime when the number of variables increases. This shows that the model is unable to learn a 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. This further demonstrates the value of having a compiled Transformer that provably works well on all inputs up to $p$ variables for any given $p$.

## 7 Acknowledgements

This work is supported by NSF awards IIS-2229876 and CCF-2403391. The authors thank Hassan Naveed for his exploratory work on using RASP for SAT-solver implementation, William Armstrong for suggesting the abstract DPLL paper and contributing code, and Jintong Jiang for providing suggestions on the paper’s presentation and writing.

## Appendix A Training Details

We use Llama Touvron et al. () models in the HuggingFace library. For the 70M model, we use models with 6 layers, 512 embedding dimensions, 8 heads, 512 attention hidden dimensions, and 2048 MLP hidden dimensions. For the 140M model, we 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 a scheduled cosine learning rate decaying from $6\times 10^{-4}$ to $6\times 10^{-5}$ with $\beta_{1}=0.9$ and $\beta_{2}=0.95$.

## Appendix B Additional Experiment Results

In [Figure 3](#A2.F3) we provide results on the number of Chain-of-Thought tokens required to solve randomly generated SAT instances. In [Figure 4](#A2.F4) we provide results on how the SAT/UNSAT prediction accuracy is affected by numerical errors introduced by softmax.

Figure: Figure 3: Chain-of-Thought Lengths generated by the compiled SAT-Solver Model vs 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 in our datasets is bounded by $8p\cdot 2^{0.08p}$
Refer to caption: /html/2410.07432/assets/imgs/CoTlen.png

Figure: Figure 4: The impact of soft attention in Transformer layers on the SAT/UNSAT prediction accuracy. $\beta$ is a scaling factor that allows the soft attention operation to better simulate hard attention at the cost of larger model parameter values in attention layers. The model achieves perfect accuracy on all “marginal” datasets starting at $\beta=17.5$, and for lower $\beta$ values, accuracy is negatively correlated with the number of variables in the datasets.
Refer to caption: /html/2410.07432/assets/imgs/soft_attn.png

## Appendix C Proofs

### C.1 Notation Details

##### 3-SAT

SAT problems where the Boolean formula is expressed in conjunctive normal form (CNF) with three literals per clause will be referred to as 3-SAT. A formula in CNF is a conjunction (i.e. “AND”) of clauses, a clause is a disjunction (i.e. “OR”) of several literals, and each literal is either a variable or 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:

$$ $\displaystyle(x_{1}\lor\neg x_{2})\land(\neg x_{1}\lor x_{2}\lor\neg x_{3})\land(x_{2}\lor x_{4}\lor\neg x_{1})\land$ $\displaystyle(x_{1}\lor\neg x_{3}\lor x_{4})\land(\neg x_{2}\lor\neg x_{3}\lor\neg x_{4})\land(\neg x_{4}\lor\neg x_{1})$ $$

The 3-SAT problem refers to determining if any assignment of truth values to the variables allows the formula $\phi$ to evaluate as true. It is well-known that 3-SAT is NP-hard and is widely believed to be unsolvable in polynomial time.

##### DIMACS Encoding

The DIMACS format is a 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 a terminating “0” (i.e. “0” represents $\land$ symbols and parentheses). Positive integers correspond to variables, while negative integers represent the negations of variables. For instance, if a clause includes the literals $x_{1}$, $\neg x_{2}$, and $x_{3}$, it would be represented as ”1 -2 3 0” in the DIMACS format.

For the 3-SAT example in the previous paragraph, the corresponding DIMACS representation would be:

1 -2 0 -1 2 -3 0 2 4 -1 0 1 -3 4 0 -2 -3 -4 0 -4 -1 0

### C.2 Useful Lemmas for Transformers

In this section, we present adapted versions of several lemmas from Feng et al. (). Specifically, an MLP with ReGLU can exactly simulate ReLU, linear operations, and multiplication without error. For Self-attention lemmas, we directly adapt from Feng et al. ().

#### C.2.1 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 $f({\bm{x}})={\bm{W}}_{2}[({\bm{W}}_{1}{\bm{x}}+{\bm{b}})\otimes\operatorname{relu}({\bm{V}}{\bm{x}}+{\bm{c}})]$ can approximate the following vector operations for arbitrary input ${\bm{x}}$:

- •
Simulate a 2-layer MLP with ReLU activation: ${\bm{W}}_{2}\operatorname{ReLU}({\bm{W}}^{\prime}_{1}{\bm{x}}+{\bm{b}}^{\prime}_{1})+{\bm{b}}^{\prime}_{2}$
- •
Simulate any linear operation ${\bm{W}}{\bm{x}}$
- •
Simulate element-wise multiplication: ${\bm{x}}_{1}\otimes{\bm{x}}_{2}$

###### Lemma C.1 (Simulating a 2-Layer ReLU MLP with ReGLU Activation) .

A 2-layer MLP with ReGLU activation function can simulate any 2-layer MLP with ReLU activation function.

###### Proof.

Let the ReLU MLP be defined as:

$$ $g({\bm{x}})={\bm{W}}^{\prime}_{2}\,\operatorname{ReLU}({\bm{W}}^{\prime}_{1}{\bm{x}}+{\bm{b}}^{\prime}_{1})+{\bm{b}}^{\prime}_{2}.$ $$

Set the weights and biases of the ReGLU MLP as follows:

$$ $\displaystyle{\bm{W}}_{1}$ $\displaystyle=\mathbf{0},\quad{\bm{b}}_{1}=\mathbf{1},$ $\displaystyle{\bm{V}}$ $\displaystyle={\bm{W}}^{\prime}_{1},\quad{\bm{b}}_{2}={\bm{b}}^{\prime}_{1},$ $\displaystyle{\bm{W}}_{2}$ $\displaystyle={\bm{W}}^{\prime}_{2},\quad{\bm{b}}={\bm{b}}^{\prime}_{2}.$ $$

Then, the ReGLU MLP computes:

$$ $f({\bm{x}})={\bm{W}}^{\prime}_{2}\left[(\mathbf{0}\cdot{\bm{x}}+\mathbf{1})\otimes\operatorname{ReLU}({\bm{W}}^{\prime}_{1}{\bm{x}}+{\bm{b}}^{\prime}_{1})\right]+{\bm{b}}^{\prime}_{2}.$ $$

Simplifying:

$$ $f({\bm{x}})={\bm{W}}^{\prime}_{2}\left[\mathbf{1}\otimes\operatorname{ReLU}({\bm{W}}^{\prime}_{1}{\bm{x}}+{\bm{b}}^{\prime}_{1})\right]+{\bm{b}}^{\prime}_{2}={\bm{W}}^{\prime}_{2}\,\operatorname{ReLU}({\bm{W}}^{\prime}_{1}{\bm{x}}+{\bm{b}}^{\prime}_{1})+{\bm{b}}^{\prime}_{2}=g({\bm{x}}).$ $$

Thus, the ReGLU MLP 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 compute any linear operation $f({\bm{x}})={\bm{W}}{\bm{x}}+{\bm{b}}$.

###### Proof.

To compute a linear function using the ReGLU MLP, we can set the activation to act as a scalar multiplier of one. Set the weights and biases as:

$$ $\displaystyle{\bm{W}}_{1}$ $\displaystyle={\bm{W}},\quad{\bm{b}}_{1}={\bm{b}},$ $\displaystyle{\bm{V}}$ $\displaystyle=\mathbf{0},\quad{\bm{b}}_{2}=\mathbf{1},$ $\displaystyle{\bm{W}}_{2}$ $\displaystyle={\bm{I}},\quad{\bm{b}}=\mathbf{0}.$ $$

Here, ${\bm{I}}$ is the identity matrix.

Since ${\bm{V}}{\bm{x}}+{\bm{b}}_{2}={\bm{b}}_{2}=\mathbf{1}$, we have:

$$ $\operatorname{ReLU}({\bm{V}}{\bm{x}}+{\bm{b}}_{2})=\operatorname{ReLU}(\mathbf{1})=\mathbf{1}.$ $$

Then, the ReGLU MLP computes:

$$ $f({\bm{x}})={\bm{I}}\left[({\bm{W}}{\bm{x}}+{\bm{b}})\otimes\mathbf{1}\right]={\bm{W}}{\bm{x}}+{\bm{b}}.$ $$

Thus, any linear operation can be represented by appropriately setting ${\bm{W}}_{1}$, ${\bm{b}}_{1}$, and ${\bm{W}}_{2}$.
∎

###### 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 ${\bm{x}}_{1}$ and ${\bm{x}}_{2}$, that is,

$$ $f({\bm{x}})={\bm{x}}_{1}\otimes{\bm{x}}_{2},$ $$

where ${\bm{x}}=[{\bm{x}}_{1};{\bm{x}}_{2}]$ denotes the concatenation of ${\bm{x}}_{1}$ and ${\bm{x}}_{2}$.

###### Proof.

Let ${\bm{x}}=[{\bm{x}}_{1};{\bm{x}}_{2}]\in\mathbb{R}^{2n}$, where ${\bm{x}}_{1},{\bm{x}}_{2}\in\mathbb{R}^{n}$.

Set the weights and biases:

$$ $\displaystyle{\bm{W}}_{1}$ $\displaystyle=\begin{bmatrix}{\bm{I}}_{n}\\ {\bm{I}}_{n}\end{bmatrix},$ $\displaystyle{\bm{b}}_{1}$ $\displaystyle=\mathbf{0}_{2n},$ $\displaystyle{\bm{V}}$ $\displaystyle=\begin{bmatrix}{\bm{I}}_{n}\\ -{\bm{I}}_{n}\end{bmatrix},$ $\displaystyle{\bm{b}}_{2}$ $\displaystyle=\mathbf{0}_{2n},$ $\displaystyle{\bm{W}}_{2}$ $\displaystyle=\begin{bmatrix}{\bm{I}}_{n}&-{\bm{I}}_{n}\end{bmatrix},$ $\displaystyle{\bm{b}}$ $\displaystyle=\mathbf{0}_{n}.$ $$

Compute:

$$ $\displaystyle{\bm{W}}_{1}{\bm{x}}+{\bm{b}}_{1}$ $\displaystyle=\begin{bmatrix}{\bm{x}}_{1}\\ {\bm{x}}_{1}\end{bmatrix},$ $\displaystyle{\bm{V}}{\bm{x}}+{\bm{b}}_{2}$ $\displaystyle=\begin{bmatrix}{\bm{x}}_{2}\\ -{\bm{x}}_{2}\end{bmatrix},$ $\displaystyle\operatorname{ReLU}({\bm{V}}{\bm{x}}+{\bm{b}}_{2})$ $\displaystyle=\begin{bmatrix}\operatorname{ReLU}({\bm{x}}_{2})\\ \operatorname{ReLU}(-{\bm{x}}_{2})\end{bmatrix}.$ $$

The element-wise product:

$$ $({\bm{W}}_{1}{\bm{x}}+{\bm{b}}_{1})\otimes\operatorname{ReLU}({\bm{V}}{\bm{x}}+{\bm{b}}_{2})=\begin{bmatrix}{\bm{x}}_{1}\otimes\operatorname{ReLU}({\bm{x}}_{2})\\ {\bm{x}}_{1}\otimes\operatorname{ReLU}(-{\bm{x}}_{2})\end{bmatrix}.$ $$

Compute the output:

$$ $\displaystyle f({\bm{x}})$ $\displaystyle={\bm{W}}_{2}\left[({\bm{W}}_{1}{\bm{x}}+{\bm{b}}_{1})\otimes\operatorname{ReLU}({\bm{V}}{\bm{x}}+{\bm{b}}_{2})\right]+{\bm{b}}$ $\displaystyle={\bm{x}}_{1}\otimes\operatorname{ReLU}({\bm{x}}_{2})-{\bm{x}}_{1}\otimes\operatorname{ReLU}(-{\bm{x}}_{2})$ $\displaystyle={\bm{x}}_{1}\otimes\left(\operatorname{ReLU}({\bm{x}}_{2})-\operatorname{ReLU}(-{\bm{x}}_{2})\right)$ $\displaystyle={\bm{x}}_{1}\otimes{\bm{x}}_{2}.$ $$

Thus, the ReGLU MLP computes $f({\bm{x}})={\bm{x}}_{1}\otimes{\bm{x}}_{2}$ without restrictions on ${\bm{x}}_{2}$.
∎

###### Lemma C.1 (Simulating a 2-Layer ReLU MLP with ReGLU Activation) .

###### Proof.

###### Lemma C.2 (Simulating Linear Operations with ReGLU MLP) .

###### Proof.

###### Lemma C.3 (Element-wise Multiplication via ReGLU MLP) .

###### Proof.

#### C.2.2 Capabilities of the Self-Attention Layer

In this subsection, we provide 2 core lemmas on the capabilities of the self-attention layer from Feng et al. ().

Let $n\in\mathbb{N}$ be an integer and let ${\bm{x}}_{1},{\bm{x}}_{2},\cdots,{\bm{x}}_{n}$ be a sequence of vectors where ${\bm{x}}_{i}=(\tilde{\bm{x}}_{i},r_{i},1)\in[-M,M]^{d+2}$, $\tilde{\bm{x}}_{i}\in\mathbb{R}^{d}$, $r_{i}\in\mathbb{R}$, and $M$ is a large constant. Let ${\bm{K}},{\bm{Q}},{\bm{V}}\in\mathbb{R}^{d^{\prime}\times(d+2)}$ be any matrices with $\|{\bm{V}}\|_{\infty}\leq 1$, and let $0<\rho,\delta<M$ be any real numbers. Denote ${\bm{q}}_{i}={\bm{Q}}{\bm{x}}_{i}$, ${\bm{k}}_{j}={\bm{K}}{\bm{x}}_{j}$, ${\bm{v}}_{j}={\bm{V}}{\bm{x}}_{j}$, and define the *matching set* ${\mathcal{S}}_{i}=\{j\leq i:|{\bm{q}}_{i}\cdot{\bm{k}}_{j}|\leq\rho\}$. Equipped with these notations, we define two basic operations as follows:

- •
COPY: The output is a sequence of vectors ${\bm{u}}_{1},\cdots,{\bm{u}}_{n}$ with ${\bm{u}}_{i}={\bm{v}}_{\mathrm{pos}(i)}$, where $\mathrm{pos}(i)=\operatorname{argmax}_{j\in{\mathcal{S}}_{i}}{r_{j}}$.
- •
MEAN: The output is a sequence of vectors ${\bm{u}}_{1},\cdots,{\bm{u}}_{n}$ with ${\bm{u}}_{i}=\operatorname{mean}_{j\in{\mathcal{S}}_{i}}{{\bm{v}}_{j}}$.

###### Assumption C.4 .

[Assumption C.6 from Feng et al. ()]
The matrices ${\bm{Q}},{\bm{K}},{\bm{V}}$ and scalars $\rho,\delta$ satisfy that for all considered sequences ${\bm{x}}_{1},{\bm{x}}_{2},\cdots,{\bm{x}}_{n}$, the following hold:

- •
For any $i,j\in[n]$, either $|{\bm{q}}_{i}\cdot{\bm{k}}_{j}|\leq\rho$ or ${\bm{q}}_{i}\cdot{\bm{k}}_{j}\leq-\delta$.
- •
For any $i,j\in[n]$, either $i=j$ or $|r_{i}-r_{j}|\geq\delta$.

[Assumption C.4](#A3.Thmtheorem4) says that there are sufficient gaps between the attended position (e.g., $\mathrm{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.

###### Lemma C.5 (Lemma C.7 from Feng et al. ( 2023 ) ) .

Assume [Assumption C.4](#A3.Thmtheorem4) holds with $\rho\leq\frac{\delta^{2}}{8M}$. For any $\epsilon>0$, there exists an attention layer with embedding size $O(d)$ and one causal attention head that can approximate the COPY operation defined above. Formally, for any considered sequence of vectors ${\bm{x}}_{1},{\bm{x}}_{2},\dots,{\bm{x}}_{n}$, denote the corresponding attention output as ${\bm{o}}_{1},{\bm{o}}_{2},\dots,{\bm{o}}_{n}$. Then, we have $\|{\bm{o}}_{i}-{\bm{u}}_{i}\|_{\infty}\leq\epsilon$ for all $i\in[n]$ with ${\mathcal{S}}_{i}\neq\emptyset$. Moreover, the $\ell_{\infty}$ norm of attention parameters is bounded by $O(\mathrm{poly}(M,1/\delta,\log(n),\log(1/\epsilon)))$.

###### Lemma C.6 (Lemma C.8 from Feng et al. ( 2023 ) ) .

Assume [Assumption C.4](#A3.Thmtheorem4) holds with
$\rho\leq\frac{\delta\epsilon}{16M\ln(\frac{4Mn}{\epsilon})}$.
For any $0<\epsilon\leq M$, there exists an attention layer with embedding size $O(d)$ and one causal attention head that can approximate the MEAN operation defined above. Formally, for any considered sequence of vectors ${\bm{x}}_{1},{\bm{x}}_{2},\dots,{\bm{x}}_{n}$, denote the attention output as ${\bm{o}}_{1},{\bm{o}}_{2},\dots,{\bm{o}}_{n}$. Then, we have $\|{\bm{o}}_{i}-{\bm{u}}_{i}\|_{\infty}\leq\epsilon$ for all $i\in[n]$ with ${\mathcal{S}}_{i}\neq\emptyset$. Moreover, the $\ell_{\infty}$ norm of attention parameters is bounded by $O(\mathrm{poly}(M,1/\delta,\log(n),\log(1/\epsilon)))$.

###### Assumption C.4 .

###### Lemma C.5 (Lemma C.7 from Feng et al. ( 2023 ) ) .

###### Lemma C.6 (Lemma C.8 from Feng et al. ( 2023 ) ) .

### C.3 Theoretical Construction

Preprint Note: We’re in the process of reformatting the construction and proof for better organization

##### Notations

- •
$p$ denotes the number of variables
- •
$t_{i}$ denotes the token at position $i$
- •
$T_{vars}$ denotes the set of tokens that denote variables and their negations. i.e. ‘1’, ‘2’, $\dots$, ‘n’, ‘-1’, ‘-2’, $\dots$, ‘-n’
- •
$b$ 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.

###### Proof.

##### Input Format.

We consider 3-CNF-SAT formulas in the DIMACS representation, with an initial [BOS] token and an ending [SEP] token. Each variable $x_{i}$ for $i\in[n]$ has 2 associated tokens: i and -i (e.g., 1 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

$$ $\displaystyle(\lnot x_{2}\lor\lnot x_{4}\lor\lnot x_{1})\land(x_{3}\lor x_{4}\lor\lnot x_{1})\land(\lnot x_{1}\lor\lnot x_{3}\lor\lnot x_{2})$ $\displaystyle\land(x_{1}\lor\lnot x_{2}\lor\lnot x_{4})\land(\lnot x_{4}\lor x_{2}\lor x_{1})\land(x_{1}\lor\lnot x_{2}\lor x_{4})$ $$

would be represented as:

[BOS] -2 -4 -1 0 3 4 -1 0 -1 -3 -2 0 1 -2 -4 0 -4 2 1 0 1 -2 4 0 [SEP]

##### Solution Trace Format.

The trace keeps track of the order of the assignments made and whether each assignment is a decision (assumption) or a unit propagation (deduction). Literals with a preceding D token are decision literals while other literals are from unit propagation. When the model encounters a conflict between the current assignment and the formula, it performs a backtrack operation denoted by [BT] and performs another attempt with the last decision literal negated. In particular, compared to [Figure 1](#S1.F1), we used D to abbreviate Assume and use [BT] to abbreviate Backtrack

As an example, the solution trace for the above SAT formula would be:
[SEP] D 2 D 1 -4 3 [BT] D 2 D -1 -4 [BT] -2 D 3 D 4 -1 SAT

##### Embedding Layer.

Our token set consists of one token for each variable and its negation, the separator token 0, and a special token D to denote where decisions are made. The positional encoding occupies a single dimension and contains the numerical value of the position of the token in the string. (i.e. there exists a dimension $pos$ such that the position embedding of position $i$ is $i\cdot\mathbf{e}_{pos}$)

##### Layer 1.

The first layer prepares for finding the nearest separator token and $D$ token. Let $i$ denote the position index of tokens:

- 1.
Compute $i_{\text{sep}}$ where $i_{\text{sep}}=i$ if the corresponding token $t_{i}\in\{\text{`{0}', `{[SEP]}', `{[BT]}'}\}$ and $i_{\text{sep}}=0$ otherwise
- 2.
Similarly, compute $i_{\texttt{D}}$ where $i_{\texttt{D}}=i$ if the corresponding token $t_{i}=\texttt{D}$ and $i_{\text{sep}}=0$ otherwise.
- 3.
Compute $(i-1)^{2}$, $i^{2}$ for index equality comparison

The first 2 operations can both be computed using a single MLP layer that multiplies between $i$ from the positional encoding using [Lemma C.3](#A3.Thmtheorem3). Similarly, the 3rd operation is a multiplication operation that can be performed with [Lemma C.3](#A3.Thmtheorem3).

##### Layer 2.

This layer uses 2 heads to perform the following tasks:

- 1.
Copy the index and type of the last separator token and stores
$\displaystyle p_{i}^{sep}{}^{\prime}$
$\displaystyle=\max\{j:j\leq i,t_{j}\in\{\text{`{0}', `{[SEP]}', `{[BT]}'}\}\}$
$\displaystyle b_{\texttt{0}}$
$\displaystyle=(t_{j}=\text{`{0}'})$
$\displaystyle b_{\texttt{[SEP]}}$
$\displaystyle=(t_{j}=\text{`{[SEP]}'})$
$\displaystyle b_{\texttt{[BT]}}$
$\displaystyle=(t_{j}=\text{`{[BT]}'})$
for $j=p_{i}^{sep}{}^{\prime}$
- 2.
(Backtrack) Compute the position of the nearest D token $p_{i}^{\texttt{D}}=\max\{j:j\leq i,t_{j}=\text{`{D}'}\}$
- 3.
Compute $(p_{i}^{sep}{}^{\prime})^{2}$ for index operation

Task 1 can be achieved via the COPY operation from [Lemma C.5](#A3.Thmtheorem5) with ${\bm{q}}_{i}=1$, ${\bm{k}}_{i}=i_{\text{sep}}$, ${\bm{v}}_{j}=(j,\mathbb{I}[t_{j}=\text{`{0}'}],\mathbb{I}[t_{j}=\text{`{[SEP]}'}],\mathbb{I}[t_{j}=\text{`{[UP]}'}],\mathbb{I}[t_{j}=\text{`{[BackTrack]}'}])$.

Task 2 is highly similar to task 1 and can be achieved using COPY with ${\bm{q}}_{i}=1$, ${\bm{k}}_{i}=i_{\texttt{D}}$, ${\bm{v}}_{j}=(j)$

Task 3 is a multiplication operation that can be performed using [Lemma C.3](#A3.Thmtheorem3).

##### Layer 3

This layer uses 1 head to copy the several values from the previous token to the current token. Specifically, this layer computes:

- 1.
The position of the previous separator token, not including the current position:
$p_{i}^{sep}=\max\{j:j<i,t_{j}\in\{\text{`{0}', `{[SEP]}',`{[UP]}', `{[BackTrack]}'}\}\}$
- 2.
Dermine if the previous token is D: $b_{decision}=(t_{i-1}=\text{`{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}^{sep}=i-p_{i}^{sep}{}^{\prime}$
- 4.
Compute $(p_{i}^{sep})^{2}$, for equality comparison at the next layer.

Task 1 and 2 is done by copying $p_{i}^{sep}{}^{\prime}$ and $\mathbb{I}[t_{i}=\text{`{D}'}]$ from the previous token. Specifially, we use the COPY operation from [Lemma C.5](#A3.Thmtheorem5) with ${\bm{q}}_{i}=((i-1)^{2},i-1,1)$ and ${\bm{k}}_{j}=(-1,2j,-j^{2})$ which determines $i-1=j$ via $-((i-1)-j)^{2}=0$ and ${\bm{v}}_{j}=(p_{i}^{sep}{}^{\prime},\mathbb{I}[t_{i}=\text{`{D}'}])$.
Task 4 is a local multiplication operation that can be implemented via [Lemma C.3](#A3.Thmtheorem3).

##### Layer 4.

This layer uses 2 heads to perform the following tasks:

- 1.
Compute the sum of all variable token embeddings after the previous separator to encode a vector representation of assignments and clauses at their following separator token.
$\mathbf{r}_{i}=\sum_{j>p_{i}^{sep},t_{j}\in T_{vars}}\mathbf{e}_{id(t_{j})}=\sum_{p_{j}^{sep}=p_{i}^{sep},t_{j}\in T_{vars}}\mathbf{e}_{id(t_{j})}$
- 2.
(Induction) Compute the position of the second-to-last separator $p_{i}^{sep-}=\max\{j:j<p_{i}^{sep},t_{j}\in\{\text{`{0}', `{[SEP]}',`{[UP]}', `{[BackTrack]}}^{\prime}\}\}=p_{p_{i}^{sep}{}^{\prime}}^{sep}$ and the corresponding current position in the previous state $p_{i}^{-}=p_{i}^{sep-}+d_{i}^{sep}$. As a special case for the first state, we also add $4$ to $p_{i}^{-}$ if $b_{\texttt{[SEP]}}$ is true, i.e. $p_{i}^{-}=p_{i}^{sep-}+d_{i}^{sep}+4\cdot b_{\texttt{[SEP]}}$. The additional $4$ is the number of variables per clause + 1 to ensure that we don’t consider the last clause as an assignment.
- 3.
(Backtrack) Compute the position of the nearest D token to the last separator token $p_{i}^{\texttt{D}-}=p_{p_{i}^{sep}{{}^{\prime}}}^{\texttt{D}}$
- 4.
Compute $b_{exceed}=(p_{i}^{-}>p_{i}^{\texttt{D}-}+1)$, this denotes whether we’re beyond the last decision of the previous state.
- 5.
Compare $(p_{i}^{\texttt{D-}}\leq p_{i}^{-})$ for $b_{\text{BT_finished}}$ at the next layer.
- 6.
Compare if $p_{i}^{\texttt{D-}}=p_{i}^{-}$ for the $b_{backtrack}$ operator.
- 7.
Compute $b_{copy}^{\prime}=(p_{i}^{-}<p_{i}^{sep}{}^{\prime}-1)$

Task 1 is achieved using a MEAN operation with ${\bm{q}}_{i}=((p_{i}^{sep})^{2},p_{i}^{sep},1)$, ${\bm{k}}_{j}=((-1,2p_{j}^{sep},-(p_{j}^{sep})^{2})$, ${\bm{v}}_{j}=\mathbf{e}_{id(t_{j})}$ for $t_{j}\in T_{vars}$. This attention operations results in $\frac{\mathbf{r}_{i}}{i-p_{i}^{sep}}$ The MLP layer then uses [Lemma C.3](#A3.Thmtheorem3) to multiply the mean result by $i-p_{i}^{sep}$ to obtain the $\mathbf{r}_{i}$.

Task 2 is achieved using the COPY operation with ${\bm{q}}_{i}=((p_{i}^{sep})^{2},p_{i}^{sep},1)$, ${\bm{k}}_{j}=(-1,2j,-j^{2})$ and ${\bm{v}}_{j}=p_{i}^{sep}{}^{\prime}$. The MLP layer then performs the addition operation the computes $p_{i}^{-}$ by [Lemma C.2](#A3.Thmtheorem2)

Similarly, Task 3 is achieved using the COPY operation with ${\bm{q}}_{i}=((p_{i}^{sep})^{2},p_{i}^{sep},1)$, ${\bm{k}}_{j}=(-1,2j,-j^{2})$ and ${\bm{v}}_{j}=p_{i}^{\texttt{D}}$.

##### Layer 5.

The third layer uses 5 heads to perform the following tasks:

- 1.
Determine whether the current assignment $\mathbf{r}_{i}$ satisfies the formula. $b_{sat}$
- 2.
Determine whether the current assignment $\mathbf{r}_{i}$ results in a contradiction with a clause of the formula $b_{cont}$
- 3.
Find clauses with at least 2 False literals and sum up the unassigned literals in these clauses. This would result in all the variables that can be currently determined via unit propagation. ${\mathbf{e}}_{UP}$
- 4.
Compute $b_{final}=b_{exceed}\land b_{decision}$
- 5.
Compare $b_{no_decision}=(p_{i}^{\texttt{D}}\leq p_{i}^{sep})$, which denotes whether the current state contains no decision variables
- 6.
Compute $b_{\text{BT_finished}}=(p_{i}^{\texttt{D-}}\leq p_{i}^{-})\land b_{\texttt{[BackTrack]}}$
- 7.
Compare $p_{i}^{-}$ with $p_{i}^{\texttt{D}-}-1$ by storing $p_{i}^{-}\leq p_{i}^{\texttt{D}-}-1$ and $p_{i}^{-}\geq p_{i}^{\texttt{D}-}-1$ (to check for equality at the next layer)
- 8.
Compare $b_{\text{backtrack}}=(p_{i}^{-}=p_{i}^{\texttt{D}-}-1)$

To describe the operations performed in this layer, we interpret the ${\mathbf{r}}_{i}$ vectors computed in the previous layer as a $2n$-dimensional binary encoding of the clause/assignment preceding token $i$. The value at dimension $2j-1$ is 1 if the clause/assignment contains variable $j$ (1-indexed) in positive polarity and the value at dimension $2j$ is one iff the clause/assignment contains variable $j$ is in negative polarity.
For example, the clause 1 -2 4 is represented as the binary vector ${\mathbf{r}}=[1,0,0,1,0,0,1,0]$ when the number of variables is $n=4$. The ${\mathbf{r}}$ representation for each clause is at the ‘0’ separator following the clause in the input format.

We now define the linear transformation $T[{\mathbf{v}}_{true},{\mathbf{v}}_{false},{\mathbf{v}}_{none}]\in\mathbb{R}^{2n\times 2n}$ where ${\mathbf{v}}_{true},{\mathbf{v}}_{false},{\mathbf{v}}_{none}\in\{(0,0),(0,1),(1,0),(1,1)\}$. The transformation takes every pair of values in ${\mathbf{r}}$ corresponding to each variable, determines whether the variable is true, false, or none-existent in the clause/assignment represented by ${\mathbf{r}}$, and replaces each pair with the corresponding ${\mathbf{v}}_{true},{\mathbf{v}}_{false},{\mathbf{v}}_{none}$ value.

For example, when ${\mathbf{r}}=[1,0,0,1,0,0,1,0]$, applying $T[(1,1),(1,0),(0,1)]$ will result in $[1,1,1,0,0,1,1,1]$. Also, $T[(1,0),(0,1),(0,0)]$ is equivalent to the identity operation. Intuitively, the transformation changes 2-element binary vectors representing true, false, and non-existence within the clause/assignment. The transformation is used to construct query and key matrices to satisfy the desired properties of the assignment-clause dot product.

##### Parallel Deduction over Clauses

Task 1 (checking satisfiability) is achieved via an MEAN [Lemma C.6](#A3.Thmtheorem6) with ${\mathbf{q}}_{i}=({\mathbf{r}}_{i},1)$ and ${\mathbf{k}}_{j}=M(-{\mathbf{r}}_{j},c_{j}^{(1)})$ and $v_{j}=\bm{1}[t_{j}=\text{`{[BOS]}'}]$, where

$$ $c_{j}^{(1)}=\begin{cases}0&t_{j}=\text{`{0}'},\\ -0.5&t_{j}=\text{`{[BOS]}'}\\ -M&otherwise\end{cases}$ $$

and $M$ is a sufficiently large constant to approximate hard-max with the softmax operation.

Correctness: Consider the case where ${\mathbf{r}}_{i}$ denotes the binary encoding of the current assignment and ${\mathbf{r}}_{j}$ denotes the binary encoding of a clause at a ‘0’ separator position. Then ${\mathbf{r}}_{i}\cdot{\mathbf{r}}_{j}$ denotes the number of common literals in the assignment and the clause, i.e. how many literals in the clause are True according to the assignment ${\mathbf{r}}_{i}$. Therefore, the clause is satisfied by the assignment ending at position $i$ as long as ${\mathbf{r}}_{i}\cdot{\mathbf{r}}_{j}\geq 1$. Since we only consider the ${\mathbf{r}}_{j}$ values at the ‘0’ separators as the binary encoding of the clause, all these positions have $c_{j}^{(1)}=0$. Therefore, ${\mathbf{q}}_{i}\cdot{\mathbf{k}}_{j}=-M{\mathbf{r}}_{i}\cdot{\mathbf{r}}_{j}$, which is 0 0 for non-satisfied clauses and $<-M$ for satisfied clauses. Also notice that since $c_{j}^{(1)}=-0.5$ for $j=1$ (i.e. the first [BOS] token), so ${\mathbf{q}}_{i}\cdot{\mathbf{k}}_{1}=-\frac{M}{2}$. If the formula is satisfied, all clauses must be satisfied, and each clause must have attention score ${\mathbf{q}}_{i}\cdot{\mathbf{k}}_{j}<-M$ while the [BOS] token has attention score $-\frac{M}{2}$. For sufficiently large $M$, we can view the softmax operation as selecting the value vector of the largest attention score item, which is [BOS]. Since $v_{1}=\bm{1}[t_{1}=\text{`{[BOS]}'}=1$, the result of the attention head will be $1$. Conversely, if at least one clause is not satisfied, then ${\mathbf{q}}_{i}\cdot{\mathbf{k}}_{j}=0$ for that particular clause. As such, the [BOS] token will not be selected and the result of the attention operation will be 0 0.

Similarly, task 2 (Detecting Conflict) is also achieved via MEAN([Lemma C.6](#A3.Thmtheorem6)) with ${\mathbf{q}}_{i}=(T[(1,0),(0,1),(1,1)]{\mathbf{r}}_{i},1)$, ${\mathbf{k}}_{j}=M(-{\mathbf{r}}_{j},c_{j}^{(1)})$, $v_{j}=1-\bm{1}[t_{j}=\text{`{[BOS]}'}]$, where the definition of $M$ and $c_{j}^{(1)}$ is the same as Task 1.

For task 3 (unit propagation), apply MEAN ([Lemma C.6](#A3.Thmtheorem6)) with ${\mathbf{q}}_{i}=(T[(0,1),(1,0),(0,0)]{\mathbf{r}}_{i},1)$, ${\mathbf{k}}_{j}=M({\mathbf{r}}_{j},c_{j}^{(2)})$, ${\mathbf{v}}_{j}=c{\mathbf{r}}_{j}$ where

$$ $c_{j}^{(2)}=\begin{cases}0&t_{j}=\text{`{0}'},\\ 1.5&t_{j}=\text{`{[BOS]}'}\\ -M&otherwise\end{cases}$ $$

Let the attention result be ${\mathbf{o}}_{UP}$.
The MLP layer then computes ${\mathbf{e}}_{UP}=ReLU({\mathbf{o}}_{UP})-ReLU({\mathbf{o}}_{UP}-1)-T[(1,1),(1,1),(0,0)]{\mathbf{r}}_{i}$ via [Lemma C.1](#A3.Thmtheorem1).

Correctness: Here we show that, if the assignment at position $i$ does not make the formula unsatisfied, then the resulting vector is approximately a binary encoding of all literals that can be unit-propagated. Consider again the case where ${\mathbf{r}}_{i}$ denotes the binary encoding of the current assignment and ${\mathbf{r}}_{j}$ denotes the binary encoding of a clause at a ‘0’ separator position. Here ${\mathbf{q}}_{i}\cdot{\mathbf{k}}_{j}$ denotes $M$ times the number of false literals in clause $j$ according to the current assignment $i$. Since each clause has three variables, if a clause has three false assignments, then the formula is unsatisfied by the assignment and thus requires no further unit propagation. Therefore, we consider the case where each clause has at most 2 opposing assignments.

If there are no clauses with 2 opposing assignments, then all clause attention logits ${\mathbf{q}}_{i}\cdot{\mathbf{k}}_{j}$ will be at most $M$, while the attention logit to the $\tt{[BOS]}$ token will be $c_{1}^{(2)}=1.5M$. Since $M$ is a large number, most attention weights will be assigned to $\tt{[BOS]}$ after the softmax operation and result in a zero embedding vector.

If at least one clause has 2 opposing assignments, all these clauses will have attention logits ${\mathbf{q}}_{i}\cdot{\mathbf{k}}\approx 2M$. Therefore, the attention value will be evenly distributed on all clauses with 2 opposing assignments. The resulting attention output ${\mathbf{o}}_{[UP]}$ will be the average of embedding of all clauses with 2 opposing assignments, multiplied by $c$ since ${\mathbf{v}}_{j}=c\cdot{\mathbf{r}}_{j}$. Since there are at most $c$ clauses, the number of attended clauses is at most $c$, and the divisor when computing the average is at most $c$. Therefore, the resulting ${\mathbf{o}}_{[UP]}$ will be a embedding vector where every literal that appeared in at least one clause with 2 false literals have their corresponding position assigned to a $\geq 1$ value.

##### Layer 6

This layer does the remaining boolean operators required for the output. In particular,

- •
$b_{unsat}=b_{no_decision}\land b_{cont}$
- •
$b_{\texttt{[BT]}}=b_{cont}\land\lnot(t_{i}=\texttt{[BT]})$
- •
Compute a vector that is equal to $b_{backtrack}\cdot{\mathbf{e}}_{BT}$, which is equal to ${\mathbf{e}}_{BT}$ if $b_{backtrack}$ is True and $\bm{0}$ otherwise. This is to allow the operation at the output layer for backtracking

Note that $\land$ can be implemented as a single ReLU operation for tasks 1 and 2 that can be implemented with [Lemma C.1](#A3.Thmtheorem1), and task 3 is a multiplication operation implemented with [Lemma C.3](#A3.Thmtheorem3)

##### Layer 7

This layer performs a single operation with the MLP layer: Compute $b_{copy}\cdot e_{copy}$, which gates whether $e_{copy}$ should be predicted based on $b_{copy}$. This enables condition 5 at 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 conditional in the order below:

- 1.
If $b_{sat}$ output SAT
- 2.
If $b_{cont}\land b_{no_decision}$ output UNSAT
- 3.
If $b_{cont}\land\lnot(t_{i}=\texttt{[BackTrack]})$ output ‘[BackTrack]’
- 4.
(BackTrack) If $b_{backtrack}$, output the negation of the token from position $p_{i}^{\texttt{D}-}+1$
- 5.
(Induction) If $b_{copy}$, copy token from position $p_{i}^{-}+1$ as output ($e_{copy}$)
- 6.
output a unit propagation variable, if any.
- 7.
output D if the current token is not D
- 8.
output a unassigned variable

For the output layer, we use $l_{\texttt{[TOKEN]}}$ to denote the output logit of [TOKEN]. Since the final output of the model is the token with the highest logit, we can implement output priority by assigning outputs of higher priority rules with higher logits than lower priority rules. Specifically, we compute the output logits vector using the output layer linear transformation as:

$$ $2^{7}\cdot b_{sat}\cdot{\mathbf{e}}_{\texttt{SAT}}+2^{6}\cdot b_{cont}\cdot{\mathbf{e}}_{\texttt{[BackTrack]}}+2^{5}\cdot b_{unsat}\cdot{\mathbf{e}}_{\texttt{UNSAT}}$ $$

$$ $+2^{4}\cdot b_{backtrack}\cdot{\mathbf{e}}_{BT}+2^{3}\cdot b_{copy}\cdot{\mathbf{e}}_{copy}+2^{2}\cdot{\mathbf{e}}_{\texttt{UnitPropVar}}+2^{1}\cdot(1-\bm{1}[t_{i}=`\texttt{D}^{\prime}])\cdot{\mathbf{e}}_{\texttt{D}}+2^{0}\cdot T[(0,0),(0,0),(1,1)]{\mathbf{r}}_{i}$ $$

∎

###### Proposition C.7 .

There exists a transformer with 7 layers, 5 heads, $O(p)$ embedding dimension, and $O(p^{2})$ weights that, on all inputs ${\bm{s}}\in\operatorname{DIMACS}(p,c)$, predicts the same token as the output as the above operations. Furthermore, let $l_{ctx}=4c+p\cdot 2^{p}$ be the worst-case maximum context length required to complete SAT-solving, then all weights are within $\operatorname{poly}(l_{ctx})$ and can be represented within $O(p+\log c)$ bits.

We only argue from a high level why this is true due to the complexity of the construction. In the above construction, we demonstrate how each operation can be approximated by a Self-attention or MLP layer. We can set the embedding dimension to the sum 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 in 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.

The only intermediate values whose dimensions are dependent on $p$ 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, shows that all parameter values are polynomial with respect to the context length and the inverse of approximation errors. Note that we need only guarantee the final error is less than 1 to prevent affecting the output token. Furthermore, we can choose all parameter values so that they are multiples of $0.5$. As such, all parameters are within $\operatorname{poly}(l_{ctx})$ and can be represented by $O(\log(l_{ctx}))=O(p+\log c)$

###### Proposition C.7 .

### C.4 Correctness

Note: This section assumes prior knowledge in propositional logic and SAT solving, including an understanding of the DPLL algorithm. For a brief explanation of the notations in this section, please refer to (Nieuwenhuis et al. ()). For more general knowledge, please refer to (Biere et al. ()).

We prove that the above model autoregressive solves $\operatorname{3-SAT}_{p,c}$ by showing that it uses the CoT to simulate the “Abstract DPLL Procedure”.

#### C.4.1 Abstract DPLL

In this section, we provide a 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. () 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 propagation (i.e., deduction).

For example, the ordered trace $3^{d}\>1\>\overline{2}\>4^{d}\>5$ denotes the following sequence of operations:

Assume $x_{3}=T\rightarrow$ Deduce $x_{1}=T\rightarrow$ Deduce $x_{2}=F\rightarrow$ Assume $x_{4}=T\rightarrow$ Deduce $x_{5}=T$.

Let $F$ denote the a SAT formula in CNF format (which includes 3-SAT), $C$ denote a clause (e.g., $x_{1}\lor\lnot x_{2}\lor x_{3}$), $l$ denote a single literal (e.g., $\lnot x_{2}$), and $l^{d}$ denote a decision literal. Let $M\models F$ denote that the assignment in $M$ satisfies the formula $F$.

###### Definition C.8 (State in the DPLL Transition System) .

A *state* $S\in{\mathbb{S}}$ in the DPLL transition system is either:

- •
The special states $\operatorname{SAT},\operatorname{UNSAT}$, indicating that the formula satisfiable or unsatisfiable
- •
A pair $M\parallel F$, where:
–
$F$ is a finite set of clauses $C_{1}\land C_{2}\dots\land C_{c}$ (a conjunctive normal form (CNF) formula), and
–
$M$ is a sequence of annotated literals $l_{1}\circ l_{2}\dots\circ l_{i}$ for some $i\in[n]$ representing variable assignments, where $\circ$ denotes concatenation. Annotations indicate whether a literal is a decision literal (denoted by $l^{\mathrm{d}}$) or derived through unit propagation.

We denote the empty sequence of literals by $\emptyset$, unit sequences by their only literal, and the concatenation of two sequences by simple juxtaposition. While $M$ is a sequence, it can also be viewed as a set of variable assignments by ignoring annotations and order.

###### Definition C.9 (Adapted from Definition 1 of Nieuwenhuis et al. ( 2005 ) ) .

The Basic DPLL system consists of the following transition rules ${\mathbb{S}}\Longrightarrow{\mathbb{S}}$:

$$ $\displaystyle\operatorname{UnitPropagate}:$ $\displaystyle M\,$ $\displaystyle\|\,F\land(C\lor l)$ $\displaystyle\quad\Longrightarrow\quad$ $\displaystyle M\circ l\,\|\,F\land(C\lor l)$ if $\displaystyle\begin{cases}M\models\neg C,\\ l\text{ is undefined in }M.\end{cases}$ $\displaystyle\operatorname{Decide}:$ $\displaystyle M\,$ $\displaystyle\|\,F$ $\displaystyle\quad\Longrightarrow\quad$ $\displaystyle M\circ l^{\mathrm{d}}\,\|\,F$ if $\displaystyle\begin{cases}l\text{ or }\neg l\text{ occurs in a clause of }F,\\ l\text{ is undefined in }M.\end{cases}$ $\displaystyle\operatorname{Backjump}:$ $\displaystyle M\circ l^{\mathrm{d}}\circ N\,$ $\displaystyle\|\,F$ $\displaystyle\quad\Longrightarrow\quad$ $\displaystyle M\circ l^{\prime}\,\|\,F$ if $\displaystyle\begin{cases}\text{There is some clause }C\lor l^{\prime}\text{ s.t. }\\ F\models C\lor l^{\prime},\quad M\models\lnot C,\\ l^{\prime}\text{ is undefined in }M,\\ l^{\prime}\text{ or }\neg l^{\prime}\text{ occurs in a clause of }F.\end{cases}$ $\displaystyle\operatorname{Fail}:$ $\displaystyle M\,$ $\displaystyle\|\,F\land C$ $\displaystyle\quad\Longrightarrow\quad$ $\displaystyle\operatorname{UNSAT}$ if $\displaystyle\begin{cases}M\models\neg C,\\ M\text{ contains no decision literals.}\end{cases}$ $\displaystyle\operatorname{Success}:$ $\displaystyle M\,$ $\displaystyle\|\,F$ $\displaystyle\quad\Longrightarrow\quad$ $\displaystyle\operatorname{SAT}$ if $\displaystyle M\models F$ $$

We also use $S\Longrightarrow^{*}S^{\prime}$ to denote that there exist $S_{1},S_{2},\dots,S_{i}$ such that $S\Longrightarrow S_{1}\Longrightarrow\dots\Longrightarrow S_{i}\Longrightarrow S^{\prime}$. Also $S\Longrightarrow^{!}S^{\prime}$ denote that $S\Longrightarrow^{*}S^{\prime}$ and $S^{\prime}$ is a final state ($\operatorname{SAT}$ or $\operatorname{UNSAT}$).

Explanation of the $\operatorname{Backjump}$ Operation:

The $\operatorname{Backjump}$ operation allows the DPLL algorithm to backtrack to a previous decision and learn a new literal. In particular, $F\models C\lor l^{\prime}$ means that, for some clause $C$, every assignment that satisfies $F$ must either satisfy $C$ (i.e., contain the negation of each literal in $C$) or contain $l^{\prime}$ as an assignment. However, if $M\models\lnot C$, which means that $M$ conflicts with $C$ 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 $l^{\prime}$ as an assignment to ensure that it satisfies $C\lor l^{\prime}$, a requirement for satisfying $F$.

In our construction, we only consider the narrower set of $\operatorname{BackTrack}$ operations that find the last decision and negate it:

###### Lemma C.10 .

[Corrollary of Lemma 6 from Nieuwenhuis et al. ()]
Assume that $\emptyset\parallel F\Longrightarrow^{*}M\circ l^{\mathrm{d}}\circ N\,\|\,F$, the $\operatorname{BackTrack}$ operation:

$$ $\displaystyle M\circ l^{\mathrm{d}}\circ N\,$ $\displaystyle\|\,F$ $\displaystyle\quad\Longrightarrow\quad$ $\displaystyle M\circ\lnot l\,\|\,F$ if $\displaystyle\begin{cases}\text{There exists clause }C\text{ in }F\text{ such that}\\ M\circ l^{\mathrm{d}}\circ N\models\lnot C\\ N\text{contains no decision literals}\\ \end{cases}$ $$

is always a valid $\operatorname{Backjump}$ operation in [Definition C.9](#A3.Thmtheorem9).

###### Definition C.11 (Run of the DPLL Algorithm) .

A *run* of the DPLL algorithm on formula $F$ is a sequence of states $S_{0}\Longrightarrow S_{1}\Longrightarrow\dots\Longrightarrow S_{T}$ such that:

- •
$S_{0}$ is the initial state $\emptyset\parallel F$
- •
For each $i=0,1,\dots,n-1$, the transition $S_{i}\Longrightarrow S_{i+1}$ is valid according to the transition rules of the DPLL system in [Definition C.9](#A3.Thmtheorem9) (e.g., $\operatorname{UnitPropagate}$, $\operatorname{Decide}$, $\operatorname{Backjump}$, or $\operatorname{Fail}$);
- •
$S_{n}$ is a final state that is either $\operatorname{SAT}$ or $\operatorname{UNSAT}$

Note that the above definition is simply the expansion of $\emptyset\parallel F\Longrightarrow^{!}S_{T}$.

The following theorem states that the DPLL procedure always decides the satisfiability of CNF formulas:

###### Lemma C.12 .

[Theorem 5 and Theorem 9 Combined from Nieuwenhuis et al. ()]
The Basic DPLL system provides a decision procedure for the satisfiability of CNF formulas $F$. Specifically:

- 1.
$\emptyset\parallel F\Longrightarrow^{!}\operatorname{UNSAT}$ if and only if $F$ is unsatisfiable.
- 2.
$\emptyset\parallel F\Longrightarrow^{!}\operatorname{SAT}$ if and only if $F$ is satisfiable.
- 3.
There exist no infinite sequences of the form $\emptyset\parallel F\Longrightarrow S_{1}\Longrightarrow\cdots$

###### Definition C.8 (State in the DPLL Transition System) .

###### Definition C.9 (Adapted from Definition 1 of Nieuwenhuis et al. ( 2005 ) ) .

###### Lemma C.10 .

###### Definition C.11 (Run of the DPLL Algorithm) .

###### Lemma C.12 .

#### C.4.2 Trace Equivalence and Inductive Proof

We demonstrate that our Transformer in [Theorem 4.5](#S4.Thmtheorem5) solves SAT by showing that the CoT produced by the Transformer is ”trace equivalent” to an abstract DPLL algorithm with some heuristic. We first provide definition of “trace equivalence”:

###### Definition C.13 (Trace Equivalence of Algorithms) .

Let $A$ and $B$ be two algorithms. Let $\Sigma_{A}$ and $\Sigma_{B}$ be the sets of possible states of $A$ and $B$, respectively. We say that algorithms $A$ and $B$ are *trace equivalent* if there exists a bijective mapping $\phi:\Sigma_{A}\rightarrow\Sigma_{B}$, independent of the input, such that for every input $s$, the traces produced by $A$ and $B$ satisfy the following:

If the execution of $A$ on input $s$ produces the trace $\mathrm{Tr}_{A}(s)=[\sigma_{1}^{A},\sigma_{2}^{A},\dotsc,\sigma_{n}^{A}]$, and the execution of $B$ on the same input $s$ produces the trace $\mathrm{Tr}_{B}(s)=[\sigma_{1}^{B},\sigma_{2}^{B},\dotsc,\sigma_{n}^{B}]$, then for all $i\in\{1,2,\dotsc,n\}$,

$$ $\sigma_{i}^{B}=\phi(\sigma_{i}^{A}).$ $$

That is, the sequences of states of $A$ and $B$ are in one-to-one correspondence via the fixed mapping $\phi$, and corresponding states are related by this mapping for every input $s$.

We first show how to convert a chain of thought of the model into a state in the abstract DPLL algorithm. Consider the following model input and Chain-of-Thought trace:

[BOS] -2 -4 -1 0 3 4 -1 0 -1 -3 -2 0 1 -2 -4 0 -4 2 1 0 1 -2 4 0 [SEP] D 2 D 1 -4 3 [BT] D 2 D -1 -4

Recall that [BT] denotes backtracking and D denotes that the next token is a decision literal.

Note that the prompt input ends at [SEP] and the rest is the Chain-of-Though produced by the model.

We want to convert this trace to a 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 D 2 D -1 -4 portion of the trace and thus $M=2^{d}\>\bar{1}^{d}\>\bar{4}$ as described in [Section C.4.1](#A3.SS4.SSS1). We formalize this process as follows:

###### Definition C.14 (Translating CoT to Abstract DPLL State) .

For any number of variables $p\in{\mathbb{N}}^{+}$, let ${\mathcal{V}}$ be the set of tokens:

$$ ${\mathcal{V}}=\{\,\texttt{-i},\ \texttt{i}\mid i\in[p]\,\}\cup\{\,\texttt{D},\ \texttt{[SEP]},\ \texttt{[BOS]},\ \texttt{[BT]},\ \texttt{0},\ \texttt{SAT},\ \texttt{UNSAT}\,\}.$ $$

Define a mapping $f_{{\mathcal{S}}}:{\mathcal{V}}^{*}\rightarrow{\mathcal{S}}\cup\{\operatorname{error}\}$ that converts a sequence of tokens $R\in{\mathcal{V}}^{*}$ into an abstract DPLL state as follows:

- 1.
If $R$ ends with SAT or UNSAT, then set $M_{{\mathcal{S}}}(R)$ to $\operatorname{SAT}$ or $\operatorname{UNSAT}$ accordingly.
- 2.
Else if $R$ contains exactly one [SEP] token, split $R$ at [SEP] into $R_{\text{DIMACS}}$ and $R_{\text{Trace}}$.
- 3.
Parse $R_{\text{DIMACS}}$ into a CNF formula $F$, assuming it starts with [BOS] and ends with 0. If parsing fails, set $M_{{\mathcal{S}}}(R)=\operatorname{fail}$.
- 4.
Initialize an empty sequence $M$ to represent variable assignments and set a flag $\textit{isDecision}\leftarrow\texttt{False}$.
- 5.
Process each token $t$ in $R_{\text{Trace}}$ sequentially:
•
If $t=\texttt{D}$, set $\textit{isDecision}\leftarrow\texttt{True}$.
•
Else if $t=\texttt{[BT]}$, remove literals from $M$ up to and including the last decision literal (i.e., perform backtracking).
•
Else if $t=\texttt{i}$ or -i for some $i\in[n]$:
–
Let $l$ be the literal corresponding to $x_{i}=T$ if $t=\texttt{i}$, or $x_{i}=F$ if $t=\texttt{-i}$.
–
If $l$ is already assigned in $M$ with a conflicting value, set $M_{{\mathcal{S}}}(R)=\operatorname{fail}$.
–
Else, append $l$ to $M$, annotated as a decision literal if $\textit{isDecision}=\texttt{True}$, or as a unit propagation otherwise.
–
Reset $\textit{isDecision}\leftarrow\texttt{False}$.
•
Else, set $M_{{\mathcal{S}}}(R)=\operatorname{error}$.
- 6.
Return the state $M\parallel F$.
- 7.
If any of the above steps fail, set $M_{{\mathcal{S}}}(R)=\operatorname{fail}$.

We now present the inductive lemma:

###### Lemma C.15 (Inductive Lemma) .

For any $p,c\in{\mathbb{N}}^{+}$, for any input $F_{\text{DIMACS}}\in\operatorname{DIMACS}(p,c)$ of length $n$, let $F$ be the boolean formula in CNF form encoded in $F_{\text{DIMACS}}$. Let $A$ be the model described in section [C.3](#A3.SS3) with parameters $p,c$. Let $({\bm{s}}_{1:n},{\bm{s}}_{1:n+1},\dots)$ be the trace of ${\bm{s}}$ when running the Greedy Decoding [Algorithm 1](#alg1) with model $A$ and input prompt ${\bm{s}}_{1:n}=F_{\text{DIMACS}}$.
For every $i\in{\mathbb{N}}^{+}$, if $f_{\mathcal{S}}({\bm{s}}_{1:n+i})=S$ and $S\notin\{\operatorname{SAT},\operatorname{UNSAT},\operatorname{error}\}$, then there exist $j\in{\mathbb{N}}^{+}$ and $S^{\prime}\in{\mathbb{S}}$ such that $S\Longrightarrow S^{\prime}$ and $f_{{\mathcal{S}}}({\bm{s}}_{1:n+i+j})=S^{\prime}$.

We now show trace equivalence between the model $A$ and some instantiating of the abstract DPLL with a specific heuristic:

###### Definition C.16 .

For any heuristic $h:{\mathbb{S}}\rightarrow{\mathcal{L}}$ where ${\mathcal{L}}$ is the set of literals, let $\operatorname{DPLL}$h denote an instantiation of the abstract DPLL algorithm that selects $h(S)$ as the decision literal when performing $\operatorname{Decide}$ and only performs the $\operatorname{BackTrack}$ operation for $\operatorname{Backjump}$. $h(S)$ is a valid heuristic if $\operatorname{DPLL}$h always abides by the $\operatorname{Decide}$ transition.

###### Lemma C.17 .

(Trace Simulation)
There exists a valid heuristic $h:{\mathbb{S}}\rightarrow{\mathcal{L}}$ for which the Transformer model $A$ is trace equivalent to $\operatorname{DPLL}_{h}$ on all inputs in $\operatorname{DIMACS}(p,c)$

###### Proof.

We aim to show that there exists a valid heuristic $h:\mathcal{S}\rightarrow\mathcal{L}$ such that the Transformer model $A$ is trace equivalent to $\operatorname{DPLL}_{h}$ on all inputs in $\operatorname{DIMACS}(p,c)$.

Define the heuristic $h$ as follows: For any state $S\in\mathcal{S}$, let $h(S)$ be the literal that the Transformer model $A$ selects as its next decision literal when in state $S$.

Formally, given that the model $A$ outputs tokens corresponding to decisions, unit propagations, backtracks, etc., and that these tokens can be mapped to transitions in the abstract DPLL system via the mapping $M_{\mathcal{S}}$ (as per the Translating CoT to Abstract DPLL State definition), we set:

$$ $h(S)=\begin{cases}\text{the decision literal chosen by }A\text{ in state }S,&\text{if }A\text{ performs a }\operatorname{Decide}\text{ transition},\\ \text{undefined},&\text{otherwise}.\end{cases}$ $$

This heuristic is valid because $A$ always abides by the $\operatorname{Decide}$ transition rules, ensuring $h(S)$ selects a literal that occurs in $F$ and is undefined in $M$, satisfying the conditions of a valid heuristic.

Define a mapping $\phi:\Sigma_{A}\rightarrow\Sigma_{B}$, where $\Sigma_{A}$ is the set of possible states of model $A$, and $\Sigma_{B}$ is the set of possible states of $\operatorname{DPLL}_{h}$, such that for any state $S$ in the execution trace of $A$, $\phi(S)=S$. That is, we identify the states of $A$ with the corresponding states in $\operatorname{DPLL}_{h}$ by mapping the sequence of assignments and the formula $F$ directly.

Proof of Trace Equivalence:

We proceed by induction on the number of steps in the execution trace.

*Base Case ($i=0$):*

At the beginning, both algorithms start from the initial state with no assignments:

$$ $\text{For }A:\quad S_{0}^{A}=\emptyset\parallel F,\quad\text{and}\quad\text{For }\operatorname{DPLL}_{h}:\quad S_{0}^{B}=\emptyset\parallel F.$ $$

Clearly, $\phi(S_{0}^{A})=S_{0}^{B}$.

*Inductive Step:*

Assume that after $k$ steps, the states correspond via $\phi$:

$$ $\phi(S_{k}^{A})=S_{k}^{B}.$ $$

We need to show that after the next transition, the states still correspond, i.e., $\phi(S_{k+1}^{A})=S_{k+1}^{B}$.

Suppose the model $A$ applies a $\operatorname{UnitPropagate}$ operation, transitioning from state $S_{k}^{A}$ to $S_{k+1}^{A}$ by adding a literal $l$ deduced via unit propagation.

Since unit propagation is deterministic and depends solely on the current assignment $M$ and formula $F$, $\operatorname{DPLL}_{h}$ will also apply the same $\operatorname{UnitPropagate}$ operation, transitioning from $S_{k}^{B}$ to $S_{k+1}^{B}$ by adding the same literal $l$.

Thus, $\phi(S_{k+1}^{A})=S_{k+1}^{B}$.

Suppose the model $A$ applies a $\operatorname{Decide}$ operation, transitioning from $S_{k}^{A}$ to $S_{k+1}^{A}$ by adding a decision literal $l=h(S_{k}^{A})$.

By the definition of the heuristic $h$, $\operatorname{DPLL}_{h}$ also selects $l$ as the decision literal in state $S_{k}^{B}$. Both algorithms make the same decision and transition to the same next state.

Therefore, $\phi(S_{k+1}^{A})=S_{k+1}^{B}$.

Suppose the model $A$ applies a $\operatorname{Backjump}$ operation, backtracking to a previous state and assigning a new literal.

Since $\operatorname{DPLL}_{h}$ performs only the $\operatorname{BackTrack}$ operation for $\operatorname{Backjump}$ (as per the definition), and $A$ simulates this operation, both algorithms backtrack in the same manner and update their assignments accordingly.

Thus, $\phi(S_{k+1}^{A})=S_{k+1}^{B}$.

If the model $A$ reaches a terminal state indicating $\operatorname{SAT}$ or $\operatorname{UNSAT}$, then so does $\operatorname{DPLL}_{h}$, since their sequences of transitions have been identical up to this point.

In all cases, the next state of model $A$ corresponds to the next state of $\operatorname{DPLL}_{h}$ under the mapping $\phi$. Therefore, by induction, the execution traces of $A$ and $\operatorname{DPLL}_{h}$ are such that for all $i$,

$$ $\phi(S_{i}^{A})=S_{i}^{B}.$ $$

Since the heuristic $h$ selects the same decision literals as the model $A$, and $A$ always abides by the $\operatorname{Decide}$ transition (as per its design), $h$ is a valid heuristic according to the definition provided.

∎

###### Definition C.13 (Trace Equivalence of Algorithms) .

###### Definition C.14 (Translating CoT to Abstract DPLL State) .

###### Lemma C.15 (Inductive Lemma) .

###### Definition C.16 .

###### Lemma C.17 .

###### Proof.

## Appendix D Code for Theoretical Constuction

## Peer Reviews

confidence: 3
contribution: 4
initial_rating: 8
presentation: 4
questions: 1. What is the maximum number of steps, w.r.t. the variable number, for running DPLL over the generated 3-SAT problems? How does it compare to the empirical maximum CoT length?
2. What is the accuracy of the compiled model on instances with more than 20 variables, i.e. beyond the guaranteed upper bound? Does the accuracy drop drastically?
soundness: 4
strengths: 1. This is the first work to study the capabilities of LLMs to solve NP-complete problems.
2. This paper proves by construction that LLMs can simulate the DPLL algorithm to solve the 3-SAT problem with, though, a bounded number of variables. It demonstrates that Transformers can perform unit propagation and backtracking, which are the core operations of the DPLL algorithm.
3. To support the theoretical argument, the authors also developed a compiler to compile the theoretical construction into a Transformer implementation and verified its practical capability to perfectly solve bounded 3-SAT problems.
4. The evaluation results match the theoretical statement. The main theorem implies that Transformers can perfectly solve 3-SAT problems with a bounded number of variables. In the evaluation, they also observed near-100% accuracy over problems with a bounded number of variables whereas the accuracy dropped significantly as the variable number further increased.
summary: This paper investigates the capabilities of LLMs to solve an NP-complete problem, the 3-SAT problem. The authors first prove by construction that LLMs can simulate the DPLL algorithm to solve the 3-SAT problem with a bounded number of variables. To support this theoretical argument, they also compiled a Transformer implementation from the construction, which perfectly solved the bounded 3-SAT problems in their evaluation. A further empirical investigation demonstrated that, instead of by construction, LLMs could learn to solve the bounded 3-SAT problems whereas they are unable to generalize to problems with more variables. This observation matches the limitation of the theoretical construction requiring a bounded number of variables for 3-SAT problems.
weaknesses: 1. The main theorem implies that an arbitrarily large LLM is required to simulate a general DPLL algorithm for solving all 3-SAT problems. Considering a bounded program (a program of a specific size) can implement the general DPLL algorithm, it is still unclear how to approach the general DPLL algorithm using a bounded LLM.
2. The experiment setting in Sec 6.2 contradicts the description of Figure 2. Sec 6.2 states that the model is trained on the Marginal dataset and evaluated on the three generated datasets while Figure 2 describes the other way.

---

confidence: 3
contribution: 1
initial_rating: 3
presentation: 2
questions: I have no questions for the authors.
soundness: 2
strengths: The authors present how a 3-SAT solving algorithm can be expressed within the confinements of the building blocks of the Transformer architecture and demonstrate that it remains accurate across varying numbers of involved variables and clauses.
summary: This work investigates the application of the Transformer architecture for SAT solving. 
To this end, the authors present theoretical boundaries on decoder-only Transformers' size and solving capabilities in 3-SAT problems.
Furthermore, they introduce "Parametric Transformer" (PARAT) to create and evaluate the SAT-solving model.
The evaluation itself consists of a simulation study where 3-SAT problems with varying numbers of variables have been generated as a benchmark.
The authors show how their compiled model is able to solve all problems with perfect accuracy, while models that were trained instead fail when challenged with problems of previously unseen numbers of variables.
weaknesses: The contribution and significance of PARAT remained unclear to me after considering both the main text and appendices. 
The authors claim that PARAT "is designed to provide an intuitive syntax resembling standard numerical array manipulation, akin to NumPy, [...]" (page 6, line 311). 
Considering the referenced "ParametricTransformer Code" in Appendix D, it becomes evident that the language in question is pure Python using the numpy library. 
The language "Python" is named not once in the paper, and the formulation of contributing a "compiler" with the notation "akin to" numpy and PARAT's "NumPy-like Array Syntax" (page 6, line 314) seems completely unjustified and bordering on deception.

---

confidence: 3
contribution: 1
initial_rating: 5
presentation: 3
questions: The model demonstrates poor generalization, achieving high accuracy only on SAT instances with variable counts similar to those in the training data. Performance significantly declines on larger instances, indicating that it may be learning patterns specific to the training data rather than pure logical reasoning, thus failing to fully substantiate the claim that Transformers are capable of logical reasoning.
soundness: 2
strengths: 1. Leveraging a Transformer to simulate the entire DPLL SAT-solving process, rather than focusing on optimizing specific heuristics such as variable selection, represents a novel approach.
2. The paper presents the PARAT compiler, which translates the procedural logic of the DPLL solving process into a Transformer model, achieving perfect accuracy on SAT problems with up to 20 variables and 88 clauses.
3. The trained model sustains high accuracy on SAT test instances with variable counts comparable to those in the training dataset.
summary: This paper investigates the logical reasoning capabilities of Transformer models in solving SAT problems. The authors designed a decoder Transformer to emulate the DPLL algorithm, tackling SAT through variable selection, conflict detection, and backtracking. The PARAT compiler translates high-level procedural logic into model weights, enabling practical implementation.
weaknesses: 1. The evaluation assessed only the accuracy of satisfiability predictions, without examining the correctness of the reasoning process itself. Thus, even when predictions were correct, the reasoning steps might still diverge from the intended algorithm. Additionally, there was no in-depth analysis of the accuracy drop on larger SAT instances to identify if errors arose from issues in conflict analysis, backtracking, or other specific areas.
2. The experiments compared the Chain-of-Thought (CoT) length solely with theoretical upper bounds, without including baseline comparisons. Evaluating against the reasoning steps of a standard DPLL solver or other baselines could offer a clearer perspective on the model’s reasoning capabilities.
3. The trained model shows limited generalization, performing well only on test instances with variable counts similar to those in the training data. Its accuracy declines significantly on SAT instances with up to 20 variables, possibly dropping below 50%.

---

confidence: 3
contribution: 2
initial_rating: 5
presentation: 2
questions: What is the incremental contribution of the proposed compiler compared to the prior Tracr compiler?
soundness: 3
strengths: The problem tackled in this paper is highly interesting and relevant. I appreciate the effort of theoretical analysis conducted on the reasoning capabilities of transformer models, which is a rapidly evolving and impactful area of AI research.
summary: This paper provides a theoretical analysis of the Transformer's ability to solve 3-SAT problems through chain of thoughts, along with a compiler that can output a Transformer model satisfying a given specification. The empirical results demonstrate that the Transformer can achieve high accuracy in solving small-scale 3-SAT problems.
weaknesses: This paper has several issues that need to be addressed.

First, the paper's introduction claims to answer a "fundamental question about whether LLMs can perform propositional reasoning." However, after reviewing the paper, it does not appear that the theoretical and empirical analysis provided is sufficient to conclusively answer this broad question. The analysis is focused narrowly on 3-SAT problems, and it is unclear how the results could be generalized to other propositional reasoning problems. Additionally, the model used in the experiments may not be representative of a typical large language model with billions of parameters.

Second, the proofs for the theorems presented in Section 4 are missing. While it is possible the proofs require additional space, it is necessary to at least provide a high-level outline of the proof approach in Section 4. Purely moving numerous lemmas and proofs to an appendix is an unsatisfactory way to present such a crucial part of the paper.

Third, the incremental contribution of the proposed compiler compared to the prior Tracr compiler is unclear. It appears that the primary focus of this work is on addressing implementation issues with Tracr, but the specific novel aspects are not well articulated. The paper should clearly explain what new capabilities or improvements are offered by the proposed compiler over the previous work.

---

confidence: 2
contribution: 3
initial_rating: 5
presentation: 2
questions: Having shared broad and high-level concerns regarding the paper, I encourage the authors to address these directly. 
Here is a summary of the key points:
- Do you agree that your theoretical contributions do not demonstrate the existence of a decoder-only Transformer that solves SAT? Do you believe this could be resolved with minor revisions, and if so, how would you approach this?
- How do you ensure the decision procedure in Definition 4.3 always terminates? What considerations 
lead to defining the "semantics" of a decoder-only transformer as mapping to a probability 
distribution? Is this crucial? If I am not mistaken, this perspective somewhat diverges from research 
addressing the expressiveness of transformers, such as the paper "Attention is Turing-complete", which you cite, or studies focusing on the expressiveness of single-pass or encoder-only transformers.
- Can you provide a clear and concise definition of what Parat is?
soundness: 2
strengths: - Investigating the reasoning capabilities of transformers, particularly concerning formal 
problems, is highly valuable.
- Boolean satisfiability serves as an appropriate baseline candidate.
- Supporting the initial contribution of theoretical expressiveness with experiments that 
provide a practical perspective is a sound approach.
summary: The paper contributes to research on understanding the reasoning capabilities of transformers when using the chain of thought. Its contributions are threefold:
- It asserts that a decoder-only transformer can, in principle, solve Boolean SAT using the chain-of-thought to reason similar to the DPLL algorithm.
- It introduces PARAT, described as a "compiler that takes procedural specifications as input and outputs a transformer model that implements these specifications."
- It empirically explores whether a transformer can be trained to solve SAT problems.
weaknesses: My main concerns regard the first two contributions. I categorize the weaknesses based on the contributions of this paper and order them from most important to least important in each category. 

### Transformers with CoT solve SAT
- The claim of the paper may be perceived as somewhat misleading. While it states, 
  "we construct a decoder-only Transformer that can solve SAT," the actual result 
  (Theorem 1) is that "for any $p,c \in \mathbb{N}^+$ there exists a decoder-only Transformer 
  with [...] that can decide all 3SAT instances of at most $p$ variables and $c$ clauses using CoT." 
  This is correctly described as the construction of a decoder-only Transformer for 
  a bounded version of 3SAT. Alternatively, Theorem 1 implies that the class of all 
  decoder-only Transformers solves the general 3SAT problem: given an arbitrary 
  3SAT formula, there exists a decoder-only Transformer that can reason whether it is satisfiable. 
  The distinction is significant, as this contribution of the paper is directed towards proving 
  that a single decoder-only Transformer exists for solving SAT. In fact this is not implied by Theorem 1.
- Definition 4.3 could benefit from clarification. While the intended meaning might be inferred, 
  there remains uncertainty due to the probabilistic nature of the map computed by a decoder-only 
  transformer. The pivotal question is ensuring the decision procedure always 
  terminates. It appears that a parameter may be absent in this definition, one that would 
  guarantee termination after a predetermined length if an end-of-sequence token does not 
  appear.
- The intuition behind the Transformer template constructed for Theorem 1 needs improvement.
  While Figure 1 is comprehensive, despite being oddly distant in placement within the paper, 
  the explanations from line 277 to 300 are overly abstract. Specifically, lines 288 to 294 
  lack clarity, making it difficult for the reader to grasp their meaning. This may confuse 
  the reader more than it helps.

### Parat
- The main concern is that the paper struggles to clearly define what PARAT is. The initial description 
between lines 85 to 87 reads, "We design PARAT, a compiler of high-level sequence operations in Numpy-like 
syntax into Transformer model weights, to empirically validate and analyse theoretical constructions of 
Transformer algorithms." However, there is ambiguity surrounding the terms "compiler", "high-level sequence operations", "Transformer model weights", and "Transformer algorithms". Further on line 306, it states, "... a framework for converting theoretical constructions of Transformers into practical models ...". Yet, it remains unclear what is meant by "theoretical constructions of Transformers" and how these relate to "high-level sequence operations". The first detailed exposition of PARAT (commencing with section 5.1) immediately delves into features and operations, leaving a reader, such as myself, completely perplexed as to what it truly encompasses.
- Without addressing the aforementioned ambiguities, it remains unclear why PARAT's contribution is significant for exploring the reasoning capabilities of Transformers, the paper's primary objective. While it appears to be a useful tool, developed with considerable effort, it seems to distract from the main aim of the paper and takes up space that could be used to better elucidate the first contribution.

Meta-review: This paper investigates how well LLMs can solve the 3-SAT problem. In particular, it constructs a decoder-only Transformer to solve SAT using backtracking and deduction via Chain-of-Thought (CoT). The reviews agree that this is overall an important question. Unfortunately, there is also much confusion here that should be clarified before publication. First, it is not true that this is the "first work to study the capabilities of LLMs to solve NP-complete problems," as one reviewer argued, as the following selected pointers to SAT works show:

https://github.com/casmlab/NPHardEval

Zhengyuan Shi, Min Li, Yi Liu, Sadaf Khan, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, Qiang Xu: SATformer: Transformer-Based UNSAT Core Learning. ICCAD 2023: 1-4
https://arxiv.org/abs/2209.00953

Minyu Chen, Guoqiang Li, Ling-I Wu, Ruibang Liu, Yuxin Su, Xi Chang, Jianxin Xue:
Can Language Models Pretend Solvers? Logic Code Simulation with LLMs. SETTA 2024: 102-121
https://arxiv.org/html/2403.16097v1

Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, Wynne Hsu:
Faithful Logical Reasoning via Symbolic Chain-of-Thought. ACL (1) 2024: 13326-13365

Second, in the feedback to one of the reviewers, the author argue that there is a potential misunderstanding that the paper  <<“investigates the application of the Transformer architecture for SAT solving,” whereas our primary focus is to “answer a fundamental question about whether LLMs can perform propositional reasoning,” which is a different>> To be honest, I do not see how this is different. 3SAT is NP-complete, and SAT solvers are equal to "propositional reasoning". That is also, I guess, why the abstract refers to 3SAT and SAT solvers. Finally, one reviewer points out that the "evaluation assessed only the accuracy of satisfiability predictions, without examining the correctness of the reasoning process itself." While I see the general argument of the authors provided in the rebuttal, adding such an experiment would improve the papers. Overall, this is a borderline case, and due to many open issues and missing related work, I recommend pushing for one of the next venues. Please note that this decision should not be taken as a statement regarding the usefulness of your research.

Decision: Reject