claimroutineinferred_dep

Choosing M keeps tree within 2^{sigma n}

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

Statement (paper)

Testing powers of two M⩾ΓM\ge\Gamma in increasing order, computing CC and h=⌈log⁡2(4CM)⌉h=\lceil\log_2(4CM)\rceil exactly and stopping at the first MM with Γh⩽σM\Gamma h\le\sigma M, yields M=Ok(σ−1log⁡(2/σ))M=O_k\bigl(\sigma^{-1}\log(2/\sigma)\bigr). For this choice the exponent satisfies (Γn/M)log⁡2(4CM)⩽σn(\Gamma n/M)\log_2(4CM)\le\sigma n, so the tree has at most (Cn+1)2 2σn(Cn+1)^2\,2^{\sigma n} nodes.

In plain English

Searching powers of two M⩾ΓM\ge\Gamma in increasing order and stopping at the first one with Γh⩽σM\Gamma h\le\sigma M, where h=⌈log⁡2(4CM)⌉h=\lceil\log_2(4CM)\rceil, gives M=Ok(σ−1log⁡(2/σ))M=O_k(\sigma^{-1}\log(2/\sigma)). For this MM the exponent (Γn/M)log⁡2(4CM)(\Gamma n/M)\log_2(4CM) is at most σn\sigma n, so the tree has at most (Cn+1)2 2σn(Cn+1)^2\,2^{\sigma n} nodes.

Why it's here

This fixes the parameter MM so that the node-count bound from the previous claim becomes the poly⁡k(n,σ−1) 2σn\operatorname{poly}_k(n,\sigma^{-1})\,2^{\sigma n} size required by the lemma. It also keeps MM only about σ−1log⁡(2/σ)\sigma^{-1}\log(2/\sigma), which controls the occurrence bound BB in the leaves.
Classified routine:
A parameter-choice calculation that plugs a suitable M into the node-count bound of the previous claim (claim-lem-sparsify-3), in the style of the parameter tuning in Impagliazzo–Paturi–Zane sparsification.

Uses

claimTree size via B-choice positions

Used by

claimLeaf occurrence bound and count partitionclaimPer-node and parameter-search cost

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Choosing M keeps tree within 2^{sigma n}" rests on claim-lem-sparsify-3