claimroutineinferred_dep

Path length and B-choice bounds

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

Statement (paper)

Every root-to-node path in the tree has length at most CnCn, where C=4∑j=0k−2(3M)jC=4\sum_{j=0}^{k-2}(3M)^j, and the path chooses the BB-child in at most Γn/M\Gamma n/M times, where Γ=4∑j=0k−23j=2(3k−1−1)\Gamma=4\sum_{j=0}^{k-2}3^j=2(3^{k-1}-1).

In plain English

Every root-to-node path in the sparsification tree has length at most CnCn with C=4∑j=0k−2(3M)jC=4\sum_{j=0}^{k-2}(3M)^j, and it takes the BB-child at most Γn/M\Gamma n/M times, where Γ=4∑j=0k−23j=2(3k−1−1)\Gamma=4\sum_{j=0}^{k-2}3^j=2(3^{k-1}-1).

Why it's here

This follows from the linear bound on width-jj insertions per path (Lemma A.3) together with the branching rule's insertion counts (Lemma A.1). Summing over widths jj gives the depth bound CnCn, and the BB-child count is capped using the fact that each BB-child inserts many clauses. These bounds let the node-count claim describe each node by its depth and the positions of its BB-choices, giving the 2σn2^{\sigma n} size bound.
Classified routine:
Direct bookkeeping consequence of the per-width insertion bound (Lemma A.3) and the branching rule's insertion counts (Lemma A.1): summing TjT_j over widths gives the depth bound, and dividing by the minimum number of insertions per B-child caps the B-choices, as in the Impagliazzo–Paturi–Zane sparsification lemma analysis.

Uses

lemWidth-j insertions are linearly boundedlemSparsification branching rule is sound

Used by

claimTree size via B-choice positions

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Path length and B-choice bounds" rests on lem:spar-insertion-bound
  • info
    inferred_dep
    outline: "Path length and B-choice bounds" rests on lem:spar-branch