SAT solvers learn clauses as they search — each dead end produces a clause that prevents revisiting the same failure. But clauses accumulate, and memory fills. The solver must periodically delete low-quality clauses. The standard quality metric is Literal Block Distance (LBD): how many distinct decision levels a clause spans. Low LBD means the clause captures a tight, reusable relationship. High LBD means it's sprawling and unlikely to help again.
Luo and colleagues (arXiv:2602.20829) show that LBD fails on exactly the problems where SAT solving matters most: complex arithmetic circuit verification. On multiplier verification benchmarks, LBD degenerates into a proxy for clause length because the structure of arithmetic circuits — deep, wide, with many interacting decision levels — makes almost every learned clause span many levels. When every clause has high LBD, the quality metric carries no information.
The fix: decouple the two things LBD conflates. A clause has an inherent quality based on its logical lineage (what conflict produced it, how many resolution steps led to it) and a dynamic quality based on its usage pattern (how often it participates in unit propagation, how recently it contributed to a conflict). LBD mixes these into one number. Separating them allows the solver to keep clauses that are structurally simple and operationally active, even when LBD can't distinguish them from useless ones.
The speedup: up to 5.74x on arithmetic circuits, with no degradation on general benchmarks.
The general observation: when a composite quality metric fails on hard instances, the failure often reveals that the metric conflates independent dimensions. Decomposing the metric into its constituent dimensions recovers discriminative power precisely where the composite metric lost it. The hard instances are hard because they compress the metric's dynamic range — and decompression is the fix.