Abstract
This paper tests whether a solver-hardness ordering transfers to LLM constraint-reasoning accuracy after near-matching clause density. Expander-Tseitin formulas become much more expensive than ladder-Tseitin formulas for the tested CDCL solvers, but verdict-accuracy gaps change sign across the three included models and pool to +1.7 percentage points (p=0.74).
TL;DR: Glucose shows a strong expander-over-ladder cost separation, and five additional CDCL solvers preserve the large-bin direction; three evaluated LLMs do not preserve that ordering in verdict accuracy. This is a scoped diagnostic and negative result, not a new solver or a certificate-solving claim.
If you're skimming
- Question: after controlling the usual density cue, does solver hardness predict LLM SAT/UNSAT verdict accuracy?
- Solver-side result: the Glucose mean-conflict separation grows from 3.3-fold to 51.4-fold across registered size bins; five additional solvers preserve the large-bin direction.
- Model-side result: the near-matched-density gaps range from -31.7 to +20.0 percentage points and pool to +1.7 points (p=0.74); none of the three models passes the registered transfer gate.
- Boundary: Glucose conflicts are a solver-specific proxy, and the model endpoint is verdict accuracy rather than certificate-verified solving.
The confound
LLM evaluations often make SAT instances harder by moving toward the random-SAT phase transition. That changes clause density and solver difficulty together. A model can therefore react to a visible density cue without tracking the structural hardness that makes one formula expensive for a solver.
The diagnostic compares proof-hard expander-Tseitin formulas with proof-easy ladder-Tseitin formulas at aligned size bins, near-matched density, and matched maximum clause width. Pigeonhole anchors and density-mismatched controls keep the interpretation narrow.
The result
The solver axis is clear. For Glucose, the registered median conflict ratio crosses 10-fold at the larger size bins and reaches 47.4-fold at 60 expander variables. A post-primary sensitivity repeats the direction across five other CDCL implementations, while keeping raw conflict scales solver-specific.
The LLM axis is not. The expander-minus-ladder verdict-accuracy gap is positive for two models and negative for one; the pooled gap is +1.7 percentage points. Correctness versus log conflicts has the wrong sign for the proposed transfer account (r=+0.15).
Surface form remains a confound
A proof-preserving relabeling changes neither satisfiability nor the relevant resolution complexity, yet it lowers accuracy in all five tested base-formula clusters for one model and changes only one cluster for another. That establishes model-specific surface sensitivity. Five clusters are too few for a uniform recognizability law, and the page does not claim one.
Observed token spend does not repair the transfer
A preregistered extension tests provider-reported completion-token spend. After accounting for formula length and censoring, observed spend does not consistently increase with the solver-cost proxy. These measurements describe output-length and test-time spend under fixed budgets; they do not estimate internal reasoning compute, allocation efficiency, or the marginal value of more tokens.
What the paper does not claim
- It does not introduce a solver, decoding method, or new solving algorithm.
- It does not equate CDCL conflicts with exact or shortest proof length.
- It does not measure certificate construction or satisfying-witness generation.
- It does not establish an architecture-wide impossibility result from three API-served autoregressive models.
- It does not claim venue acceptance. The public record is an arXiv preprint.
What is public
- Paper on arXiv with the full design, statistics, controls, and limitations.
- Public artifact v1.0.0 with synthetic instances, derived measurements, solver receipts, analysis scripts, deterministic checks, and figure code.
- Publication entry linking the paper, DOI, local PDF, artifact, and this canonical project page.
Frequently asked questions
What does "solver-hard is not model-hard" mean?
The tested SAT families separate strongly under solver-cost and resolution-hardness measures, but that ordering does not consistently predict verdict accuracy for the three included LLMs. The title names this scoped negative result, not a universal law.
Is this a new solver or solving algorithm?
No. It is a diagnostic. Established SAT families and solvers provide a controlled axis for testing what LLM verdict accuracy tracks.
Does a correct verdict mean the model constructed a certificate?
No. The endpoint is parsed SAT or UNSAT verdict accuracy. The study does not verify satisfying assignments or proof certificates.
Is this an accepted venue paper?
No venue acceptance is claimed. The public paper is an arXiv preprint.
Are the code and aggregate reproduction data public?
Yes. The public artifact includes synthetic inputs, derived measurements, solver receipts, analyses, and deterministic verification without generated model response text.
Links
BibTeX
@article{verma2026solverhard,
title={Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning},
author={Verma, Lucky},
journal={arXiv preprint arXiv:2607.17047},
year={2026}
}