claimroutine

Branch on high-incidence variables

Claim·§D.3 Arbitrary clause density·inside lemCounting zeros of sparse polynomial systems

Statement (paper)

Let

\lambda=\lceil\log_2 n\rceil

and

D_*=\max\{1,\lceil N_0/n\rceil\}\lceil\sqrt{\lambda}\rceil

. After normalizing monomials, at most

n/\sqrt{\lambda}

variables belong to more than

D_*

scopes, so fixing these variables in all possible ways partitions the original count into at most

2^{n/\sqrt{\lambda}}

branch counts. On each branch, after substituting the fixed bits and combining duplicate monomials, each free scope

I_i

has size at most

k\lambda^c

, each free variable appears in at most

D_*=\lambda^{O_{k,c}(1)}

scopes, and the branch count is either zero (a constant-one equation), or

2^{\text{number of free variables}}

(no equations remain), or is the number of common zeros of the remaining equations.

In plain English

Fixing the at most

n/\sqrt{\lambda}

variables that lie in more than

D_*

scopes, in all

2^{n/\sqrt{\lambda}}

possible ways at most, splits the count of common zeros into branch counts. In each branch every remaining scope has size at most

k\lambda^c

, every free variable lies in at most

D_*=\lambda^{O_{k,c}(1)}

scopes, and the branch count is zero,

2^{\#\text{free variables}}

, or the number of common zeros of the remaining equations.

Why it's here

This is the reduction step that gives the sparse system bounded variable degree, at the cost of only

2^{n/\sqrt{\lambda}}

branches. Since the total incidence count is small (at most

cn

equations, each with few monomials of degree at most

k

), few variables can have high incidence, so the branching is cheap. The later claims then work with a system whose scopes are small and whose variables each appear in few scopes.

Classified routine:

A Markov/averaging argument on the total incidence count, followed by the standard technique of exhaustively branching on the few high-degree variables to obtain a bounded-degree instance.

Uses

Nothing else in the paper

Used by

claimMultilinear incidence polynomial with linear degree

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.