theoremroutineunresolved_ref

Counting zeros of sparse polynomials faster

Theorem·thm:overview-sparse-polynomials·§2.9 A faster algorithm for #k-SAT via counting solutions to sparse low-degree polynomial equations over F_2

Statement (paper)

Fix integers k⩾2k\ge2 and c⩾1c\ge1. Let P1,…,PmtestP_1,\ldots,P_{m_{\mathrm{test}}} be polynomials over F2\mathbb F_2 in n⩾20n\ge20 Boolean variables, with mtest⩽cnm_{\mathrm{test}}\le cn. Each PiP_i is given as a list of at most (log⁡n)c(\log n)^c monomials of degree at most kk. The exact number of common zeros in {0,1}n\{0,1\}^n can be computed deterministically in 2Ok,c(n(log⁡log⁡n)2/log⁡n)2^{O_{k,c}(n(\log\log n)^2/\sqrt{\log n})} bit operations and nOk,c(1)n^{O_{k,c}(1)} space.

In plain English

For fixed k⩾2k\ge2 and c⩾1c\ge1, given at most cncn polynomials over F2\mathbb F_2 in n⩾20n\ge20 variables, each with at most (log⁡n)c(\log n)^c monomials of degree at most kk, the number of common zeros in {0,1}n\{0,1\}^n can be computed deterministically in 2Ok,c(n(log⁡log⁡n)2/log⁡n)2^{O_{k,c}(n(\log\log n)^2/\sqrt{\log n})} bit operations and nOk,c(1)n^{O_{k,c}(1)} space.

Why it's here

This is the counting engine behind the faster #k\#k-SAT algorithm, giving a 2o(n)2^{o(n)} bound for sparse low-degree systems. The proof branches on high-incidence variables to bound incidence, picks explicit layout parameters, and applies the general counting proposition per branch, with the branching overhead absorbed into the exponent and a brute-force fallback for small nn.
Classified routine:
Assembles the earlier nodes: it branches on high-incidence variables to bound incidence, plugs in the explicit parameters of lem-incidence-parameters, and applies prop-count on each branch with a brute-force fallback for small n. The new counting machinery lives in prop-count and the layout lemmas; this theorem is bookkeeping on top of them.

Uses

lemExplicit parameter choice satisfies layout hypotheseslemLayout data is efficiently constructiblelemDeterministic balanced incidence labelingpropCost of counting solutions via factor evaluation

Used by

propRunning time of the interpolation counting algorithm

Inside the proof

claimBranch on high-incidence variablesclaimPer-branch parameters satisfy layout hypothesesclaimPer-branch cost and total exponentclaimNumerical checks with exhaustive fallbackclaimPolynomial space by sequential branches

Sources

PaperOpen
Section
§2.9 A faster algorithm for #k-SAT via counting solutions to sparse low-degree polynomial equations over F_2
Page
—
Label
thm:overview-sparse-polynomials
Line
main_full_version.tex:1640
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    Per-branch exponent uses the unlabeled cost estimate eq:three-costs from Section 3.5.