@inproceedings{wei-etal-2025-satbench,
    title = "{SATB}ench: Benchmarking {LLM}s' Logical Reasoning via Automated Puzzle Generation from {SAT} Formulas",
    author = "Wei, Anjiang  and
      Wu, Yuheng  and
      Wan, Yingjia  and
      Suresh, Tarun  and
      Tan, Huanmi  and
      Zhou, Zhanke  and
      Koyejo, Sanmi  and
      Wang, Ke  and
      Aiken, Alex",
    editor = "Christodoulopoulos, Christos  and
      Chakraborty, Tanmoy  and
      Rose, Carolyn  and
      Peng, Violet",
    booktitle = "Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing",
    month = nov,
    year = "2025",
    address = "Suzhou, China",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-emnlp/2025.emnlp-main.1716/",
    pages = "33820--33837",
    ISBN = "979-8-89176-332-6",
    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 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"
}