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\ge20

, applying Lemma with

\sigma=1/\lceil\sqrt{\lambda}\rceil

, where

\lambda=\lceil\log_2 n\rceil

, yields a tree with

n^{O_k(1)}2^{O(n/\sqrt{\lambda})}

nodes and polynomial depth, in which every leaf has occurrence bound

B=O_k((\sigma^{-1}\log(2/\sigma))^{k-1})=\lambda^{O_k(1)}

and at most

Bn

nonempty clauses.

In plain English

For

n\ge20

, taking

\sigma=1/\lceil\sqrt{\lambda}\rceil

with

\lambda=\lceil\log_2 n\rceil

in the sparsification lemma gives a polynomial-depth tree with

n^{O_k(1)}2^{O(n/\sqrt{\lambda})}

nodes. Every leaf has occurrence bound

B=\lambda^{O_k(1)}

and at most

Bn

nonempty clauses.

Why it's here

This instantiates the sparsification lemma at a specific

\sigma

, trading an

2^{O(n/\sqrt{\log n})}

branching cost for leaves whose variable occurrences are only polylogarithmic in

n

. Hence each leaf is a sparse

k

-CNF with at most

Bn

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.

Selected node

Statement (paper)

In plain English

Why it's here