mlsanityData to 14 Oct 2026

Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability

arXiv 2605.28602 ↗First posted 27 May 2026cs.AI cs.CL cs.LOcited by 2

On the map: LLM reasoning → Reasoning benchmarks and evaluation

Abstract (arXiv)

Large language models (LLMs) are increasingly used for tasks that implicitly reduce to Boolean satisfiability (SAT), yet their reasoning ability on SAT remains unclear. We present a systematic study of LLMs on 2-SAT and 3-SAT, together with two canonical reductions, Vertex Cover and discrete 3D packing, to probe representation-invariant reasoning. We first evaluate models using conventional metrics, including accuracy, precision, recall, and F1, as well as the SAT phase-transition setting. We find that these metrics can be misleading: many models obtain high scores by over-predicting satisfiable formulas, fail to reproduce the classical easy-hard-easy signature around the 3-SAT threshold, and degrade sharply as the number of variables grows. To address this problem, we introduce a paired-formula protocol based on minimally different satisfiable and unsatisfiable instances, together with Accurate Differentiation Rate (ADR), which requires both members of each pair to be classified correctly. ADR separates reasoning-oriented models from heuristic ones and correlates with witness validity. Beyond CNF, we test cross-representation consistency by converting CNF to Vertex Cover and 3-SAT to discrete 3D packing. Model decisions on CNF and on the corresponding graph or packing instances agree for most models on more than 80 percent of instances, suggesting stable decision rules across representations. Overall, our results show that SAT is a conservative probe for LLM reasoning, and that paired evaluation with ADR provides a more faithful and representation-robust assessment than conventional metrics.

Key facts. Cited by 2 papers in the map (data through 14 Oct 2026). Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning. Builds on 4 of its 53 references that are in the map. First posted on arXiv 27 May 2026.

Builds on

4 of 53 references.

References · 4

  1. 2020Evaluation: from precision, recall and F-measure to ROC, informedness, markedness and correlationcited by 425
  2. 2024Vulnerability Detection with Code Language Models: How Far Are We?cited by 139
  3. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  4. 2025A Contemporary Survey of Large Language Model Assisted Program Analysiscited by 11

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 2.

2 papers.

  1. 2026Amplitude-Only FFN Intervention for Tool-Structured LLM Inference: Method, Gated Evaluation Protocol, and Cross-Model Empirical Resultscited by 0
  2. 2026Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoningcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
  2. 2024Can Large Language Models Reason? A Characterization via 3-SAT
  3. 2026Evaluating Robustness of Reasoning Models on Parameterized Logical Problems
  4. 2025SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs
  5. 2025FINEREASON: Evaluating and Improving LLMs' Deliberate Reasoning through Reflective Puzzle Solving
  6. 2025Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transition
  7. 2026The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics
  8. 2025Putnam-AXIOM: A Functional and Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs