Can Transformers Reason Logically? A Study in SAT Solving
On the map: LLM reasoning → Reasoning benchmarks and evaluation
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
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.
Builds on
27 of 40 references.
Closest ancestors · 7
Same direction, newest first
- 2024Can Large Language Models Reason? A Characterization via 3-SAT13 Aug
- 2023NPHardEval: Dynamic Benchmark on Reasoning Ability of Large Language Models via Complexity Classes22 Dec
- 2023Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples24 May
- 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning20 May
- 2023LLaMA: Open and Efficient Foundation Language Models27 Feb
- 2022Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought3 Oct
- 2022On the Paradox of Learning to Reason from Data23 May
Other references · 20
- 2017Attention Is All You Needcited by 60,361
- 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
- 2020ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Languagecited by 324
- 2023Towards Revealing the Mystery behind Chain of Thought: A Theoretical Perspectivecited by 294
- 2020Transformers as Soft Reasoners over Languagecited by 270
- 2022Transformers Learn Shortcuts to Automatacited by 268
- 2024Chain of Thought Empowers Transformers to Solve Inherently Serial Problemscited by 260
- 2023Looped Transformers as Programmable Computerscited by 237
- 2018Learning a SAT Solver from Single-Bit Supervisioncited by 200
- 2022The Parallelism Tradeoff: Limitations of Log-Precision Transformerscited by 193
- 2021Thinking Like Transformerscited by 184
- 2021Saturated Transformers are Constant-Depth Threshold Circuitscited by 139
8 more
- 2019On the Turing Completeness of Modern Neural Network Architecturescited by 129
- 2021Self-Attention Networks Can Process Bounded Hierarchical Languagescited by 105
- 2023Tracr: Compiled Transformers as a Laboratory for Interpretabilitycited by 104
- 2024Faithful Logical Reasoning via Symbolic Chain-of-Thoughtcited by 100
- 2023Code Execution with Pre-trained Language Modelscited by 34
- 2022SATformer: Transformer-Based UNSAT Core Learningcited by 14
- 2024Can Language Models Pretend Solvers? Logic Code Simulation with LLMscited by 4
- 2021MatSat: a matrix-based differentiable SAT solvercited by 2
Built on by
Citing papers per year: 2025: 6; 2026: 10.
16 papers.
Sort:
By area:
- 2025ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoningcited by 201
- 2025Beyond Semantics: The Unreasonable Effectiveness of Reasonless Intermediate Tokenscited by 41
- 2025SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulascited by 33
- 2025Performative Thinking? The Brittle Correlation Between CoT Length and Problem Complexitycited by 9
- 2025Evaluating Implicit Biases in LLM Reasoning through Logic Grid Puzzlescited by 1
- 2026Learning-augmented smooth integer programs with PAC-learnable oraclescited by 1
- 2026Evaluating Robustness of Reasoning Models on Parameterized Logical Problemscited by 1
- 2026Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Tracescited by 1
- 2026Self-Improvement for Fast, High-Quality Plan Generationcited by 1
- 2025Boolean Satisfiability via Imitation Learningcited by 0
- 2026Infeasibility Aware Large Language Models for Combinatorial Optimizationcited by 0
- 2026Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysiscited by 0
4 more
- 2026Learning How to Cubecited by 0
- 2026Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoningcited by 0
- 2026Learning Symbolic Constraint Representations from Examples: A Neuro-Symbolic Approachcited by 0
- 2026Conditional Transfer from Controlled Pretraining Mixtures to Codecited by 0
- 2026Conditional Transfer from Controlled Pretraining Mixtures to Code8 Oct 2026
- 2026Learning Symbolic Constraint Representations from Examples: A Neuro-Symbolic Approach10 Sep 2026
- 2026Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning19 Jul 2026
- 2026Learning How to Cube15 May 2026
- 2026Self-Improvement for Fast, High-Quality Plan Generation5 May 2026
- 2026Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysis22 Apr 2026
- 2026Infeasibility Aware Large Language Models for Combinatorial Optimization1 Apr 2026
- 2026Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Traces16 Feb 2026
- 2026Evaluating Robustness of Reasoning Models on Parameterized Logical Problems13 Feb 2026
- 2026Learning-augmented smooth integer programs with PAC-learnable oracles22 Jan 2026
- 2025Evaluating Implicit Biases in LLM Reasoning through Logic Grid Puzzles8 Nov 2025
- 2025Boolean Satisfiability via Imitation Learning29 Sep 2025
4 more
- 2025Performative Thinking? The Brittle Correlation Between CoT Length and Problem Complexity9 Sep 2025
- 2025SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas20 May 2025
- 2025Beyond Semantics: The Unreasonable Effectiveness of Reasonless Intermediate Tokens19 May 2025
- 2025ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning3 Feb 2025
- 2025ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoningcited by 201
- 2025Beyond Semantics: The Unreasonable Effectiveness of Reasonless Intermediate Tokenscited by 41
- 2025SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulascited by 33
- 2025Performative Thinking? The Brittle Correlation Between CoT Length and Problem Complexitycited by 9
- 2025Evaluating Implicit Biases in LLM Reasoning through Logic Grid Puzzlescited by 1
- 2026Evaluating Robustness of Reasoning Models on Parameterized Logical Problemscited by 1
- 2026Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Tracescited by 1
- 2026Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoningcited by 0
- 2026Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning19 Jul 2026
- 2026Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Traces16 Feb 2026
- 2026Evaluating Robustness of Reasoning Models on Parameterized Logical Problems13 Feb 2026
- 2025Evaluating Implicit Biases in LLM Reasoning through Logic Grid Puzzles8 Nov 2025
- 2025Performative Thinking? The Brittle Correlation Between CoT Length and Problem Complexity9 Sep 2025
- 2025SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas20 May 2025
- 2025Beyond Semantics: The Unreasonable Effectiveness of Reasonless Intermediate Tokens19 May 2025
- 2025ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning3 Feb 2025
- 2026Learning How to Cubecited by 0
- 2026Learning How to Cube15 May 2026
- 2025Boolean Satisfiability via Imitation Learningcited by 0
- 2025Boolean Satisfiability via Imitation Learning29 Sep 2025
- 2026Learning-augmented smooth integer programs with PAC-learnable oraclescited by 1
- 2026Self-Improvement for Fast, High-Quality Plan Generationcited by 1
- 2026Infeasibility Aware Large Language Models for Combinatorial Optimizationcited by 0
- 2026Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysiscited by 0
- 2026Learning Symbolic Constraint Representations from Examples: A Neuro-Symbolic Approachcited by 0
- 2026Conditional Transfer from Controlled Pretraining Mixtures to Codecited by 0
- 2026Conditional Transfer from Controlled Pretraining Mixtures to Code8 Oct 2026
- 2026Learning Symbolic Constraint Representations from Examples: A Neuro-Symbolic Approach10 Sep 2026
- 2026Self-Improvement for Fast, High-Quality Plan Generation5 May 2026
- 2026Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysis22 Apr 2026
- 2026Infeasibility Aware Large Language Models for Combinatorial Optimization1 Apr 2026
- 2026Learning-augmented smooth integer programs with PAC-learnable oracles22 Jan 2026
Similar, not cited
Close in wording, no citation either way
- 2024Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
- 2026Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability
- 2024Reasoning in Transformers -- Mitigating Spurious Correlations and Reasoning Shortcuts
- 2023Assessing Logical Reasoning Capabilities of Encoder-Only Transformer Models
- 2025Natural Language Satisfiability: Exploring the Problem Distribution and Evaluating Transformer-based Language Models
- 2026To See the Unseen: on the Generalization Ability of Transformers in Symbolic Reasoning
- 2026SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
- 2023The Expressive Power of Transformers with Chain of Thought