# SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas

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

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 20 of its 41 references that are in the map.
- First posted on arXiv 20 May 2025.

## Placed in

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

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models](https://mlsanity.com/paper/2206.04615/) (2022)
- [A large annotated corpus for learning natural language inference](https://mlsanity.com/paper/1508.05326/) (2015)
- [CommonsenseQA: A Question Answering Challenge Targeting Commonsense Knowledge](https://mlsanity.com/paper/1811.00937/) (2018)
- [DeepSeek-V3 Technical Report](https://mlsanity.com/paper/2412.19437/) (2024)
- [Making Large Language Models Better Reasoners with Step-Aware Verifier](https://mlsanity.com/paper/2206.02336/) (2022)
- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [Puzzle Solving using Reasoning of Large Language Models: A Survey](https://mlsanity.com/paper/2402.11291/) (2024)
- [Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models](https://mlsanity.com/paper/2310.00836/) (2023)
- [AutoLogi: Automated Generation of Logic Puzzles for Evaluating Reasoning Abilities of Large Language Models](https://mlsanity.com/paper/2502.16906/) (2025)
- [Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning](https://mlsanity.com/paper/2410.08047/) (2024)
- [LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models](https://mlsanity.com/paper/2401.00757/) (2024)
- [Step-by-Step Reasoning to Solve Grid Puzzles: Where do LLMs Falter?](https://mlsanity.com/paper/2407.14790/) (2024)
- [Can Transformers Reason Logically? A Study in SAT Solving](https://mlsanity.com/paper/2410.07432/) (2024)
- [LogicPro: Improving Complex Logical Reasoning via Program-Guided Learning](https://mlsanity.com/paper/2409.12929/) (2024)
- [FINEREASON: Evaluating and Improving LLMs' Deliberate Reasoning through Reflective Puzzle Solving](https://mlsanity.com/paper/2502.20238/) (2025)
- [Scaling Synthetic Logical Reasoning Datasets with Context-Sensitive Declarative Grammars](https://mlsanity.com/paper/2406.11035/) (2024)

## Built on by (most cited first, 30 of 33)

- [Astra: A Multi-Agent System for GPU Kernel Performance Optimization](https://mlsanity.com/paper/2509.07506/) (2025)
- [Recursive Models for Long-Horizon Reasoning](https://mlsanity.com/paper/2603.02112/) (2026)
- [Project Aletheia: Verifier-Guided Distillation of Backtracking for Small Language Models](https://mlsanity.com/paper/2601.14290/) (2026)
- [Pencil Puzzle Bench: A Benchmark for Multi-Step Verifiable Reasoning](https://mlsanity.com/paper/2603.02119/) (2026)
- [Vesta: A Generalist Embodied Reasoning Model](https://mlsanity.com/paper/2606.20905/) (2026)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [TopoBench: Benchmarking LLMs on Hard Topological Reasoning](https://mlsanity.com/paper/2603.12133/) (2026)
- [Throttling Web Agents Using Reasoning Gates](https://mlsanity.com/paper/2509.01619/) (2025)
- [Fine-Tuned Large Language Models for Logical Translation: Reducing Hallucinations with Lang2Logic](https://mlsanity.com/paper/2512.02987/) (2025)
- [CausalT5k: Diagnosing Refusal and Failure Modes in Trustworthy Causal Reasoning Across Causal Rungs](https://mlsanity.com/paper/2602.08939/) (2026)
- [VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline](https://mlsanity.com/paper/2604.10341/) (2026)
- [Reasoning Models Don't Just Think Longer, They Move Differently](https://mlsanity.com/paper/2605.15454/) (2026)
- [VeriLocc: End-to-End Cross-Architecture Register Allocation via LLM](https://mlsanity.com/paper/2506.17506/) (2025)
- [RegexPSPACE: A Benchmark for Evaluating LLM Reasoning on PSPACE-complete Regex Problems](https://mlsanity.com/paper/2510.09227/) (2025)
- [Evaluating Robustness of Reasoning Models on Parameterized Logical Problems](https://mlsanity.com/paper/2602.12665/) (2026)
- [The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics](https://mlsanity.com/paper/2608.03291/) (2026)
- [Harbor Adapters and Harbor-Index: Infrastructure and a Curated Meta-Dataset for Large-Scale Agentic Evaluation](https://mlsanity.com/paper/2609.04298/) (2026)
- [PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data](https://mlsanity.com/paper/2508.15180/) (2025)
- [An approach for systematic decomposition of complex llm tasks](https://mlsanity.com/paper/2510.07772/) (2025)
- [GenPlanner: From Noise to Plans -- Emergent Reasoning in Flow Matching and Diffusion Models](https://mlsanity.com/paper/2602.18812/) (2026)
- [Infeasibility Aware Large Language Models for Combinatorial Optimization](https://mlsanity.com/paper/2604.01455/) (2026)
- [How Far Are We? Systematic Evaluation of LLMs vs. Human Experts in Mathematical Contest in Modeling](https://mlsanity.com/paper/2604.04791/) (2026)
- [Quantifying Cross-Query Contradictions in Multi-Query LLM Reasoning](https://mlsanity.com/paper/2604.14525/) (2026)
- [XLGoBench: Detecting cross-lingual skill gaps with algorithmic tasks](https://mlsanity.com/paper/2605.30788/) (2026)
- [Step-by-Step Optimization-like Reasoning in LLMs over Expanding Search Spaces](https://mlsanity.com/paper/2606.05464/) (2026)
- [SciR: A Controllable Benchmark for Scientific Reasoning in LLMs](https://mlsanity.com/paper/2606.13020/) (2026)
- [Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning](https://mlsanity.com/paper/2607.17047/) (2026)
- [NOLLI: A Difficulty-Calibrated Puzzle Benchmark for Diagnosing the English-Korean Performance Gap](https://mlsanity.com/paper/2608.04397/) (2026)
- [The Geometry of Logic: Stratification Induces Semantic Structure and Robust Reasoning](https://mlsanity.com/paper/2609.32927/) (2026)
- [Blackboard Intelligence Can Surpass Autoregressive on Globally Constrained Problems](https://mlsanity.com/paper/2609.38806/) (2026)

## Abstract (arXiv)

We introduce SATBench, a benchmark for evaluating the logical reasoning capabilities of large language models (LLMs) through logical puzzles derived from Boolean satisfiability (SAT) problems. Unlike prior work that focuses on inference rule-based reasoning, which often involves deducing conclusions from a set of premises, our approach leverages the search-based nature of SAT problems, where the objective is to find a solution that fulfills a specified set of logical constraints. Each instance in SATBench is generated from a SAT formula, then translated into a puzzle using LLMs. The generation process is fully automated and allows for adjustable difficulty by varying the number of clauses. All 2100 puzzles are validated through both LLM-based and solver-based consistency checks, with human validation on a subset. Experimental results show that even the strongest model, o4-mini, achieves only 65.0% accuracy on hard UNSAT problems, close to the random baseline of 50%. Our error analysis reveals systematic failures such as satisfiability bias, context inconsistency, and condition omission, highlighting limitations of current LLMs in search-based logical reasoning. Our code and data are publicly available at https://github.com/Anjiang-Wei/SATBench