claimroutineinferred_dep
Arbitrary-density time and space accounting
Statement (paper)
The procedure runs in bit operations and uses bits of space: constructing the initial checks and enumerating candidates costs bit operations apart from the evaluations, there are at most evaluations per leaf, and these costs together with the number of leaves are absorbed in the claimed time bound, while the exact leaf counts, being counts of disjoint solution sets, add in an -bit accumulator under depth-first traversal.
In plain English
The counting procedure for a -CNF with arbitrary clause density runs in bit operations and uses bits of space.
Why it's here
This claim totals the cost of the whole procedure. Each leaf of the sparsification tree needs only overhead plus at most evaluations, and this is absorbed in the time bound together with the leaf count from the sparsification claim. Space stays polynomial because leaf counts are counts of disjoint solution sets, so a depth-first traversal can add them in an -bit accumulator. This finishes the proof of the main theorem for arbitrary density.
Classified routine:
Direct bookkeeping combining the sparsification tree size (claim-thm-main-3) with the per-leaf evaluation bound (claim-thm-main-4); polynomial space follows from the standard depth-first traversal of a sparsification tree whose leaves have disjoint solution sets, as in Calabro–Impagliazzo–Paturi sparsification.