claimroutineinferred_dep

Per-node and parameter-search cost

Claim·§A.3 The size of the tree·inside lemSparsification into bounded-occurrence k-CNF leaves

Statement (paper)

Each node of the tree can be processed, that is, the counts deg⁡c(H)\deg_c(H) computed, a branch chosen, and its children normalized, using poly⁡k(n,log⁡M)=poly⁡k(n,log⁡(2/σ))\poly_k(n,\log M)=\poly_k(n,\log(2/\sigma)) bit operations and bits of working space, since log⁡M=Ok(log⁡(2/σ))\log M=O_k(\log(2/\sigma)). The parameter search examines Ok(Lσ)O_k(L_\sigma) powers of two with integer operands of Ok(Lσ)O_k(L_\sigma) bits, so constructing the numerical parameters uses poly⁡k(Lσ)\poly_k(L_\sigma) bit operations and bits of working space.

In plain English

Each tree node is processed (computing the counts deg⁡c(H)\deg_c(H), choosing a branch, normalizing the children) in poly⁡k(n,log⁡(2/σ))\poly_k(n,\log(2/\sigma)) bit operations and space, and the numerical parameters are found in poly⁡k(Lσ)\poly_k(L_\sigma) bit operations and space.

Why it's here

This gives the running-time clauses of the lemma. Per-node cost depends only on log⁡M\log M, which is Ok(log⁡(2/σ))O_k(\log(2/\sigma)) by the choice of MM in the previous claim. The parameter search only tries Ok(Lσ)O_k(L_\sigma) powers of two with Ok(Lσ)O_k(L_\sigma)-bit operands, so it costs poly⁡k(Lσ)\poly_k(L_\sigma).
Classified routine:
Routine bit-complexity bookkeeping for a sparsification-style branching tree (in the spirit of Impagliazzo–Paturi–Zane sparsification), following directly from the bound on M in the preceding claim.

Uses

claimChoosing M keeps tree within 2^{sigma n}

Used by

Nothing in the paper

Sources

PaperOpen
Section
§A.3 The size of the tree
Page
—
Label
—
Line
main_full_version.tex:3870
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Per-node and parameter-search cost" rests on claim-lem-sparsify-4