claimroutineinferred_dep

Leaf counts via parity rows and queries

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

Statement (paper)

For every nontrivial leaf

G

of the tree, the leaf count can be computed by taking the initial parity checks of Lemma and running the greedy procedure of Lemma , where each greedy step computes

N(A;h_\gamma)

for every candidate row

h_\gamma

via Lemma and appends one attaining the minimum, and one final call gives

N(A)

for the selected matrix, which equals the leaf count. Every row gives a degree-at-most-

k

equation with at most

2^k\max\{P,D_0\}=\lambda^{O_k(1)}

monomials, and every queried system has at most

6n

equations, with a single constant

c=c(k)

bounding both the ratio of equations to variables and the exponent of

\lambda

in the monomial bound for all sufficiently large

n

In plain English

For each nontrivial leaf

G

of the sparsification tree, its model count is obtained by building sparse parity checks, greedily appending rows with counting queries, and making a final query for

N(A)

, which equals the leaf count. All queried systems have at most

6n

equations of degree at most

k

with at most

\lambda^{O_k(1)}

monomials each, so one constant

c=c(k)

bounds both the equation-to-variable ratio and the monomial exponent for large

n

Why it's here

This combines the sparse checks of Lemma 6.1 and the greedy construction of Lemma 6.2, using the leaf sparsity from the previous claim (occurrence bound

B=\lambda^{O_k(1)}

). It checks that every query fits the hypotheses of the sparse-system counting lemma (linearly many equations, polylogarithmically many monomials), so each leaf can be counted in subexponential time, which the time and space accounting then uses.

Classified routine:

Direct assembly of the earlier lemmas (sparse checks, greedy hashes, sparse-query counting) with the leaf occurrence bound from the preceding claim. The only work is bookkeeping that the queried systems meet the counting lemma's hypotheses on equation count and monomial count.

Uses

lemSparse parity checks force large supportslemGreedy appended rows give exact countlemCounting zeros of sparse polynomial systemsclaimSparsify with sigma about 1/sqrt(log n)

Used by

claimArbitrary-density time and space accounting

Sources

PaperOpen

Section: §D.3 Arbitrary clause density
Page: —
Label: —
Line: quantitative-reduction.tex:330

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Leaf counts via parity rows and contraction queries" rests on claim-thm-main-3