Model-Dependent Transfer of Solver-Cost Orderings in SAT Evaluation

SAT solvers provide exact labels and measurable search costs for generated reasoning tasks. Whether their cost ordering predicts language-model verdict accuracy is an empirical question. We study 120 unsatisfiable parity formulas from two graph families at three nearby-size pairs. Six clause-learning SAT solvers rank the random-regular family above ladders at all three pairs, with median conflict ratios from 2.9 to 5.6. Llama 3.3 and Mistral 3 are more accurate on the solver-cheaper ladders by 20.0 and 16.7 percentage points; Llama 4 is less accurate by 31.7 points (95% stratified instance-bootstrap interval: -46.7 to -16.7), with the reverse ordering appearing at all three tested sizes. SAT and UNSAT controls reveal strong answer-label asymmetry, and a request-error analysis separates infrastructure failures from absent model verdicts. The results support model-specific validation of a solver-cost ordering before it is used to order evaluation tasks. Structural differences, a small model panel and verdict-only scoring limit the interpretation to the tested diagnostic rather than a causal effect of proof hardness.