propositionroutineinferred_depunresolved_ref

Running time of the interpolation counting algorithm

Proposition·prop:interpolation-bound·§6.4 Returning to a general formula

Statement (paper)

For each fixed k⩾2k\ge2, the interpolation algorithm counts the satisfying assignments of a kk-CNF on n⩾20n\ge20 declared variables with mm clauses in (n+m)Ok(1)2Ok(ρ(n))(n+m)^{O_k(1)}2^{O_k(\rho(n))} bit operations and (n+m)Ok(1)(n+m)^{O_k(1)} bits of space.

In plain English

For fixed k⩾2k\ge2, the interpolation algorithm counts satisfying assignments of a kk-CNF with n⩾20n\ge20 declared variables and mm clauses using (n+m)Ok(1)2Ok(ρ(n))(n+m)^{O_k(1)}2^{O_k(\rho(n))} bit operations and (n+m)Ok(1)(n+m)^{O_k(1)} bits of space.

Why it's here

This is the cost accounting for the general-formula algorithm. Sparsification (Lemma 6.3) reduces the input to bounded-occurrence leaves, the greedy-hash construction (Lemma 6.2) turns each leaf count into a bounded number of common-zero counts of sparse low-degree systems, and the sparse-polynomial counting theorem answers each count. Summing these costs gives the stated time and space bounds.
Classified routine:
Cost accounting that combines sparsification (Lemma 6.3), the greedy-hash reduction (Lemma 6.2) and the sparse-polynomial counting theorem. Its bound is the sum of their costs, obtained by standard bookkeeping.

Uses

lemSparsification into bounded-occurrence k-CNF leavesthmCounting zeros of sparse polynomials fasterlemGreedy appended rows give exact count

Used by

Nothing in the paper

Sources

PaperOpen
Section
§6.4 Returning to a general formula
Page
—
Label
prop:interpolation-bound
Line
main_full_version.tex:3570
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: Prop 6.4 counts each leaf "by the sparse-formula algorithm of Section 6.3" (line 3600). That algorithm is built on Lemma greedy-hashes ("The final count is #F by the greedy lemma", line 3526). The proof also says "initial checks, and additional rows are computed by the deterministic procedures above".
  • warn
    unresolved_ref
    Counting each leaf relies on the unlabeled sparse-formula argument of Section 6.3 (eq:sparse-formula-cost) rather than a statement.