claimroutineinferred_dep

Arbitrary-density time and space accounting

Claim·§D.3 Arbitrary clause density·inside thmSubexponential deterministic k-CNF model counting

Statement (paper)

The procedure runs in (n+m)Ok(1)2Ok(nlog⁡log⁡n/log⁡n)(n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})} bit operations and uses (n+m)Ok(1)(n+m)^{O_k(1)} bits of space: constructing the initial checks and enumerating candidates costs 2λOk(1)2^{\lambda^{O_k(1)}} bit operations apart from the evaluations, there are at most 3n(2mG)P+1=2λOk(1)3n(2m_G)^P+1=2^{\lambda^{O_k(1)}} 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 (n+1)(n+1)-bit accumulator under depth-first traversal.

In plain English

The counting procedure for a kk-CNF with arbitrary clause density runs in (n+m)Ok(1)2Ok(nlog⁡log⁡n/log⁡n)(n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})} bit operations and uses (n+m)Ok(1)(n+m)^{O_k(1)} bits of space.

Why it's here

This claim totals the cost of the whole procedure. Each leaf of the sparsification tree needs only 2λOk(1)2^{\lambda^{O_k(1)}} overhead plus at most 2λOk(1)2^{\lambda^{O_k(1)}} 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 (n+1)(n+1)-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.

Uses

claimSparsify with sigma about 1/sqrt(log n)claimLeaf counts via parity rows and queries

Used by

Nothing in the paper

Sources

PaperOpen
Section
§D.3 Arbitrary clause density
Page
—
Label
—
Line
quantitative-reduction.tex:347
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Arbitrary-density time and space accounting" rests on claim-thm-main-3
  • info
    inferred_dep
    outline: "Arbitrary-density time and space accounting" rests on claim-thm-main-4