SATBench - Benchmarking LLMs’ Logical Reasoning via Automated Puzzle Generation from SAT Formulas

Sep 14, 2026

Uploaded by Violet

SATBench introduces a benchmark for evaluating large language models’ logical reasoning by automatically generating puzzle instances from Boolean satisfiability (SAT) formulas. Each SAT instance is translated into a natural-language puzzle using LLMs, with difficulty adjusted by varying the number of clauses. All 2100 puzzles are validated through LLM-based and solver-based consistency checks, plus human validation on a subset. Results show limited accuracy on hard UNSAT problems and reveal systematic failures such as satisfiability bias, context inconsistency, and condition omission.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages18

Reading Time45 min

AccessFree to download

Abstract

Introduction

Related Work

SATBench Methodology

Generation Pipeline

Consistency Validation

Evaluation Pipeline

Results

SATBench: Benchmarking LLMs’ Logical Reasoning via Automated Puzzle Generation from SAT Formulas Anjiang Wei1 *† Tarun Suresh3 Sanmi Koyejo 1 Yuheng Wu1 * Huanmi Tan4 Ke Wang5 Yingjia Wan2 Zhanke Zhou 1 Alex Aiken 1 1 Stanford University 2UCLA 3UIUC 4 CMU 5Nanjing University Abstract 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 searchbased 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:](https:)//[github.com/Anjiang-Wei/SATBench](github.com/Anjiang-Wei/SATBench) 1 Introduction Logical reasoning is a fundamental component of human intelligence and continues to be a significant challenge in the field of artificial intelligence. The growing interest in the reasoning capabilities of large language models (LLMs) highlights the pressing need for robust benchmarks and evaluation methods (Luo et al., 2023) . While many datasets have been proposed to evaluate logical reasoning capabilities of LLMs, earlier datasets do not exclusively evaluate logical reasoning in isolation, e.g., LogiQA (Liu et al., 2020), and *Equal contribution. †Correspondence to: [anjiang@cs.stanford.edu](anjiang@cs.stanford.edu) ReClor (Yu et al., 2020), which combine logical reasoning with commonsense reasoning. Recently, new datasets have been introduced to assess logical reasoning in isolation, such as FOLIO (Han et al., 2024a) and P-FOLIO (Han et al., 2024b) . These datasets are manually curated by researchers and focus on logical problems based on inference rules, which involve deriving conclusions from a set of premises. In this work, we introduce SATBench, a benchmark designed to create logical puzzles from Boolean satisfiability (SAT) problems (Cook, 1971 ; Pan et al., 2024) with LLMs. Unlike benchmarks based on inference rules, SAT problems are characterized as search-based logical reasoning tasks, where the objective is to determine a truth assignment that fulfills a specified set of logical constraints (Madusanka et al., 2024) . This approach to logical reasoning emphasizes a search process akinto backtracking used in SAT solvers. Unlike other search-based benchmarks such as ZebraLogic (Linet al., 2025), which presuppose the existence of a valid solution, SAT problems can result in either a satisfiable solution (SAT) or no solution (UNSAT) . As shown in Figure 1, starting from a SAT formula in Conjunctive Normal Form (CNF), such as (A ∨ ¬B) ∧ (¬C ∨ ¬D), our framework uses LLMs to generate a story context and define a mapping between formula variables and entities in the story. Each clause is then translated into a natural language condition based on this mapping. By sampling CNF formulas with varying numbers of clauses, we can control puzzle difficulty. To ensure the quality of resulting logical puzzles, we reverse the generation process: LLMs translate the natural language conditions back into logical formulas, whic

FAQs

What is SATBench and what does it benchmark?

SATBench is a benchmark that evaluates the logical reasoning capabilities of large language models using puzzles generated from Boolean satisfiability (SAT) problems.

How are SATBench puzzles generated and how is difficulty controlled?

Each puzzle is generated from a sampled SAT formula and translated into a story context with natural-language conditions using LLMs. Difficulty is adjusted by varying the number of clauses in the sampled CNF formulas.

How are puzzles validated and how is model reasoning evaluated?

Puzzle quality is verified with both LLM-assisted and solver-based consistency checks, and reasoning traces are assessed using an LLM-as-a-judge strategy in the evaluation pipeline.

Sep 14, 2026

Uploaded by Violet

SATBench - Benchmarking LLMs’ Logical Reasoning via Automated Puzzle Generation from SAT Formulas_Page 1

Open in WPS to view all 18 pages