KNIGHT: Exact Local Certificates and Sharp Cost Separations in Variable-Elimination Ordering

The size of a CNF formula after variable elimination depends on the interaction between resolution, tautology removal, and subsumption. We investigate exact one-step comparisons between candidate elimination pivots and develop KNIGHT, a certificate framework that establishes strict normalized clause-count dominance from surviving-background lower bounds and minimal-resolvent upper bounds. An exact slack identity characterizes the bounds, while incremental inspection and tautology-aware indexing provide complementary certification procedures. Two parameterized CNF families identify the information captured by local comparisons and the quadratic work that an incremental procedure may incur on tautological resolvent pairs. In constructed instances, indexing reduces median certificate time from 9.15 to 0.88 ms, with higher traced allocation; on 1,000 seeded random comparisons, the methods certify 10 of 406 favorable cases, increasing to 12 when one successor is evaluated exactly. We further establish sharp cumulative elimination costs for an infinite connected CNF family constructed from a seven-clause gadget. For k connected copies, the unrestricted optimum is (11k² + 19k − 10)/2, whereas the optimum constrained to begin with the locally smallest pivot is (11k² + 25k − 16)/2 for k ≥ 2. The resulting additive separation is exactly 3k − 3. A shared-positive-variable decomposition yields a symmetry-reduced exact dynamic program. Together, these results connect verifiable local clause-count comparisons with exact global elimination-order analysis.