claimroutine

Sparsify with sigma about 1/sqrt(log n)

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

Statement (paper)

For n⩾20n\ge20, applying Lemma  with σ=1/⌈λ⌉\sigma=1/\lceil\sqrt{\lambda}\rceil, where λ=⌈log⁡2n⌉\lambda=\lceil\log_2 n\rceil, yields a tree with nOk(1)2O(n/λ)n^{O_k(1)}2^{O(n/\sqrt{\lambda})} nodes and polynomial depth, in which every leaf has occurrence bound B=Ok((σ−1log⁡(2/σ))k−1)=λOk(1)B=O_k((\sigma^{-1}\log(2/\sigma))^{k-1})=\lambda^{O_k(1)} and at most BnBn nonempty clauses.

In plain English

For n⩾20n\ge20, taking σ=1/⌈λ⌉\sigma=1/\lceil\sqrt{\lambda}\rceil with λ=⌈log⁡2n⌉\lambda=\lceil\log_2 n\rceil in the sparsification lemma gives a polynomial-depth tree with nOk(1)2O(n/λ)n^{O_k(1)}2^{O(n/\sqrt{\lambda})} nodes. Every leaf has occurrence bound B=λOk(1)B=\lambda^{O_k(1)} and at most BnBn nonempty clauses.

Why it's here

This instantiates the sparsification lemma at a specific σ\sigma, trading an 2O(n/log⁡n)2^{O(n/\sqrt{\log n})} branching cost for leaves whose variable occurrences are only polylogarithmic in nn. Hence each leaf is a sparse kk-CNF with at most BnBn nonempty clauses, which the later leaf-counting steps and the time accounting rely on.
Classified routine:
This is a direct instantiation of the paper's sparsification lemma (lem-sparsify, in the style of the Impagliazzo–Paturi–Zane / Calabro–Impagliazzo–Paturi sparsification lemma) at σ≈1/√log n. The only work is substituting the parameter and simplifying the resulting bounds.

Uses

lemSparsification into bounded-occurrence k-CNF leaves

Used by

claimLeaf counts via parity rows and queriesclaimArbitrary-density time and space accounting

Sources

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

Phase 2 aligns this node to a Lean declaration.