Can Transformers Reason Logically? A Study in SAT Solving

Introduction

Despite the impressive performance of Large Language Models (LLMs), their ability to perform reliable, multi-step logical reasoning remains a subject of intense debate. Critics often point to "hallucinations"—where models produce logically flawed or factually incorrect conclusions—as evidence that Transformers are merely "stochastic parrots" rather than true reasoners.

To move beyond anecdotal evidence, this paper investigates the Boolean Satisfiability Problem (SAT), specifically 3-SAT. SAT serves as the "gold standard" for deductive reasoning: it is NP-complete, meaning any problem in the complexity class NP can be reduced to it. If a Transformer can solve SAT, it possesses the fundamental machinery for formal deduction. The authors ask: Is the Transformer architecture inherently capable of the trial-and-error and deduction required for SAT, and if so, why do they often fail to generalize to larger problems?

Methods

The authors approach the problem through three distinct lenses:

1. Theoretical Construction: They prove that a decoder-only Transformer can simulate the DPLL (Davis–Putnam–Logemann–Loveland) algorithm. DPLL is a classic SAT-solving procedure that uses backtracking (trial and error) and unit propagation (deduction). Crucially, they show that a Transformer can perform logical deduction across all clauses in parallel in a single forward pass.
2. PARAT (Parametric Transformer): To bridge theory and practice, the authors developed a tool called PARAT. It allows researchers to write high-level NumPy-like code and "compile" it directly into the weights of a PyTorch Transformer model. This "compiled" model serves as a ground-truth proof of their construction.
3. Empirical Training: Instead of just programming the weights, they tested whether a standard Transformer (LLaMA-style) could learn to solve SAT by training it on algorithmic traces—step-by-step logs of the DPLL algorithm solving formulas.

Expand

Source, p. 2

Datasets

The study utilized several synthetic 3-SAT datasets, focusing on formulas near the "critical ratio" where problems are hardest to solve:

• Random: Formulas where clauses are generated entirely at random.
• Marginal: A challenging set of SAT/UNSAT pairs that differ by only a single literal, making it impossible for a model to rely on simple statistical shortcuts.
• Skewed: Formulas with biased literal distributions to test robustness against non-uniform data.
• Reasoning Traces: A new dataset of Chain-of-Thought (CoT) "paths" showing the model how to assume variable values, deduce consequences, and backtrack upon hitting a conflict.

Key Insights

• Parallel Deduction Power: While a standard Turing Machine must check clauses one by one, a Transformer’s attention mechanism allows it to evaluate the status of every single clause simultaneously. This makes the Transformer a surprisingly efficient "parallel deduction engine."
• CoT as State Management: In this framework, Chain-of-Thought isn't just "thinking out loud." It serves as the model's external memory, allowing it to store the current state of the backtracking search and "undo" bad decisions.
• The Softmax Precision Trap: The authors identify a "non-uniform" requirement: for a Transformer to solve SAT, its parameters must depend on the problem size. As the number of variables grows, the attention mechanism needs higher numerical precision (a "harder" softmax) to distinguish between relevant and irrelevant tokens.
• Why Length Generalization Fails: The paper provides a theoretical explanation for a common LLM failure: a model trained on small logic puzzles fails on larger ones because the numerical errors in the softmax function compound as the sequence length increases, eventually leading to a "logical collapse."

Key Results

The "compiled" model created via PARAT achieved 100% accuracy on all tested SAT instances, empirically validating the theoretical proof.

Furthermore, models trained on one distribution (e.g., Random) and tested on another (e.g., Skewed) of the same size maintained near-perfect accuracy (often >99%). This strong intra-length generalization suggests the models learned the actual DPLL procedure, not just statistical patterns.

Expand

Source, p. 8

However, the models hit a strict generalization wall. When models trained on 11–15 variables were tested on 20 variables, performance plummeted. This confirms that while Transformers can learn the logic of an algorithm, the architectural requirement for size-dependent precision prevents them from scaling that logic to larger inputs without retraining.

Limitations and Future Work

The primary limitation is the non-uniformity of the result. Because the weights must be tuned to the specific number of variables, we still lack a "universal" Transformer weight set that can solve SAT for any arbitrary input length.

Future work may involve investigating alternative attention mechanisms that are less sensitive to numerical compounding or exploring "looped" Transformer architectures that can iterate on a problem without being limited by fixed layer depths. The authors also suggest that their tool, PARAT, could be used to "hand-code" other complex algorithms into Transformers to better understand the limits of neural computation.

@inproceedings{pan2025can,
  author = {Leyan Pan and Vijay Ganesh and Jacob Abernethy and Chris Esposo and Wenke Lee},
  title = {{Can Transformers Reason Logically? A Study in SAT Solving}},
  booktitle = {International Conference on Machine Learning},
  year = {2025},
  url = {https://openreview.net/forum?id=5BGC2I2fxx},
}