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

Summary

Fully automated pipeline: sample CNF, LLM-write story+variable mapping, translate clauses to conditions, then LLM+solver bidirectional-entailment checks plus human sample. 2100 puzzles (easy 4-19 / medium 20-30 / hard 31-50 clauses). Unlike FOLIO/P-FOLIO (inference rules) or ZebraLogic (assumes a solution exists), instances can be SAT or UNSAT. o4-mini 89.3% overall but only 65.0% on hard UNSAT (near 50% random). Failure modes: satisfiability bias, context inconsistency, condition omission. GitHub LICENSE field empty; README/HF card say Apache-2.0. EMNLP 2025 (pages 33820-33837).

Keywords

satbench · sat · logical-reasoning · unsat · emnlp · stanford

Topics

logical reasoning, SAT, puzzle generation, LLM evaluation

Research notes

• Primary: GitHub README + arxiv abs 2505.14615 + HF card. Paper/repo/dataset not previously in papers_local or datasets_local. Discord posted the GitHub repo.