claimroutineinferred_dep

Fixed-density counting via tensor contraction

Claim·§D.2 Fixed clause density·inside thmSubexponential deterministic k-CNF model counting

Statement (paper)

Let

s=n+m

. Applying Theorem over

\mathbb Z/2^{n+1}\mathbb Z

with

P_0=n+1

and

\ell=1

to the constructed bipartite network, and multiplying by

2^u

modulo

2^{n+1}

when

u

declared variables are unused, yields

\#F

as the least nonnegative residue, in time

s^{O_k(1)}2^{O_k(s/\sqrt{\log s})}

and polynomial space. In particular, when

m\le Dn

we have

n\le s\le(1+D)n

, so the running time is

(n+m)^{O_{k,D}(1)}2^{O_{k,D}(n/\sqrt{\log n})}

In plain English

Contracting the clause network over

\mathbb Z/2^{n+1}\mathbb Z

(with

P_0=n+1

\ell=1

), and multiplying by

2^u

for

u

unused variables, gives

\#F

in time

s^{O_k(1)}2^{O_k(s/\sqrt{\log s})}

and polynomial space, where

s=n+m

. When

m\le Dn

this is

(n+m)^{O_{k,D}(1)}2^{O_{k,D}(n/\sqrt{\log n})}

Why it's here

The clause network from the previous claim has

O_k(s)

edges and small degree, so the contraction theorem applies. Working modulo

2^{n+1}

is enough because

\#F\le 2^n

, so the residue is the exact count. Since

n\le s\le(1+D)n

when

m\le Dn

, the bound in terms of

s

becomes the stated fixed-density bound of the main theorem.

Classified routine:

Direct application of the paper's tensor-contraction theorem to the clause network from the previous claim, plus bookkeeping: #F ≤ 2^n makes the residue mod 2^{n+1} exact, each unused variable contributes a factor of 2, and n ≤ s ≤ (1+D)n converts the bound in s into a bound in n.

Uses

thmSubexponential Boolean tensor network contractionclaimClause network as bipartite tensor network

Used by

Nothing in the paper

Sources

PaperOpen

Section: §D.2 Fixed clause density
Page: —
Label: —
Line: quantitative-reduction.tex:86

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Fixed-density bound via contraction theorem" rests on claim-thm-main-1