lemmanovel

Counting zeros of sparse polynomial systems

Lemma·lem:tensor-sparse-query·§D.3 Arbitrary clause density

Statement (paper)

Fix integers k,c⩾1k,c\ge1. Let P1,…,PaP_1,\ldots,P_a be polynomials over F2\mathbb F_2 on n⩾20n\ge20 declared Boolean variables. Suppose a⩽cna\le cn and each PiP_i is listed as at most ⌈log⁡2n⌉c\lceil\log_2 n\rceil^c monomials of degree at most kk. The number of common zeros is computable deterministically in nOk,c(1)2Ok,c(nlog⁡log⁡n/log⁡n)n^{O_{k,c}(1)}2^{O_{k,c}(n\log\log n/\sqrt{\log n})} bit operations and nOk,c(1)n^{O_{k,c}(1)} bits of space.

In plain English

For a⩽cna\le cn polynomials over F2\mathbb F_2 in n⩾20n\ge20 Boolean variables, each given as at most ⌈log⁡2n⌉c\lceil\log_2 n\rceil^c monomials of degree at most kk, the number of common zeros can be computed deterministically in nOk,c(1)2Ok,c(nlog⁡log⁡n/log⁡n)n^{O_{k,c}(1)}2^{O_{k,c}(n\log\log n/\sqrt{\log n})} bit operations and polynomial space.

Why it's here

This is the subexponential counting engine for sparse systems with linearly many equations, which the main counting results call as a query. The proof branches on the few high-incidence variables, then uses the truncated-product parity extraction (Lemma 5.2) to write the count as a sum of low-degree bipartite network contractions. Each contraction is then evaluated by the tensor contraction theorem.
Classified novel:
This is the paper's subexponential counting engine for linearly many sparse F_2 equations. It combines branching on high-incidence variables, the paper's own truncated-product parity extraction, and its new subexponential tensor contraction theorem. Known #SAT/polynomial-system counting algorithms (e.g., Lokshtanov et al. 2017-style polynomial method) give only 2(1−δ)n2^{(1-\delta)n}, not 2o(n)2^{o(n)}.

Uses

lemParity indicator as linear-coefficient h-expansionlemTruncated product extracts parity indicators with linear degreethmSubexponential Boolean tensor network contraction

Used by

thmSubexponential deterministic k-CNF model countingclaimLeaf counts via parity rows and queries

Inside the proof

claimBranch on high-incidence variablesclaimMultilinear incidence polynomial with linear degreeclaimIndexing monomials with few wiresclaimNetwork contractions sum to branch polynomialclaimTest-group entries by subset inversionclaimContraction cost gives total running time

Sources

PaperOpen
Section
§D.3 Arbitrary clause density
Page
—
Label
lem:tensor-sparse-query
Line
quantitative-reduction.tex:108
Leannot aligned

Phase 2 aligns this node to a Lean declaration.