这篇论文用严格实验告诉你，LLM在约束推理上的表现和求解器难度不是一码事。他们控制密度、比较两类公式，发现准确率差距和求解器冲突量几乎不相关，甚至反着走。
研究团队在子句密度近乎匹配的条件下，比较了证明难的expander-Tseitin公式与证明易的ladder-Tseitin公式，以及密度不匹配的控制组。求解器Glucose的平均冲突代理差异高达51倍，其他五个求解器也保持方向一致。三个模型各243个实例的准确率差距从-32到+20个百分点，合并差距为+1.7个百分点（p=0.74），且正确率与冲突代理呈错误正向关联（r=+0.15）。证明保留重标定使一个模型准确率平均下降93点，但对另一个模型影响不大。16k token实验中，推理模型在证明易匹配公式上的token消耗反而更多，而32k C1差距消失。
Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning
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\times$, 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.