lemmaroutineinferred_depstructure_uncertain

Sparsification into bounded-occurrence k-CNF leaves

Lemma·lem:sparsify·§6.4 Returning to a general formula

Statement (paper)

Fix k⩾2k\ge2. Given a kk-CNF on nn declared variables with mm clauses and a rational 0<σ⩽10<\sigma\le1, a deterministic algorithm constructs a tree of kk-CNFs on the same variables. Let LσL_\sigma be the total binary encoding length of the supplied numerator and denominator of σ\sigma. An assignment satisfies the input exactly when it satisfies one leaf formula, and it cannot satisfy two distinct leaves. The tree has poly⁡k(n,σ−1) 2σn \operatorname{poly}_k(n,\sigma^{-1})\,2^{\sigma n} nodes and depth poly⁡k(n,σ−1)\poly_k(n,\sigma^{-1}). In every leaf, each variable occurs at most BB times, where BB is an explicitly computed integer satisfying B=Ok ⁣([σ−1log⁡(2/σ)]k−1). B=O_k\!\Bigl(\bigl[\sigma^{-1}\log(2/\sigma)\bigr]^{k-1}\Bigr). Input normalization uses poly⁡k(n,m)\poly_k(n,m) bit operations. Constructing the numerical parameters uses poly⁡k(Lσ)\poly_k(L_\sigma) bit operations. Thereafter, processing each node uses poly⁡k(n,log⁡(2/σ))\poly_k(n,\log(2/\sigma)) bit operations. The input count is the sum of the leaf counts.

In plain English

Given a kk-CNF and a rational 0<σ⩽10<\sigma\le1, a deterministic algorithm builds a tree of kk-CNFs on the same variables with poly⁡k(n,σ−1)2σn\operatorname{poly}_k(n,\sigma^{-1})2^{\sigma n} nodes and polynomial depth. Every satisfying assignment of the input satisfies exactly one leaf, and in each leaf every variable occurs at most B=Ok([σ−1log⁡(2/σ)]k−1)B=O_k([\sigma^{-1}\log(2/\sigma)]^{k-1}) times, so the input count is the sum of the leaf counts.

Why it's here

This lemma reduces counting for a general kk-CNF to counting for formulas with bounded variable occurrence, at a cost of only 2σn2^{\sigma n} branches. It assembles the branching rule (Lemma A.1) and the insertion bounds (Lemmas A.2, A.3) into path-length and B-choice bounds. A suitable MM then turns these into the size, occurrence, partition and running-time guarantees that the main theorem's sparsification step uses.
Classified routine:
This is a version of the Sparsification Lemma of Impagliazzo, Paturi and Zane (2001), in the disjoint-leaves, bounded-occurrence form later given by Calabro, Impagliazzo and Paturi. Its proof assembles the standard IPZ branching and insertion-count arguments from the appendix lemmas, with explicit bit-complexity bookkeeping.

Uses

lemSparsification branching rule is soundlemMarked clauses containing a set are fewlemWidth-j insertions are linearly bounded

Used by

thmSubexponential deterministic k-CNF model countingpropRunning time of the interpolation counting algorithmclaimSparsify with sigma about 1/sqrt(log n)

Inside the proof

claimBranching rule with disjoint childrenclaimPath length and B-choice boundsclaimTree size via B-choice positionsclaimChoosing M keeps tree within 2^{sigma n}claimLeaf occurrence bound and count partitionclaimPer-node and parameter-search cost

Sources

PaperOpen
Section
§6.4 Returning to a general formula
Page
—
Label
lem:sparsify
Line
main_full_version.tex:3543
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    Appendix  proves the lemma, including the disjointness (the branching rule partitions satisfying assignments of the parent)
  • info
    inferred_dep
    the appendix proving this lemma (app:sparsify) contains the marked-degree counting bound used in the occurrence bound B
  • info
    inferred_dep
    the appendix proving this lemma (app:sparsify) contains the insertion bound used for depth and node count
  • info
    structure_uncertain
    No proof environment; Appendix A (main_full_version.tex:3636-3884) proves it using Lemmas A.1-A.3 plus unlabeled tree-size and leaf-bound arguments.