# Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 21 of its 28 references that are in the map.
- First posted on arXiv 19 Jul 2026.

## Placed in

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

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

- [Are Emergent Abilities of Large Language Models a Mirage?](https://mlsanity.com/paper/2304.15004/) (2023)
- [Faith and Fate: Limits of Transformers on Compositionality](https://mlsanity.com/paper/2305.18654/) (2023)
- [The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity](https://mlsanity.com/paper/2506.06941/) (2025)
- [Does Thinking More always Help? Mirage of Test-Time Scaling in Reasoning Models](https://mlsanity.com/paper/2506.04210/) (2025)
- [Position: Stop Anthropomorphizing Intermediate Tokens as Reasoning/Thinking Traces!](https://mlsanity.com/paper/2504.09762/) (2025)
- [Learning Iterative Reasoning through Energy Diffusion](https://mlsanity.com/paper/2406.11179/) (2024)
- [THOUGHTTERMINATOR: Benchmarking, Calibrating, and Mitigating Overthinking in Reasoning Models](https://mlsanity.com/paper/2504.13367/) (2025)
- [SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas](https://mlsanity.com/paper/2505.14615/) (2025)
- [Energy-Based Transformers are Scalable Learners and Thinkers](https://mlsanity.com/paper/2507.02092/) (2025)
- [Sampling with flows, diffusion and autoregressive neural networks: A spin-glass perspective](https://mlsanity.com/paper/2308.14085/) (2023)
- [Can Transformers Reason Logically? A Study in SAT Solving](https://mlsanity.com/paper/2410.07432/) (2024)
- [When More Thinking Hurts: Overthinking in LLM Test-Time Compute Scaling](https://mlsanity.com/paper/2604.10739/) (2026)
- [Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transition](https://mlsanity.com/paper/2504.03930/) (2025)
- [Can Large Language Models Reason? A Characterization via 3-SAT](https://mlsanity.com/paper/2408.07215/) (2024)
- [Comprehension Without Competence: Architectural Limits of LLMs in Symbolic Computation and Reasoning](https://mlsanity.com/paper/2507.10624/) (2025)
- [Adaptive Test-Time Compute Allocation for Reasoning LLMs via Constrained Policy Optimization](https://mlsanity.com/paper/2604.14853/) (2026)
- [Self-Supervised Transformers as Iterative Solution Improvers for Constraint Satisfaction](https://mlsanity.com/paper/2502.15794/) (2025)
- [SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs](https://mlsanity.com/paper/2509.00930/) (2025)
- [CODA: Difficulty-Aware Compute Allocation for Adaptive Reasoning](https://mlsanity.com/paper/2603.08659/) (2026)
- [Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability](https://mlsanity.com/paper/2605.28602/) (2026)
- [Evaluating Robustness of Reasoning Models on Parameterized Logical Problems](https://mlsanity.com/paper/2602.12665/) (2026)

## Abstract (arXiv)

LLM constraint reasoners are often evaluated near the random-SAT phase transition, confounding density and solver hardness. We test instance-level transfer while near-matching clause density. At aligned size bins, with near-matched density and matched maximum clause width, we compare proof-hard expander-Tseitin and proof-easy ladder-Tseitin formulas, pigeonhole anchors, and density-mismatched controls. Theory separates their resolution hardness; a solver-specific Glucose mean-conflict proxy differs by up to 51×, and five other solvers preserve the direction. Across three included models (243 instances each; a fourth is excluded for abstention), the near-matched-density accuracy gaps range from -32 to +20 points, with a pooled gap of +1.7 points (p=0.74) and a wrong-signed correctness-versus-conflict association (r=+0.15). A proof-preserving relabeling lowers accuracy in all five clusters for one model (mean -93 points) but not another, exposing model-surface sensitivity. In a preregistered extension, provider-reported completion-token spend does not consistently increase with the proxy after accounting for formula length and censoring. At 16k, the reasoning model spends more on proof-easy matched formulas and exhausts its budget on the solver-easiest UNSAT family; the 32k C1 gap is absent. These scoped dissociations concern verdict accuracy and observed token spend, not certificate solving, exact proof length, or allocation efficiency.