CDCL SAT solvers learn clauses during search — logical consequences of the problem that prune the search space. The solver accumulates thousands of learned clauses and must periodically discard the least useful ones. The dominant heuristic for judging clause quality is Literal Block Distance (LBD): how many distinct decision levels appear in the clause. Low LBD means the clause's variables are concentrated in a few levels of the search tree — a sign of structural relevance.
Ding and colleagues (arXiv:2602.20829) show that LBD degenerates on arithmetic circuit verification — exactly the class of hard industrial problems where good clause management matters most. On these problems, LBD reduces to a simple function of clause length, losing all sensitivity to the clause's structural role in the search. The metric that works well on typical benchmarks becomes uninformative on the hardest instances.
The degeneration happens because arithmetic circuits produce search trees with specific structural properties that make LBD correlate trivially with clause size. The metric was never designed for this structure — it was validated on diverse benchmarks where its correlation with usefulness held empirically. On the hard tail of the distribution, the empirical correlation breaks.
The fix decouples two properties of learned clauses that LBD conflates: inherent lineage (where the clause came from in the proof) and dynamic usage patterns (how the clause is actually used during search). By tracking these separately, the solver achieves 5.7x speedup on arithmetic circuits while maintaining performance on standard benchmarks.
The general observation: a quality metric that works well on average can degenerate on the hardest instances of a problem class — precisely where good judgment matters most. The degeneration is not random failure but structural: the metric's assumptions match the typical case but not the extreme case. Robustness requires metrics that track distinct properties independently, not single numbers that conflate them.