# Can Transformers Reason Logically? A Study in SAT Solving

arXiv: https://arxiv.org/abs/2410.07432 · HTML: https://mlsanity.com/paper/2410.07432/

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 27 of its 40 references that are in the map.
- First posted on arXiv 9 Oct 2024.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 27 of 27)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Towards Revealing the Mystery behind Chain of Thought: A Theoretical Perspective](https://mlsanity.com/paper/2305.15408/) (2023)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Transformers Learn Shortcuts to Automata](https://mlsanity.com/paper/2210.10749/) (2022)
- [Chain of Thought Empowers Transformers to Solve Inherently Serial Problems](https://mlsanity.com/paper/2402.12875/) (2024)
- [Looped Transformers as Programmable Computers](https://mlsanity.com/paper/2301.13196/) (2023)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [The Parallelism Tradeoff: Limitations of Log-Precision Transformers](https://mlsanity.com/paper/2207.00729/) (2022)
- [Thinking Like Transformers](https://mlsanity.com/paper/2106.06981/) (2021)
- [Saturated Transformers are Constant-Depth Threshold Circuits](https://mlsanity.com/paper/2106.16213/) (2021)
- [On the Turing Completeness of Modern Neural Network Architectures](https://mlsanity.com/paper/1901.03429/) (2019)
- [Self-Attention Networks Can Process Bounded Hierarchical Languages](https://mlsanity.com/paper/2105.11115/) (2021)
- [Tracr: Compiled Transformers as a Laboratory for Interpretability](https://mlsanity.com/paper/2301.05062/) (2023)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [On the Paradox of Learning to Reason from Data](https://mlsanity.com/paper/2205.11502/) (2022)
- [Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples](https://mlsanity.com/paper/2305.15269/) (2023)
- [NPHardEval: Dynamic Benchmark on Reasoning Ability of Large Language Models via Complexity Classes](https://mlsanity.com/paper/2312.14890/) (2023)
- [Code Execution with Pre-trained Language Models](https://mlsanity.com/paper/2305.05383/) (2023)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [Can Large Language Models Reason? A Characterization via 3-SAT](https://mlsanity.com/paper/2408.07215/) (2024)
- [Can Language Models Pretend Solvers? Logic Code Simulation with LLMs](https://mlsanity.com/paper/2403.16097/) (2024)
- [MatSat: a matrix-based differentiable SAT solver](https://mlsanity.com/paper/2108.06481/) (2021)

## Built on by (most cited first, 16 of 16)

- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [Beyond Semantics: The Unreasonable Effectiveness of Reasonless Intermediate Tokens](https://mlsanity.com/paper/2505.13775/) (2025)
- [SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas](https://mlsanity.com/paper/2505.14615/) (2025)
- [Performative Thinking? The Brittle Correlation Between CoT Length and Problem Complexity](https://mlsanity.com/paper/2509.07339/) (2025)
- [Evaluating Implicit Biases in LLM Reasoning through Logic Grid Puzzles](https://mlsanity.com/paper/2511.06160/) (2025)
- [Learning-augmented smooth integer programs with PAC-learnable oracles](https://mlsanity.com/paper/2602.02505/) (2026)
- [Evaluating Robustness of Reasoning Models on Parameterized Logical Problems](https://mlsanity.com/paper/2602.12665/) (2026)
- [Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Traces](https://mlsanity.com/paper/2602.14404/) (2026)
- [Self-Improvement for Fast, High-Quality Plan Generation](https://mlsanity.com/paper/2605.03625/) (2026)
- [Boolean Satisfiability via Imitation Learning](https://mlsanity.com/paper/2509.25411/) (2025)
- [Infeasibility Aware Large Language Models for Combinatorial Optimization](https://mlsanity.com/paper/2604.01455/) (2026)
- [Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysis](https://mlsanity.com/paper/2604.20523/) (2026)
- [Learning How to Cube](https://mlsanity.com/paper/2605.16632/) (2026)
- [Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning](https://mlsanity.com/paper/2607.17047/) (2026)
- [Learning Symbolic Constraint Representations from Examples: A Neuro-Symbolic Approach](https://mlsanity.com/paper/2609.12267/) (2026)
- [Conditional Transfer from Controlled Pretraining Mixtures to Code](https://mlsanity.com/paper/2610.11548/) (2026)

## Abstract (arXiv)

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