\documentclass[11pt,reqno]{amsart}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{dsfont}
\usepackage[margin=1in]{geometry}
\usepackage{microtype}
\usepackage[colorlinks=true,allcolors=blue,backref=page]{hyperref}
\numberwithin{equation}{section}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}\newtheorem{remark}[theorem]{Remark}
\newcommand{\poly}{\operatorname{poly}}
\newcommand{\Prob}{\mathbb P}
\DeclareMathOperator{\Bin}{Bin}
\allowdisplaybreaks[2]
\renewcommand{\le}{\leqslant}
\renewcommand{\ge}{\geqslant}
\setlength{\emergencystretch}{1.5em}
\setcounter{tocdepth}{1}
\title{The Exponential Time Hypothesis is False}
\author{OpenAI}
\date{17 October 2026, revised 25 October 2026}
\hypersetup{pdftitle={ETH is False},
 pdfauthor={OpenAI},
 pdfsubject={Exact counting, sparse parity tests, and polynomial interpolation}}
\begin{document}
\begin{abstract}
We give a deterministic algorithm for exactly counting the satisfying assignments
of an arbitrary $k$-CNF formula.
For every fixed $k\ge2$, on a formula with $n$ variables and $m$ clauses,
our algorithm uses $\poly_k(n,m)$ space and runs in time
$(n+m)^{O_k(1)}2^{\,n/(\log n)^{\frac12+o(1)}}$.
Our algorithm refutes the Exponential Time Hypothesis (ETH), which
postulates that deciding $3$-SAT on $n$ variables requires
$2^{\Omega(n)}$ time in the worst case.
\end{abstract}
\maketitle

\tableofcontents
\vspace{-\baselineskip}

\section{Introduction}
For every fixed $k\ge3$, $k$-SAT is the canonical NP-complete
problem~\cite{Cook71}, and its exponential-time complexity underlies the Exponential Time
Hypothesis (ETH) and the Strong Exponential Time Hypothesis
(SETH)~\cite{IP01,IPZ}.
In this paper, we refute ETH by giving, for every fixed $k\ge2$,
a deterministic algorithm that counts the satisfying assignments
of a $k$-CNF in subexponential time and polynomial space.

Write the input $k$-CNF on $n$ declared variables with $m$ input clauses as
\[
 F(x_1,\ldots,x_n)=\bigwedge_{e=1}^m
 \bigl[(x_{i_{e,1}}\oplus b_{e,1})\vee\cdots\vee
       (x_{i_{e,k}}\oplus b_{e,k})\bigr],
\]
where $i_{e,j}\in\{1,\ldots,n\}$ and $b_{e,j}\in\{0,1\}$ are the
variable index and negation bit of the $j$th literal in clause $e$,
and $\oplus$ denotes addition modulo two. Repeating a literal permits
clauses with fewer than $k$ literals.
The indices $i_{e,j}$ and bits $b_{e,j}$ are fixed by $F$;
only $x_1,\ldots,x_n$ vary over assignments.
Our aim is to compute the quantity
\begin{equation}\label{eq:solution-count}
 \#F=\bigl|\{x\in\{0,1\}^n:F(x)=1\}\bigr|.
\end{equation}
Testing $\#F>0$ also decides satisfiability.
We keep $k$ fixed as $n$ grows.
Throughout, $\log$ denotes the natural logarithm.
\begin{theorem}\label{thm:main}
For each fixed $k\ge2$, there exists a deterministic algorithm that,
given a $k$-CNF $F$ on $n\ge20$ declared variables with $m$ clauses,
computes $\#F$ as defined in \eqref{eq:solution-count} in
\[
 (n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})}
\]
bit operations and $(n+m)^{O_k(1)}$ bits of space.
For each fixed $D>0$, its running time on inputs with $m\le Dn$ is
\[
 (n+m)^{O_{k,D}(1)}2^{O_{k,D}(n/\sqrt{\log n})}.
\]
\end{theorem}

The rational interpolation argument in Section~\ref{subsec:general-reduction}
gives the weaker exponent $O_k(\rho(n))$, where
\[
 \rho(n)=\frac{n(\log\log n)^2}{\sqrt{\log n}}
          =\frac{n}{(\log n)^{\frac12+o(1)}}.
\]
Appendix~\ref{app:quantitative} proves both bounds in
Theorem~\ref{thm:main} by tensor contraction.

When $\#F>0$, the standard self-reduction finds a satisfying
assignment by fixing one variable at a time and checking that the
remaining count is positive. Choosing each bit according to the two
conditional counts instead gives an exactly uniform random satisfying
assignment, with $\poly_k(n,m)$ expected overhead~\cite[Theorem~3.3(1)]{JVV86}.

The theorem also yields arbitrarily accurate subexponential-time
approximation algorithms for Max-$k$-SAT.
The Unique Games
Theorem~\cite[Section~8.1]{OpenAIUGC26} implies NP-hardness bounds
for Max-$k$-SAT that match, up to arbitrarily small error in the
approximation ratio, the guarantees of the semidefinite-programming
algorithm of~\cite{Rag08}.
Write $\operatorname{OPT}(F)$ for the maximum number of clauses of $F$
simultaneously satisfied by an assignment.
\begin{corollary}\label{cor:max-sat-approximation}
For every fixed $k\ge2$ and $\varepsilon>0$, there exists a randomized
algorithm that, given a $k$-CNF $F$ on $n\ge20$ variables with $m$ clauses,
finds an assignment satisfying at least
$\operatorname{OPT}(F)-\varepsilon m$ clauses with probability
$1-2^{-\Omega(n)}$, in
\[
 (n+m)^{O_{k,\varepsilon}(1)}2^{O_{k,\varepsilon}(\rho(n))}
\]
time and $(n+m)^{O_{k,\varepsilon}(1)}$ space.
\end{corollary}
\begin{proof}
We may assume $m>0$.
Let $f(x)$ be the fraction of clauses satisfied by $x$, and let
$\widehat f(x)$ be that fraction in a sample of $O(n/\varepsilon^2)$
clauses chosen independently and uniformly with replacement.
Hoeffding's inequality and a union bound over all $2^n$ assignments
give, with probability $1-2^{-\Omega(n)}$,
\[
 |\widehat f(x)-f(x)|\le\varepsilon/2
 \qquad\text{for every }x\in\{0,1\}^n.
\]
Thus, if $\widehat x$ maximizes $\widehat f$, then
$f(\widehat x)\ge\max_x f(x)-\varepsilon$.
Given an integer threshold $b$, a Boolean circuit with at most two
inputs per gate and size $O_{k,\varepsilon}(n)$ tests whether an
assignment satisfies at least $b$ sampled clauses.
The standard circuit-to-$3$-CNF reduction~\cite[Lemmas~15.9--15.10]{Bar23}
produces a formula with $O_{k,\varepsilon}(n)$ variables and clauses
that is satisfiable exactly when this threshold can be attained.
Theorem~\ref{thm:main}, binary search on the threshold, and
self-reduction then find an exact sample optimizer within the stated bounds.
Truncating rejection sampling after $O(n+\log(n/\varepsilon^2))$
trials per sample gives worst-case $\poly(n,m,\varepsilon^{-1})$
sampling time and adds
at most $2^{-\Omega(n)}$ to the failure probability.
\end{proof}

Note that runtime bounds of the form $2^{o(n)}$ do not transfer under general polynomial-time reductions ($2^{n^{o(1)}}$ would be needed for this), so our result does not imply that general NP problems admit subexponential time algorithms. However we do obtain subexponential time algorithms for counting graph colorings and perfect matchings.

\begin{corollary}\label{cor:graph-counting}
On simple graphs with $v$ vertices and $e$ edges, the number of
independent sets and, for each fixed $q\ge2$, the number of proper
$q$-colorings can be computed deterministically in $2^{o(v)}$ time
and $\poly_q(v,e)$ space. The number of perfect matchings can be
computed deterministically in $2^{o(v+e)}$ time and $\poly(v,e)$ space.
\end{corollary}
\begin{proof}
For $G=(V,E)$, introduce a Boolean variable $x_u$ for each $u\in V$.
Satisfying assignments of
\[
 \bigwedge_{\{u,w\}\in E}(\neg x_u\vee\neg x_w)
\]
correspond bijectively to the independent sets $\{u\in V:x_u=1\}$.
For proper $q$-colorings, use one Boolean variable per vertex and
color, require exactly one color at each vertex, and forbid equal
colors at adjacent vertices. This gives a counting-preserving
$q$-CNF encoding with $qv$ variables and $O_q(v+e)$ clauses.

For perfect matchings, use one Boolean variable per edge and a
linear-size circuit checking that exactly one selected edge meets
each vertex. The standard circuit-to-$3$-CNF
reduction~\cite[Lemmas~15.9--15.10]{Bar23} gives $O(v+e)$ variables
and clauses. The gate variables have unique values once the edge
bits are fixed, so this encoding also preserves the count.
Theorem~\ref{thm:main} gives the stated time and space bounds.
\end{proof}

The fixed-density case of Theorem~\ref{thm:main} gives a circuit lower
bound for $\mathrm E^{\mathrm{NP}}$, the class of languages decidable
in deterministic time $2^{O(n)}$ with an NP oracle.

\begin{corollary}\label{cor:quantitative-circuits}
Let $C_L(n)$ be the minimum number of noninput gates in a circuit
computing $L$ on $\{0,1\}^n$, allowing arbitrary Boolean gates of
fan-in at most two and unrestricted fan-out. There exist a language
$L\in\mathrm E^{\mathrm{NP}}$ and a constant $c>0$ such that
\begin{equation}\label{eq:quantitative-circuit-lower-bound}
 C_L(n)>c\,n\sqrt{\log n}\qquad\text{for infinitely many }n.
\end{equation}
\end{corollary}

Appendix~\ref{subsec:circuit-lower-bounds} proves the corollary.
Appendix~\ref{subsec:local-inversion} gives algorithms for inversion
and exact preimage counting of Boolean maps with constant output locality.

\subsection{Related work}\label{sec:related}
We first discuss earlier SAT and counting algorithms and the
complexity hypotheses contradicted by Theorem~\ref{thm:main}.
We then compare our approach with earlier algebraic algorithms and
identify the existing constructions used in our proof, whose roles
are developed in the roadmap in
Section~\ref{sec:technical-overview}.

\subsubsection{SAT algorithms and the exponential-time hypotheses}\label{subsec:related-sat}
Sch\"oning's local-search algorithm and PPSZ are landmarks in the
development of exponential-time algorithms for $k$-SAT~\cite{Schon99,PPSZ05}.
Sch\"oning's randomized algorithm starts from a random assignment
and repeatedly flips a uniformly chosen variable in an unsatisfied clause. Its
bounded-error decision time is
\[
 (n+m)^{O(1)}(2-2/k)^n
\]
for each fixed $k\ge3$~\cite[Section~2]{Schon99}.
In particular, this gives $(n+m)^{O(1)}(4/3)^n$ time for $3$-SAT.
The PPSZ algorithm~\cite{PPSZ05} uses a different mechanism: bounded resolution derives
additional clauses, after which variables are assigned in a random
order, taking forced values when available and guessing
otherwise. For $k=3,4$, its original analysis gave stronger
bounds for uniquely satisfiable formulas than for general ones.
The unique-SAT guarantees were later extended to general $3$-SAT and
$4$-SAT; for $3$-SAT this gave a randomized
$O(1.308^n)$ bound~\cite{Hertli14}.
Hansen, Kaplan, Zamir, and Zwick improved the PPSZ bound for every
fixed $k\ge3$ by biasing the algorithm's guesses~\cite{HKZZ19}.
Scheder obtained an improvement for the same range of $k$ by sharpening
the analysis of the original PPSZ algorithm~\cite[Theorem~1.5]{Scheder24}.
For general $3$-SAT, a preprint by Jiang and Cai gives a randomized
$O^*(1.307031578^n)$ bound~\cite[Corollary~1.2]{JC26}, where $O^*$
suppresses factors polynomial in the input size. Liu's deterministic
algorithm combines branching with derandomized local search and solves
$3$-SAT in $O(1.32793^n)$ time~\cite[Theorem~21]{Liu18}.

Randomized local search has also produced effective heuristics.
The WalkSAT heuristic chooses an
unsatisfied clause and flips one of its variables, combining random
choices with greedy moves~\cite{SKC94}. Experiments on formulas
from circuit synthesis and diagnosis demonstrated the practical value
of this approach~\cite[pp.~340--342, Tables~4--5]{SKC94}.

Among uniformly random $k$-CNFs, instances at the satisfiability
threshold were conjectured to be the hardest for deciding satisfiability~\cite[Section~1]{VW21};
for fixed $k\ge3$ and lower clause densities $m/n\le 2^k/k^C$,
where $C$ is a universal constant,
polynomial-time almost-uniform sampling of satisfying assignments is
known with high probability over the formula~\cite[Theorem~1.2]{CLWYY25}.
For a uniformly random formula with polynomially many clauses,
conditioned on satisfiability, Vyas and Williams~\cite[Theorem~3]{VW21} give a PPZ-based
algorithm that finds a solution in $2^{n(1-\Omega(\log k/k))}$ time with high
probability over both the formula and the algorithm's random choices.

The Exponential Time Hypothesis (ETH) asserted that $3$-SAT requires
$2^{\Omega(n)}$ deterministic time in the worst case, and hence so does
$k$-SAT for every fixed $k\ge3$~\cite[Theorem~1]{IP01}.
The Strong Exponential Time Hypothesis (SETH) made the sharper
prediction that $k$-SAT requires $2^{n(1-o_k(1))}$ time as $k$ grows.
Precisely, for every $\varepsilon\in(0,1)$, there is a fixed $k$ for
which no deterministic algorithm solves $k$-SAT in
$2^{(1-\varepsilon)n}(n+m)^{O(1)}$ time.
The running-time bounds for Sch\"oning's algorithm and PPSZ helped
motivate this prediction: their improvements over exhaustive search
diminish as $k$ grows~\cite[Open Problems, item~2]{IP01}.

The Gap Exponential Time Hypothesis (Gap-ETH) strengthens ETH by
postulating constants $\delta,\gamma>0$ for which no $O(2^{\gamma n})$-time
algorithm can distinguish a satisfiable $3$-CNF from one in which
every assignment violates at least a $\delta$ fraction of the clauses,
even when $m=O(n)$~\cite{Din16,MR17}. The randomized version rules
out an algorithm with the same running time that distinguishes the
two cases with probability at least $2/3$ on every promised
input~\cite[Conjecture~2.5]{CCK20}.
It has been used to prove hardness of approximating Label
Cover~\cite{Din16} and dense constraint satisfaction
problems~\cite{MR17}. It also rules out nontrivial fixed-parameter
approximations for Clique and Dominating Set. For Clique, the excluded
ratios are $o(\mathrm{OPT})$, where $\mathrm{OPT}$ is the maximum
clique size~\cite[Corollaries~5.3 and~5.6]{CCK20}.

The Nondeterministic Strong Exponential Time Hypothesis (NSETH)
asserts that, for every $\varepsilon>0$, some fixed $k$ admits no
nondeterministic $2^{(1-\varepsilon)n}(n+m)^{O(1)}$-time algorithm
for deciding whether a $k$-CNF is \emph{unsatisfiable}, or equivalently
whether a $k$-DNF is a tautology~\cite{CGIMPS16}.
NSETH has been used to establish barriers to deterministic fine-grained
reductions from SAT to problems such as 3SUM and All-Pairs Shortest
Paths~\cite{CGIMPS16}, and to delineate SETH-based lower bounds for
approximating directed graph diameter~\cite{Li21}.

Theorem~\ref{thm:main} refutes ETH, SETH, Gap-ETH, and NSETH.
Indeed, testing whether the exact count is positive or zero decides
both satisfiability and unsatisfiability in deterministic
$2^{o(n)}(n+m)^{O_k(1)}$ time for every fixed $k$; deciding
satisfiability also solves the Gap-ETH promise problem.
The deterministic algorithm also refutes the bounded-error randomized
versions of ETH~\cite[Section~1]{DHMTW} and SETH~\cite[Definition~2.1]{CDL16}, and of Gap-ETH.
It does not conflict with unconditional exponential lower bounds for
restricted proof systems such as regular resolution~\cite{BeckImp13}.
In 2016, Ryan Williams refuted the Merlin--Arthur version of SETH
(MA-SETH) by giving a protocol that certifies $k$-CNF unsatisfiability
in $2^{n/2}\poly(n,m)$ time~\cite[Theorem~3.3]{Wil16}.

\subsubsection{Exact counting and counting complexity}\label{subsec:related-counting}
In Valiant's framework, $\#\mathrm{SAT}$ and $\#3$-SAT are
$\#\mathrm P$-complete under parsimonious
reductions~\cite[Section~3, Facts~1--2]{Val79}.
For fixed $k\ge3$, previous exact-counting algorithms achieve
$\poly_k(n,m)2^{n-\Omega(n/k)}$ time, with a Las Vegas
expected-time bound in~\cite[Lemma~3.5]{IMP12} and a deterministic
bound in~\cite[Theorem~1.6]{CW21}.
For $\#2$-SAT, Wahlstr\"om's algorithm counts satisfying assignments
in $O^*(1.2377^n)$ time~\cite{Wahlstrom08}. For $\#3$-SAT, Kutzkov
uses complementary branching to count satisfying assignments in
$O^*(1.637^n)$ time~\cite{Kutzkov26}. Both algorithms are deterministic.

The counting Exponential Time Hypothesis ($\#\mathrm{ETH}$)
asserted that exactly counting the satisfying assignments of a $3$-CNF
requires $2^{\Omega(n)}$ deterministic time~\cite[Section~1]{DHMTW}.
Under $\#\mathrm{ETH}$, Curticapean~\cite{Cur18} rules out deterministic
$2^{o(v)}$-time algorithms for counting perfect matchings even in
unweighted bipartite graphs with $v$ vertices and $O(v)$ edges.
The perfect-matching algorithm in Corollary~\ref{cor:graph-counting}
applies in particular to these graphs.
Our algorithm (Theorem~\ref{thm:main}) solves $\#3$-SAT deterministically
in $2^{o(n)}\poly(n,m)$ time and therefore refutes $\#\mathrm{ETH}$.

\subsubsection{Implications for fine-grained complexity}\label{subsec:related-consequences}
ETH and SETH became standard assumptions for parameterized and
fine-grained complexity~\cite{IPZ,VW19}.
ETH-based reductions yielded lower bounds for the dependence on
solution size in Clique~\cite{CHKX06}, and on treewidth in constraint
satisfaction and partitioned subgraph isomorphism~\cite{Marx10}.
SETH supported sharp exponential bounds for Hitting Set and Set
Splitting~\cite{CDL16}, and for Independent Set and Dominating Set
parameterized by treewidth~\cite{LMS18}.
It also gave bounds on possible speedups of pseudopolynomial algorithms
for Subset Sum and Bicriteria Path~\cite{ABHS19}.

For problems in $\mathrm P$, SETH was used to rule out polynomial-factor
speedups over quadratic running times for edit
distance~\cite{BackursIndyk18}, longest common subsequence and dynamic
time warping~\cite{BK15}, Fr\'echet distance~\cite{Bri14}, and
regular-expression matching~\cite{BI16}.
Other applications concerned approximating graph
diameter~\cite{RV13} and maintaining reachability counts or the size
of the largest strongly connected component under graph
updates~\cite{AW14}.
Together these results made SETH a common basis for explaining the
apparent optimality of algorithms across quite different problems.

Our refutation of ETH and SETH removes one basis for the hardness claims
above. Some of the same lower bounds follow from weaker hypotheses that
may still hold. For example, the lower bounds for longest common
subsequence and regular-expression matching follow from the Orthogonal
Vectors Conjecture (OVC)~\cite{BK15,BI16}. OVC asserts that for every
fixed $\varepsilon>0$, no $O(N^{2-\varepsilon}\poly(d))$-time algorithm
can decide whether two sets of $N$ Boolean vectors of dimension $d$
contain an orthogonal pair, one vector from each set. The reduction
from SAT to Orthogonal Vectors shows that SETH implies OVC~\cite{Wil05,VW19}.
The lower bounds for Fr\'echet distance, graph diameter approximation,
and the treewidth dependence of Independent Set and Dominating Set also
follow from the hypothesis that unrestricted CNF-SAT admits no
$2^{(1-\delta)n}\poly(n,m)$-time algorithm for any constant
$\delta>0$~\cite{Bri14,RV13,LMS18}. Theorem~\ref{thm:main} gives a
running-time guarantee for each fixed clause width $k$, while this
hypothesis allows the width to grow with $n$.

To obtain a faster algorithm for a target problem from our SAT algorithm,
we need a reduction in the other direction, from that problem to
fixed-width SAT, that controls the number of variables. Set Splitting
with sets of size at most $k$ has such a
reduction~\cite[Observation~3.6]{CDL16}: use one Boolean variable per
element to specify its side of the split. For each set, one clause
requires at least one of its variables to be true, and a second requires
at least one to be false. The resulting $k$-CNF has one variable per
universe element, so for fixed $k$ Theorem~\ref{thm:main} gives
subexponential time in the universe size, up to a polynomial input-size
factor.

\subsubsection{Prior work on algebraic algorithms for combinatorial problems}\label{subsec:related-algebraic}
Our algorithm is algebraic, based on polynomial interpolation of carefully chosen auxiliary variables. Below we discuss prior work on using algebraic methods to design algorithm for combinatorial problems. For broader background, see the surveys of Koutis and
Williams~\cite{KW16} on algebraic fingerprints, Williams~\cite{Wil14}
on the polynomial method in algorithm design, and
Husfeldt~\cite{Hus11} on algorithmic inclusion--exclusion.

Williams's split-and-list algorithm~\cite{Wil05} partitions the
variables of a $2$-CSP into three groups, enumerates partial assignments,
and combines them using fast matrix multiplication.
Koivisto~\cite{Koi06} gives a direct sum--product formulation.
The algorithm of Sections~\ref{sec:counting}--\ref{sec:hashes}
likewise enumerates assignments within groups. Fixing
the shared measurements $\vec y$ makes their contributions multiply
independently. Scott and Sorkin~\cite[Section~6]{SS09} extend
split-and-list to polynomial-valued weights and arbitrary rings.
Our summation routine similarly uses truncated polynomial rings to
retain several coefficients in one computation.

Bj\"orklund~\cite[Sections~2--3]{Bjo16} uses inclusion--exclusion and
polynomial interpolation to reduce permanent and directed
Hamiltonian-cycle counting to a weighted sum over smaller instances.
He adds the weights of identical instances in a table, then solves each
distinct instance with nonzero total weight once.
Bj\"orklund, Kaski, and Williams~\cite{BKW19} use
low-degree curves and generalized Kakeya sets to recover polynomial
values from evaluations on a small structured set, yielding faster
algorithms for fermionants, including the permanent of integer matrices whose entries are bounded in absolute value by a fixed constant.
Our polynomial replacements serve a similar purpose: they connect
the desired count to structured evaluations from which it can be
reconstructed. Here the useful structure is separation into groups
after fixing a few shared measurements.

Bhargava, Ghosh, Kumar, and
Mohapatra~\cite[Sections~3.1--3.2]{BGKM23} evaluate multivariate
polynomials over finite fields along low-degree curves, using
Hasse derivatives and Hermite interpolation when values alone do not
suffice. For a univariate restriction $g$, the order-$j$
Hasse derivative at $t$ is the coefficient of $z^j$ in $g(t+z)$. We use the same recovery principle: compute several Taylor
coefficients at each point admitting fast summation, then recover
the original count by Hermite interpolation.

Woodruff and Yekhanin~\cite{WY07} use values and first derivatives
along a line to recover a target value in private information retrieval.
Kopparty, Saraf, and Yekhanin~\cite{KSY14} use higher-order
Hasse derivatives for local correction of multiplicity codes, extending the
line-based recovery of Reed--Muller codes. In our algorithm, the
matrix construction supplies low-degree replacement forms that let us
compute the Taylor coefficients at the interpolation points by fast
summation after fixing a few shared measurements.

\subsubsection{Antecedents of the matrix construction}\label{subsec:related-spectral}
Our counting algorithm evaluates sums of products of polynomials over
Boolean assignments. The polynomials share variables, so these sums
do not factor into independent smaller sums. We introduce linear
substitutions, depending polynomially on an interpolation parameter,
that make such a factorization possible after fixing a few integer
linear measurements. An auxiliary square rational matrix $M_0$
underlies these substitutions: a bound on $\operatorname{rank}(I-M_0)$
limits the number of measurements, while restrictions on the nonzero
entries of $M_0$ keep the substitution degrees small.
Section~\ref{subsec:preview-auxiliary} explains this connection.

Related interpolation methods have been used to obtain low-rank
approximations to structured matrices. In~\cite[Section~3]{AW17},
a low-degree polynomial matches $(-1)^j$ on an interval of integer
inner products $j$, using the interpolation lemma
of~\cite[Lemma~3.1]{AW15}. This gives low-rank matrices agreeing with
Walsh--Hadamard matrices in most entries, a result in the study of
matrix rigidity~\cite{Val77}. Related interpolation gives rigidity
bounds for Kronecker powers in~\cite[Theorem~6.1]{AGP23}.
Dvir and Liu~\cite[Claim~2.20 and Lemmas~3.3--3.4]{DL20} use a spectral approach:
sparse changes to a function invariant under permutations of its coordinates make many Fourier coefficients vanish,
reducing the rank of its group-circulant matrix.

Our construction also interpolates $(-1)^j$ on a short interval, now
to obtain a polynomial in commuting permutation matrices. The same
polynomial gives both the rank bound for $I-M_0$ and the restrictions
on the nonzero entries of $M_0$. We prove these properties and their
quantitative bounds directly in Section~\ref{sec:construction}.

\subsubsection{Sparsification and parity tests}\label{subsec:related-reductions}
We use the counting-preserving version~\cite[Appendix~A]{DHMTW} of
the sparsification lemma~\cite{IPZ}, with quantitative bounds
from~\cite[Section~6]{CIP} and
\cite[Lemma~5.14 and equation~(5.4)]{CalabroThesis}.
This partitions the satisfying assignments among sparse formulas on
the same Boolean variables. Appendix~\ref{app:sparsify} records the
disjoint branching argument and the bounds needed when its parameter
varies with the input size.

The initial parity tests are the constraints of a Tanner code
\cite[Section~II]{Tanner81}, applied to the binary vector recording
which clauses an assignment violates. We use the edge-based
expander-code construction of~\cite[Sections~IV and~VI]{SS96}:
each graph edge carries one bit, and each vertex requires its
incident bits to belong to a fixed binary linear code. The local
code's minimum distance, together with graph expansion, forces
every nonzero vector satisfying all these constraints to have
large support. This construction and distance argument are standard.
Lemma~\ref{lem:sparse-checks} supplies the parameter choices needed
here, including the bounds on the number and support size of the
tests, and constructs the graph and local code by deterministic
exhaustive searches. The graph is the bipartite double cover of a Cayley multigraph.
The shifts defining that multigraph nearly balance every nonconstant
parity on the base group: this is
the small-bias condition~\cite{NN93,AR94}, stated explicitly in
\eqref{eq:hash-walsh}. Fixing unused edge bits to zero gives a code
on exactly $m$ coordinates.
Additional parity tests exclude the remaining nonzero violation
vectors. We choose these tests by the
averaging principle underlying the method of conditional
expectations~\cite{Raghavan88}, using exact counts to evaluate each
candidate. Section~\ref{sec:hashes} gives the constructions and
quantitative bounds needed here.

Theorem~\ref{thm:main} invites a renewed search for algorithms for
problems whose known hardness results relied on ETH or SETH. The
examples in Section~\ref{subsec:related-consequences} suggest both
immediate consequences and problems for which new algorithmic ideas
are needed.

\subsection{Notation}\label{subsec:notation}
For an integer $s\ge0$, write $[s]=\{1,\ldots,s\}$, with
$[0]=\varnothing$. For a condition $E$, the scalar
$\mathds{1}_{\{E\}}$ equals one if $E$ holds and zero otherwise.
We use natural logarithms, writing $\log_2$ when the base is two.
For complexity bounds, $\poly(t_1,\ldots,t_s)$ denotes a bound of the
form $(1+t_1+\cdots+t_s)^{O(1)}$, with absolute implicit constants.
Subscripts, as in $\poly_{k,c}(t_1,\ldots,t_s)$, allow those constants
to depend on the indicated fixed parameters. Integers are stored in
signed binary notation, so an integer $z$ uses $O(\log(|z|+2))$ bits.
Rational numbers are stored as an integer numerator and a positive
integer denominator; stated bit-length bounds apply to each of them.
Space is measured in bits. Arithmetic-operation counts are distinguished
from bit-operation counts.

For a finite set $S$, vectors in $\mathbb Q^S$ have coordinates
indexed by $S$ and are column vectors unless indicated otherwise.
For $U\subseteq S$, the indicator vector $\mathbf1_U\in\{0,1\}^S$
has entries $(\mathbf1_U)_v=\mathds{1}_{\{v\in U\}}$ for $v\in S$.
We write $\vec{0}$ for the zero vector. For $v\in S$, the row
$\delta_v\in\mathbb Q^{1\times S}$ selects coordinate $v$, so
$\delta_vx=x_v$. A vector indexed by $U\subseteq S$ is extended
to $S$ by putting zero in each coordinate of $S\setminus U$.

We write $\vec{X}=(X_1,\ldots,X_n)$ for the vector of formal variables
and use arrows for polynomial coefficient vectors such as
$\vec{P}_{f,v}(T)$. For a coefficient row $\vec{p}=(p_i)_{i\in S}$
and a vector $z=(z_i)_{i\in S}$, we write their scalar pairing as
$\langle\vec{p},z\rangle=\sum_{i\in S}p_i z_i$.
In particular, $\langle\vec{P}_{f,v}(T),\vec{X}\rangle$ is a
scalar linear form in the variables $X_i$.

For a polynomial $P(\vec{X},z)$ in the variables $\vec{X}$ and a variable $z$,
$[z^j]P$ denotes the coefficient of $z^j$, viewed as a polynomial
in $\vec{X}$, and $\deg_{\vec{X}} P$ denotes total degree in $\vec{X}$.
The degree of a row of polynomials is the largest
degree of any entry. Unless otherwise specified, polynomial
coefficients are rational and matrix kernels are taken over
$\mathbb Q$.

\section{Technique overview}\label{sec:technical-overview}
We first count satisfying assignments of a $3$-CNF in which each
variable occurs in at most three clauses. The product of its clause
polynomials has degree at most $3n$, so we can use interpolation to
recover the exact count from sums over small groups of variables.
Section~\ref{subsec:preview-general-sat} then uses disjoint
sparsification and variable copying to count the satisfying assignments
of an arbitrary $k$-CNF in $(n+m)^{O_k(1)}2^{o(n)}$ time for every
fixed $k\ge2$. Taking $k=3$ already refutes ETH.
Section~\ref{subsec:preview-full-case} explains how counting on the
original variables gives the exponent $O_k(\rho(n))$ of
Proposition~\ref{prop:interpolation-bound}.

\subsection{The bounded-occurrence setting}\label{subsec:preview-setting}
Let $F$ have $n$ declared Boolean variables. Each clause contains
at most three literals, and each variable appears in at most
three clauses, counting positive and negative occurrences together.
Our task is to count the satisfying assignments of $F$ exactly.

We remove tautological clauses and repeated literals within a
clause. An empty clause gives count zero immediately.
These operations preserve the occurrence bound. For each remaining
clause $e$, let $I_e\subseteq[n]$ be its variable set.
For each variable that occurs in no clause, add a factor equal to
one with scope $\{v\}$. Such a factor leaves the count unchanged
and ensures that every variable has an assigned position in the
construction. We call these constant-one terms \emph{dummy clauses}.
Let $\mathcal F$ index all clauses, including the dummy clauses. Then
\begin{equation}\label{eq:overview-incidences}
 |I_e|\le3,\qquad
 \#\{e\in\mathcal F:v\in I_e\}\le3,\qquad
 n\le M:=\sum_{e\in\mathcal F}|I_e|\le3n.
\end{equation}
All sums below still range over the original $n$ Boolean variables.

\subsection{A direct polynomial for the count}\label{subsec:preview-encoding}
Write $L_{e,v}(X_v)=X_v$ for a positive literal and
$L_{e,v}(X_v)=1-X_v$ for a negative literal. The satisfaction
polynomial of clause $e$ is
\[
 \Phi_e((X_v)_{v\in I_e})
 =1-\prod_{v\in I_e}(1-L_{e,v}(X_v)).
\]
For example, $x_a\vee\neg x_b\vee x_c$ gives
\[
 \Phi_e(X_a,X_b,X_c)=1-(1-X_a)X_b(1-X_c).
\]
On Boolean inputs this polynomial is one when the clause is
satisfied and zero otherwise. For a dummy clause $e$, put
$\Phi_e=1$. Therefore
\begin{equation}\label{eq:overview-direct-count}
 \#F=\sum_{x\in\{0,1\}^n}\prod_{e\in\mathcal F}
                   \Phi_e((x_v)_{v\in I_e}).
\end{equation}
The product has total degree at most $M\le3n$.
This linear degree bound is the useful consequence of the
three-occurrence assumption.

Equation~\eqref{eq:overview-direct-count} is an exact expression for
the count, but evaluating its $2^n$ summands would be exhaustive search.
To motivate the algorithm, suppose we were given a partition
of the variables into $r$ groups $S_1,\ldots,S_r$ satisfying
both of the following conditions:
\begin{enumerate}
\item Each group contains at most $2n/r$ variables.
\item For every clause, all of its variables belong to a single group.
\end{enumerate}
This is a hypothetical, very restrictive assumption; we do not
assume that the input formula admits such a partition.

Under this assumption, we could count satisfying assignments in
each group independently. Let $N_g$ be the number of assignments
to the variables in $S_g$ that satisfy all clauses in that group.
Any such assignment can be combined with any satisfying assignments
in the other groups, because no clause connects different groups.
Every global satisfying assignment arises in exactly one such way.
Consequently,
\[
 \#F=\prod_{g=1}^r N_g.
\]
Computing each $N_g$ by exhaustive search within its group examines
a total of at most
\[
 \sum_{g=1}^r 2^{|S_g|}\le r\,2^{2n/r}
\]
local assignments, with polynomial work per assignment. For large
$r$, this is much faster than enumerating all $2^n$ global assignments.

We will replace the clause inputs so that different groups interact
only through a small collection of shared linear summaries. Once
the values of those summaries are fixed, we can again sum over
each group separately.

\subsection{A polynomial family with easier evaluation points}
\label{subsec:preview-deformation}
We introduce a parameter $T$. At $T=0$, the replacements must
restore the original clause inputs. At selected nonzero points
$T=1,\ldots,Q$, they should let us separate the groups by fixing
shared linear summaries. Here $Q$ is the number of selected points,
and $R$ will bound the degree of the replacement coefficients.
We choose both parameters later.

Write $\vec{X}=(X_1,\ldots,X_n)$ for the vector of formal variables.
For each occurrence $v\in I_e$, use the polynomial coefficient vector
$\vec{P}_{e,v}(T)=(p_{e,v,1}(T),\ldots,p_{e,v,n}(T))$ to replace
$X_v$ in clause $e$ by the scalar inner product
\[
 \langle \vec{P}_{e,v}(T),\vec{X}\rangle
 =\sum_{i=1}^n p_{e,v,i}(T)X_i.
\]
We call this expression the \emph{replacement linear form} for
the occurrence of variable $v$ in clause $e$. It replaces the
input $X_v$ in the clause polynomial $\Phi_e$.
We require
\[
 \langle \vec{P}_{e,v}(0),\vec{X}\rangle=X_v,
 \qquad \deg \vec{P}_{e,v}\le R.
\]
Different clauses may use different replacement linear forms
for the same variable.
Define
\begin{equation}\label{eq:simple-counting-polynomial}
 H(T)=\sum_{x\in\{0,1\}^n}\prod_{e\in\mathcal F}
       \Phi_e\bigl((\langle \vec{P}_{e,v}(T), x\rangle)_{v\in I_e}\bigr)
       \in\mathbb Q[T].
\end{equation}
At zero every replacement restores the original variable, while
the degree of each clause polynomial grows by at most a factor of $R$. Hence
\begin{equation}\label{eq:overview-value-degree}
 H(0)=\#F,\qquad \deg H\le MR\le3nR.
\end{equation}
We will recover $H(0)$ from Taylor coefficients at $t=1,\ldots,Q$.
The degree bound means that $O(1+nR/Q)$ coefficients per point
suffice, as Section~\ref{subsec:preview-interpolation} explains.
Our goal is therefore to make $R$ small relative to $Q$: many
points with low-degree replacements require fewer coefficients
at each point.

At a nonzero $t$, the value $\langle\vec{P}_{e,v}(t),x\rangle$
of a replacement linear form need not lie in $\{0,1\}$, even
when $x$ is Boolean. The transformed clause polynomials
therefore need not act as satisfaction indicators.

\subsection{Separating the sum by fixing measurements}
\label{subsec:preview-separation}
Fix $t\in[Q]$. We are given the coefficient vectors
$\vec{P}_{e,v}(t)$, whose entries are now constants. We explain
what structure lets us compute $H(t)$ quickly, and how to use it.
Throughout this subsection, write $S_g=S_{t,g}$ and $C_g=C_{t,g}$.

\begin{definition}[$(r,\tau,D)$-design]
\label{def:overview-measurement-structure}
For the given coefficient vectors $\vec{P}_{e,v}(t)$, an
\emph{$(r,\tau,D)$-design at $t$}
consists of groups $S_g$, clause assignments $\sigma_e(t)$,
and measurement matrices $C_g$ satisfying the following four
conditions:
\begin{enumerate}
\item \emph{Small groups.} Partition the variables into disjoint
groups $[n]=S_1\sqcup\cdots\sqcup S_r$, with $|S_g|\le2n/r$.
\item \emph{One assigned group per clause.} Assign each clause
$e$ to one group $\sigma_e(t)\in[r]$. Condition~4 must hold with
this same group for every replacement linear form of clause $e$.
\item \emph{Few bounded measurements.} Each group $g$ has an
integer matrix $C_g$ with columns indexed by $S_g$ and $c_g$ rows.
Each row specifies one linear measurement of the variables in
$S_g$. There are at most $2\tau n$ rows in total, and the sum of
absolute values of the coefficients in each row is at most $D$.
For an assignment $x$, write
\[
 x_g=x|_{S_g},\qquad y_g=C_gx_g,\qquad
 \vec{y}=(y_1,\ldots,y_r).
\]
\item \emph{Dependence on other groups only through measurements.}
Suppose clause $e$ is assigned to group $g=\sigma_e(t)$.
Each replacement linear form of this clause may depend freely on the
variables in $S_g$. Its dependence on any other group $S_h$ must
be a linear combination of that group's measurements $y_h$.
Precisely, for every $v\in I_e$, there must be coefficient vectors
$\vec{\lambda}_{e,v,h}\in\mathbb Q^{c_h}$, for $h\ne g$, such
that, for every $x\in\mathbb Q^n$,
\begin{equation}\label{eq:outline-separation}
 \langle\vec{P}_{e,v}(t),x\rangle
 =\langle\vec{P}_{e,v}(t)|_{S_g},x_g\rangle
   +\sum_{h\ne g}\langle\vec{\lambda}_{e,v,h},y_h\rangle.
\end{equation}
Equivalently, $\vec{P}_{e,v}(t)|_{S_h}$ lies in the row space
of $C_h$ for every $h\ne g$.
\end{enumerate}
\end{definition}
The matrices $C_h$ are shared by all clauses. A clause's assigned
group need not contain its original variables. Once $\vec{y}$
is fixed, however, the entire transformed clause polynomial
depends only on the variables in its assigned group.

\smallskip\noindent
\textbf{The algorithm.}
Given an $(r,\tau,D)$-design at $t$,
first find the coefficient vectors $\vec{\lambda}_{e,v,h}$ by
solving the linear systems guaranteed by condition~4.
For fixed $\vec{y}$, let $\mathcal X_{t,g}(y_g)$ be the assignments
to the variables in $S_g$ whose measurements equal $y_g$:
\[
 \mathcal X_{t,g}(y_g)
 =\{u\in\{0,1\}^{S_g}:C_gu=y_g\}.
\]
For such an assignment $u$, compute the contribution of group $g$
as follows. For each clause $e$ assigned to $g$, first use
\eqref{eq:outline-separation} to compute the values of its
replacement linear forms from $u$ and the fixed measurements.
Next evaluate the clause polynomial $\Phi_e$ on these values.
Finally, multiply the values
obtained from all clauses assigned to $g$. Denote this product
by $A_{t,g}(u;\vec{y})$. No assignments to the other groups are
needed for this calculation.

Each measurement of a Boolean assignment is an integer in
$[-D,D]$. Initialize $Z=0$ and perform the following steps:
\begin{enumerate}
\item Try every measurement tuple
$\vec{y}\in\mathcal Y:=\prod_{g=1}^r\{-D,\ldots,D\}^{c_g}$.
For each tuple, perform steps~2 and~3.
\item For each group $g$, try every Boolean assignment $u$ to its
variables. Keep it only if $C_gu=y_g$. Add the corresponding
products $A_{t,g}(u;\vec{y})$ to obtain the group sum
\[
 B_{t,g}(\vec{y})=
 \sum_{u\in\mathcal X_{t,g}(y_g)}A_{t,g}(u;\vec{y}).
\]
If no assignment satisfies $C_gu=y_g$, set $B_{t,g}(\vec{y})=0$.
\item Multiply the group sums and add the result
$\prod_{g=1}^r B_{t,g}(\vec{y})$ to $Z$.
\end{enumerate}
After all measurement tuples have been processed, return $Z$.

To see why this returns $H(t)$, fix $\vec{y}$ and choose one
assignment from each set $\mathcal X_{t,g}(y_g)$. Since the groups
contain disjoint sets of variables, these choices combine into
one full assignment. Every full assignment with measurements
$\vec{y}$ arises in exactly one such way. Its product of clause
polynomials is the product of the group contributions
$A_{t,g}$. Multiplying out the group sums and then summing over
$\vec{y}$ therefore gives
\begin{equation}\label{eq:outline-separated-sum}
 H(t)=\sum_{\vec{y}\in\mathcal Y}\prod_{g=1}^r
       \left(\sum_{u\in\mathcal X_{t,g}(y_g)}
                         A_{t,g}(u;\vec{y})\right).
\end{equation}
Every Boolean assignment has exactly one measurement tuple, so
this sum counts each assignment's contribution exactly once.

There are at most $(2D+1)^{2\tau n}$ measurement tuples. For each
tuple, the algorithm tries at most
$\sum_g2^{|S_g|}\le r2^{2n/r}$ assignments to individual groups.
Consequently, the running time is
\[
 (2D+1)^{2\tau n}2^{2n/r}
\]
up to polynomial factors. The first factor bounds the number of
measurement tuples; the second bounds the number of assignments
within one group. The algorithm scans one group at a time and
keeps only the current measurement tuple, the current assignment,
and running sums and products; see
Lemma~\ref{lem:measurement-separation}.

For the parameter choices in Section~\ref{subsec:preview-parameters},
we can construct replacement forms of degree at most $R$ that
restore the original variables at zero and admit an
$(r,\tau,D)$-design at every $t\in[Q]$.
Section~\ref{subsec:preview-auxiliary} gives the construction.
We first explain how these properties let us recover the count
efficiently.

\subsection{Recovering the count from Taylor coefficients}
\label{subsec:preview-interpolation}
Our goal is to recover $H(0)=\#F$ from information at the points
$t=1,\ldots,Q$. Since $\deg H\le3nR$, the $Q$ values $H(t)$ alone
may not determine $H$. We instead compute several Taylor
coefficients at each point. Choose
\[
 q=\left\lfloor\frac{3nR}{Q}\right\rfloor,\qquad J=q+1.
\]
Suppose we know the coefficients of $z^0,\ldots,z^q$ in $H(t+z)$
for every $t\in[Q]$. These data determine $H$ uniquely: if two
polynomials of degree at most $3nR$ have the same data, their
difference is divisible by $(T-t)^J$ for every $t\in[Q]$, hence by
$\prod_{t=1}^Q(T-t)^J$. This product has degree $QJ>3nR$, so the
difference must be zero. Each Taylor coefficient gives a linear
equation in the coefficients of $H$. Solving this rational linear
system recovers $H$, and its constant coefficient is the desired
count $H(0)$.

It remains to compute these Taylor coefficients. Fix $t\in[Q]$;
we want $H(t+z)$ through degree $q$ in $z$. The design controls
the replacement forms at $t$, but need not control their changes
from $t$ to $t+z$. We first give those changes a separate input,
so that fixing this input preserves the separation of groups.

\smallskip\noindent
\textbf{Keeping the shifted inputs separate.}
Write
\[
 \Delta\vec P_{e,v}(z)=\vec P_{e,v}(t+z)-\vec P_{e,v}(t).
\]
Keep $x$ as the Boolean assignment being summed over, and introduce
a separate formal vector $\vec X$ for the changes. Define
\begin{equation}\label{eq:outline-taylor-product}
 \mathcal G_x(\vec X,z)=
 \prod_{e\in\mathcal F}\Phi_e\bigl(
       (\langle\vec P_{e,v}(t),x\rangle+
        \langle\Delta\vec P_{e,v}(z),\vec X\rangle)_{v\in I_e}\bigr).
\end{equation}
Here $x$ indexes the polynomial, while $\vec X$ and $z$ are its
formal variables. Setting $\vec X=x$ restores each shifted input
$\langle\vec P_{e,v}(t+z),x\rangle$, so
\[
 H(t+z)=\sum_{x\in\{0,1\}^n}\mathcal G_x(x,z).
\]
On the other hand, fixing $\vec X=\mathbf1_U$ for some
$U\subseteq[n]$ makes every correction
$\langle\Delta\vec P_{e,v}(z),\mathbf1_U\rangle$ independent of $x$.
All dependence on $x$ then remains through
$\langle\vec P_{e,v}(t),x\rangle$, where the design applies.
Our task is therefore to recover the sum with $\vec X=x$
from sums with $\vec X$ fixed.

The degree bound makes this possible with few fixed substitutions.
Every entry of $\Delta\vec P_{e,v}(z)$ is divisible by $z$, so
each occurrence of an $X_i$ in an expanded term contributes at
least one factor of $z$. Thus
\[
 \deg_{\vec X}([z^j]\mathcal G_x(\vec X,z))\le j.
\]
Thus, after discarding powers of $z$ above $q$, every monomial
involves at most $q$ distinct variables from $\vec X$.

\smallskip\noindent
\textbf{Recovering the shifted sum by inclusion--exclusion.}
Work modulo $z^J$, so that only the coefficients through $z^q$
are retained. Replace every positive power of $X_i$ in
$\mathcal G_x$ by $X_i$. This preserves its values on Boolean
inputs. The degree bound above gives, for Boolean $\vec X$,
\[
 \mathcal G_x(\vec X,z)\equiv
 \sum_{\substack{E\subseteq[n]\\|E|\le q}}
       a_E(x,z)\prod_{i\in E}X_i\pmod{z^J},
\]
where $a_E(x,z)$ is the coefficient of the indicated monomial
after this replacement. Evaluating at $\mathbf1_U$, the vector
with ones precisely in $U$, sums the coefficients indexed by
subsets of $U$. Inclusion--exclusion extracts each one:
\[
 a_E(x,z)\equiv
 \sum_{U\subseteq E}(-1)^{|E|-|U|}
                 \mathcal G_x(\mathbf1_U,z)\pmod{z^J}.
\]
When we set $\vec X=x$, the monomial $\prod_{i\in E}x_i$
equals one exactly when all the bits in $E$ are one.
Its contribution to the sum over $x$ is therefore
$\sum_{x:\,x_i=1\ (i\in E)}a_E(x,z)$, with $x$ Boolean.
Substituting the coefficient formula above reduces this to sums
with the formal input fixed.

\smallskip\noindent
\textbf{Computing the restricted sums.}
For $U\subseteq E\subseteq[n]$ with $|E|\le q$, define
\begin{equation}\label{eq:outline-restricted-taylor-sum}
 \mathcal Z_{t,E,U}(z)=
 \sum_{\substack{x\in\{0,1\}^n\\x_i=1\ (i\in E)}}
                    \mathcal G_x(\mathbf1_U,z)
       \quad\text{in }\mathbb Q[z]/(z^J).
\end{equation}
Here $U$ fixes the formal input $\vec X=\mathbf1_U$, while $E$
fixes bits of the summation variable $x$ to one.
Summing the monomial contributions gives
\begin{equation}\label{eq:outline-taylor-recovery}
 H(t+z)\equiv
 \sum_{\substack{E\subseteq[n]\\|E|\le q}}
       \sum_{U\subseteq E}(-1)^{|E|-|U|}
                         \mathcal Z_{t,E,U}(z)\pmod{z^J}.
\end{equation}
This recovers all $J=q+1$ Taylor coefficients together.
Lemma~\ref{lem:boolean-differences} states the general identity
used here.

Each sum $\mathcal Z_{t,E,U}$ can be evaluated by the algorithm
of Section~\ref{subsec:preview-separation}. With
$\vec X=\mathbf1_U$ fixed, each correction
$\langle\Delta\vec P_{e,v}(z),\mathbf1_U\rangle$ is independent of $x$.
All dependence on $x$ comes through the forms
$\langle\vec P_{e,v}(t),x\rangle$, so fixing $\vec y$ still separates
the clause polynomials. The restrictions $x_i=1$ are local to each
group. The separation identity uses only addition, multiplication,
and distributivity, so it also applies to these truncated polynomial
values. Each clause is evaluated after substituting
$\vec X=\mathbf1_U$, using only univariate polynomials in $z$
of degree less than $J$ and discarding higher powers after each
multiplication. The multivariate expansion and its coefficients
$a_E(x,z)$ are used only to justify the identity; the algorithm
never constructs them.

Repeating this calculation at $t=1,\ldots,Q$ provides all the
Taylor coefficients needed for the interpolation above, and
therefore recovers $H(0)=\#F$.

\subsection{The three costs and the running time}
\label{subsec:preview-parameters}
Jumping ahead, Section~\ref{subsec:preview-auxiliary} will construct
replacement forms that restore the original variables at zero,
have degree at most $R$, and admit an $(r,\tau,D)$-design at every
$t\in[Q]$. For sufficiently large $n$, the construction takes
polynomial time and achieves the following parameter bounds:
\begin{equation}\label{eq:overview-parameter-bounds}
 \begin{aligned}
 r&=\Theta\!\left(\frac{\sqrt{\log n}}{(\log\log n)^2}\right),
 &Q&=\Theta\!\left(\frac{\log n}{\log\log n}\right),\\
 R&=\Theta(\sqrt{\log n}),
 &\tau&=\Theta\!\left(\frac1{r\log n}\right),\qquad
 D=r^{2Q}\le(2n)^{1/128}.
 \end{aligned}
\end{equation}
We first show how these bounds give a fast counting algorithm;
the next subsection will justify that they can all be achieved
simultaneously.

Recall that $q=J-1=\lfloor3nR/Q\rfloor$. For each evaluation
point $t$, Section~\ref{subsec:preview-interpolation} computes one
restricted sum for each pair $U\subseteq E$ with $|E|\le q$.
There are $\binom nj$ choices of an $E$ of size $j$, and then
$2^j$ choices of $U$. Each restricted sum enumerates measurement
tuples and assignments within individual groups. Thus the three
costs multiply to give, up to polynomial factors,
\begin{equation}\label{eq:overview-three-costs}
 \underbrace{\sum_{j=0}^{\min(q,n)}2^j\binom nj}_{\text{Taylor data}}
 \ \cdot\
 \underbrace{(2D+1)^{2\tau n}}_{\text{measurements}}
 \ \cdot\
 \underbrace{2^{2n/r}}_{\text{one group}}.
\end{equation}
To bound the first cost, note that $1\le q\le n/2$ for
sufficiently large $n$, since $R/Q\to0$. Using
$\binom nj\le(en/j)^j$ and the fact that $(2en/j)^j$ increases
for $1\le j\le n$, we obtain
\[
 \sum_{j=0}^q2^j\binom nj
 \le(q+1)\left(\frac{2en}{q}\right)^q.
\]
Since $q=\Theta(nR/Q)$, the logarithm of this cost is
$O(n(R/Q)\log(2Q/R))$. Taking logarithms of all three costs in
\eqref{eq:overview-three-costs} therefore gives
\[
 O\!\left(n\left[
       \frac RQ\log\frac{2Q}{R}
       +\tau\log(2D+1)+\frac1r\right]\right).
\]
Each term is small under \eqref{eq:overview-parameter-bounds}:
\[
 \begin{aligned}
 \frac RQ\log\frac{2Q}{R}
   &=O\!\left(\frac{\log\log n}{\sqrt{\log n}}
                      \cdot\log\log n\right),\\
 \tau\log(2D+1)&=O\!\left(\frac1{r\log n}\cdot\log n\right)
                  =O(1/r),\\
 \frac1r&=O\!\left(\frac{(\log\log n)^2}{\sqrt{\log n}}\right).
 \end{aligned}
\]
Thus the bounded-occurrence instance can be counted in
\begin{equation}\label{eq:overview-bounded-time}
 n^{O(1)}2^{O(n(\log\log n)^2/\sqrt{\log n})}
\end{equation}
bit operations and polynomial space. The finitely many smaller
inputs are handled by exhaustive search.

The number of points $Q$, the number of groups $r$, and the
truncation order $J=O(1+nR/Q)$ are polynomial in $n$. Hence the
loops over points and groups, arithmetic on polynomials of degree
less than $J$, and the final interpolation add only polynomially
many operations per iteration of the three enumerations above.

For the bit-complexity and space bounds, see
Appendix~\ref{subsec:overview-arithmetic}.

\subsection{Constructing the low-degree replacement linear forms}
\label{subsec:preview-auxiliary}
Consider one occurrence of $X_v$ in a clause. At $T=0$ its
replacement must equal $X_v$. At each $t=1,\ldots,Q$, the clause
must be able to evaluate that same replacement using only its
assigned group and a few shared measurements. Choosing a different
linear form at each point and interpolating would generally cost
degree $Q$. To keep Taylor recovery cheap, we need degree $R$
much smaller than $Q$.

Suppose a term in the replacement uses a variable outside the
clause's assigned group only at $t=2$. Multiplying the term by
$1-T/2$ leaves it unchanged at zero and removes it at $t=2$.
At every other evaluation point the clause can read the variable
from its own group. The same trick works for several such points:
one factor per point, at a cost of one degree each. The challenge
is therefore to write each input as a sum in which the shared
measurements determine one part, and each remaining term uses a
variable outside the assigned group at only a few points. We first
construct such a decomposition on auxiliary coordinates that record
the group choices, then substitute the variables of the formula.

\medskip\noindent
\textbf{Step 1: Set up the auxiliary coordinates.}\par\nobreak
\smallskip\noindent
At each evaluation point, an occurrence $(e,v)$ has two group
choices: the group containing variable $v$, and the group assigned
to clause $e$. Across the $Q$ points, these choices form a
sequence of $Q$ pairs. We therefore use the coordinate set
\[
 \mathcal B=([r]\times[r])^Q,\qquad D=|\mathcal B|=r^{2Q}.
\]
Write an index as
\[
 u=\bigl((a_u(1),d_u(1)),\ldots,(a_u(Q),d_u(Q))\bigr).
\]
We will construct one replacement row for every such index,
so it will be available whatever group choices we later make
for the formula.

Let $\vec\zeta=(\zeta_w)_{w\in\mathcal B}$ be formal placeholders
for the original variables that we will insert in Step~4.
At point $t$, coordinate $\zeta_w$ belongs to group $a_w(t)$,
whereas the replacement for $\zeta_u$ is assigned to group $d_u(t)$.
Thus the coordinates that this replacement may use freely are
\[
 \mathcal S_{t,d_u(t)},\qquad
 \mathcal S_{t,g}:=\{w\in\mathcal B:a_w(t)=g\}.
\]
In particular, $\zeta_w$ belongs to the assigned group exactly
when $a_w(t)=d_u(t)$. The sets $\mathcal S_{t,g}$ partition
$\mathcal B$, with $D/r$ coordinates in each group.

Our auxiliary goal is to construct coefficient rows
$\vec P_u(T)\in\mathbb Q[T]^D$ and one matrix
\[
 C\in\{0,1,-1\}^{c\times D},\qquad c\le\frac{D\tau}{3r},
\]
such that
\[
 \langle\vec P_u(0),\vec\zeta\rangle=\zeta_u,
 \qquad \deg\vec P_u\le R-1,
\]
and, at every $t\in[Q]$, the replacement linear form
$\langle\vec P_u(t),\vec\zeta\rangle$ is a linear combination
of the available data
\begin{equation}\label{eq:overview-auxiliary-requirement}
 \vec\zeta|_{\mathcal S_{t,d_u(t)}}\quad\text{and}\quad C\vec\zeta.
\end{equation}
The same measurements $C\vec\zeta$ serve every row and every
evaluation point. This is the auxiliary counterpart of the
dependence condition in the design from
Section~\ref{subsec:preview-separation}.

\medskip\noindent
\textbf{Step 2: Construct the constant matrix.}\par\nobreak
\smallskip\noindent
We start from the identity
\[
 \zeta_u=((I_D-M_0)\vec\zeta)_u+
                   \sum_{w\in\mathcal B}M_0[u,w]\zeta_w.
\]
We want the first term to be determined by $C\vec\zeta$.
In the sum, each nonzero coefficient should connect incompatible
groups at only a few points, so that a low-degree polynomial
can remove those dependencies. Define these points by
\[
 E_{u,w}=\{t\in[Q]:a_w(t)\ne d_u(t)\}.
\]
The two requirements on $M_0\in\mathbb Q^{D\times D}$ are
\begin{equation}\label{eq:outline-matrix-conditions}
 \begin{gathered}
 M_0\vec\xi=\vec\xi\quad\text{for every }\vec\xi\in\ker C,\\
 M_0[u,w]\ne0\quad\Longrightarrow\quad |E_{u,w}|\le R-1.
 \end{gathered}
\end{equation}
The first says that $I_D-M_0$ vanishes on $\ker C$. Equivalently,
each of its rows lies in the row space of $C$, so
$(I_D-M_0)\vec\zeta$ is a linear function of the measurements
$C\vec\zeta$. The second will bound the degrees of the polynomials
used in Step~3.

\smallskip\noindent
\emph{Restricting the support by keeping $f$ low-degree.}
Let $\Pi_s$ be the permutation matrix that
swaps the two entries of pair $s$ in every index, leaving all
other pairs unchanged. These matrices commute and satisfy
$\Pi_s^2=I_D$. Put
\[
 V_0=\prod_{s=1}^Q\Pi_s,\qquad
 W_0=\frac12\sum_{s=1}^Q(I_D-\Pi_s),\qquad
 M_0=V_0f(W_0),
\]
where we will choose a polynomial $f$ of degree at most $R-1$.
The complete swap $V_0$ already respects every group: its
nonzero entry in row $u$ is at the column $w$ satisfying
\[
 (a_w(s),d_w(s))=(d_u(s),a_u(s))\quad\text{for every }s.
\]
In particular, $E_{u,w}$ is empty.

Multiplying by $f(W_0)$ can undo swaps, but the degree of $f$
limits how many. Expanding $f(W_0)$ gives products of at most
$R-1$ swaps. Repeated swaps cancel because $\Pi_s^2=I_D$.
Multiplying by $V_0$ therefore gives
\begin{equation}\label{eq:overview-partial-swaps}
 M_0=\sum_{\substack{S\subseteq[Q]\\|S|\le R-1}}
             \gamma_S\prod_{s\notin S}\Pi_s
 \qquad\text{for some }\gamma_S\in\mathbb Q.
\end{equation}
The permutation in the summand indexed by $S$ swaps every pair
outside $S$. Its nonzero entries therefore satisfy
$a_w(s)=d_u(s)$ for every $s\notin S$, so $E_{u,w}\subseteq S$.
Every summand is zero whenever $|E_{u,w}|>R-1$, and hence so is
their sum. This proves the second condition in
\eqref{eq:outline-matrix-conditions} for any polynomial $f$ of
degree at most $R-1$.

\smallskip\noindent
\emph{Choosing $f$ to fix most basis directions.}
We now choose $f$ so that $M_0$ fixes most basis directions.
First consider one position, with coordinates indexed by
$[r]\times[r]$. Let $\vec e_{ab}$ be the vector that is one
at $(a,b)$ and zero elsewhere. Swapping the pair has the
orthogonal eigenbasis
\[
 \begin{array}{ll}
 \vec e_{aa}\quad(a\in[r]),\quad
 \vec e_{ab}+\vec e_{ba}\quad(a<b),
     &\text{eigenvalue }+1,\\[2pt]
 \vec e_{ab}-\vec e_{ba}\quad(a<b),
     &\text{eigenvalue }-1.
 \end{array}
\]
There are $r(r+1)/2$ vectors with eigenvalue $+1$ and
$r(r-1)/2$ with eigenvalue $-1$. All entries are in $\{0,1,-1\}$.

For each position $s\in[Q]$, choose one such vector $\vec\psi_s$,
and define $\vec\psi\in\mathbb Q^{\mathcal B}$ coordinatewise by
\[
 \psi_u=\prod_{s=1}^Q\psi_s(a_u(s),d_u(s)).
\]
These $D=(r^2)^Q$ choices give an orthogonal basis: inner products
factor into the inner products at the $Q$ positions.
The swap $\Pi_s$ acts on $\vec\psi$ by the eigenvalue of
$\vec\psi_s$. If exactly $j$ of the choices have eigenvalue $-1$,
then
\[
 W_0\vec\psi=j\vec\psi,\qquad
 V_0\vec\psi=(-1)^j\vec\psi,\qquad
 M_0\vec\psi=(-1)^jf(j)\vec\psi.
\]
Thus we make $M_0$ fix these vectors by setting $f(j)=(-1)^j$.

For a uniformly chosen basis vector, the number $j$ has distribution
\[
 W\sim\operatorname{Bin}(Q,p),\qquad p=\frac{r-1}{2r},
\]
because at each position a fraction $p$ of the $r^2$ choices have
eigenvalue $-1$. Most basis vectors therefore have $j$ near $Qp$.
Choose an interval $\mathcal I$ of $R$ consecutive integers near
$Qp$, and interpolate $f(j)=(-1)^j$ for $j\in\mathcal I$.
This gives $\deg f\le R-1$ and makes $M_0$ fix every basis
vector with $j\in\mathcal I$. Step~5 specifies the endpoints
and checks that the interval lies in $\{0,\ldots,Q\}$.

\smallskip\noindent
\emph{Measuring the exceptional directions.}
Use the transposes of the remaining basis vectors as the rows of
$C$. Their entries are in $\{0,1,-1\}$, and by orthogonality,
$\ker C$ is spanned by the basis vectors fixed above.
This proves the first condition in
\eqref{eq:outline-matrix-conditions}.

We can now see how to choose $R$. The standard deviation of $W$ is
$\sqrt{Qp(1-p)}=\Theta(\sqrt Q)$. Taking $R$ much larger than
$\sqrt Q$ puts most basis vectors inside the interval, so only a
small fraction need to be measured. We can still take $R$ much
smaller than $Q$, so that Taylor recovery needs only
$1+\lfloor 3nR/Q\rfloor=o(n)$ coefficients per point.
For the choices in Step~5, the binomial tail bound gives
\[
 c=D\Pr[W\notin\mathcal I]
      \le 2D\exp\!\left(-\frac{R^2}{8Q}\right)
      \le\frac{D\tau}{3r},
\]
as required. Thus low degree gives restricted support, while
interpolation makes the correction $I_D-M_0$ depend on only
these few measurements.

\medskip\noindent
\textbf{Step 3: Define the auxiliary replacement rows.}\par\nobreak
\smallskip\noindent
We now turn the decomposition of $\zeta_u$ from Step~2 into its
replacement. Keep the term determined by measurements unchanged.
For each $M_0[u,w]\ne0$, multiply its coefficient in the other
term by
\[
 \varphi_{u,w}(T)=\prod_{s\in E_{u,w}}(1-T/s).
\]
This polynomial equals one at zero and vanishes at every point
where $\zeta_w$ lies outside the assigned group. Define the
coefficient row $\vec P_u(T)$ by the identity
\begin{equation}\label{eq:outline-auxiliary-row}
 \langle\vec P_u(T),\vec\zeta\rangle
 =((I_D-M_0)\vec\zeta)_u+
   \sum_{\substack{w\in\mathcal B\\M_0[u,w]\ne0}}
                M_0[u,w]\varphi_{u,w}(T)\zeta_w.
\end{equation}
This directly gives all three required properties:
\begin{itemize}
\item At $T=0$, every multiplier is one, so the two terms sum to
$\zeta_u$.
\item Each multiplier has degree $|E_{u,w}|\le R-1$, so
$\deg\vec P_u\le R-1$.
\item At $T=t$, the first term is a linear function of $C\vec\zeta$.
In the sum, a coefficient can survive only if
$a_w(t)=d_u(t)$, so only coordinates in
$\mathcal S_{t,d_u(t)}$ remain.
\end{itemize}
Thus the replacement uses exactly the kinds of data allowed in
\eqref{eq:overview-auxiliary-requirement}.

\medskip\noindent
\textbf{Step 4: Substitute the original variables.}\par\nobreak
\smallskip\noindent
The auxiliary rows are now constructed. To use them for the
formula, choose schedules
\[
 a_v\in[r]^Q\quad(v\in[n]),\qquad
 d_e\in[r]^Q\quad(e\in\mathcal F).
\]
At point $t$, put variable $v$ in group $a_v(t)$ and assign
clause $e$ to group $d_e(t)$:
\[
 S_{t,g}=\{v:a_v(t)=g\},\qquad \sigma_e(t)=d_e(t).
\]
The occurrence $(e,v)$ uses the auxiliary label
\[
 u(e,v)=\bigl((a_v(s),d_e(s))\bigr)_{s\in[Q]}\in\mathcal B.
\]
Let $h$ be the largest number of occurrences receiving any one
label. We need both small variable groups and small $h$.
For our three-occurrence, width-three formula,
Lemma~\ref{lem:incidence-labels} chooses the schedules
deterministically in polynomial time so that
\[
 |S_{t,g}|\le2n/r,\qquad h\le2M/D,
\]
provided
\begin{equation}\label{eq:overview-balance-requirements}
 12D^2\le M,\qquad 2Qr^2\le n.
\end{equation}
The idea is to derandomize a random choice of schedules. If all
$a_v$ and $d_e$ are chosen independently and uniformly from
$[r]^Q$, each label has expected multiplicity $M/D$, and each
group $S_{t,g}$ has expected size $n/r$. Under the assumptions
in \eqref{eq:overview-balance-requirements}, the standard method
of conditional expectations derandomizes this choice in polynomial
time, ensuring that every label has multiplicity at most $2M/D$
and every group has size at most $2n/r$. Step~5 verifies these
assumptions for our parameter choices.

Different occurrences can receive the same label while requiring
different original variables at that coordinate. Use $h$ copies
of $\mathcal B$, placing occurrences with the same label in
different copies. Let $j(e,v)\in[h]$ denote the copy used by
$(e,v)$; put $X_v$ at its coordinate $u(e,v)$ and zero in unused
positions. Write $\vec\zeta^{(j)}(\vec X)$ for the resulting filled
vector in copy $j$. Every entry is zero or an original variable.
Repeated appearances of $X_v$ use the same value, so these copies
introduce no new Boolean variables.

Apply the auxiliary row to the copy containing the occurrence:
\begin{equation}\label{eq:overview-transferred-row}
 \langle\vec P_{e,v}(T),\vec X\rangle
 =\left\langle\vec P_{u(e,v)}(T),
                  \vec\zeta^{(j(e,v))}(\vec X)\right\rangle.
\end{equation}
At zero the right side reads the coordinate containing $X_v$,
and substituting variables preserves the degree bound $R-1$.
At point $t$, its freely used coordinates contain only variables
$v'$ with $a_{v'}(t)=d_e(t)$. These are precisely the variables
in the clause's assigned group $S_{t,d_e(t)}$.
All occurrences of clause $e$ use this same assigned group.

The remaining dependence is through the $hc$ linear measurements
$C\vec\zeta^{(j)}(\vec X)$, over the $h$ copies. These may involve
several original groups. Fixing a total such as $x_1+x_2$ would
still couple two groups containing $x_1$ and $x_2$. We therefore
split each measurement into its contributions from individual
groups. For each measurement $\ell(\vec X)$, write
\[
 \ell(\vec X)=\sum_{g=1}^r
        \ell|_{S_{t,g}}(\vec X|_{S_{t,g}}),
\]
and collect the coefficient rows of these restrictions into
$C_{t,g}$. Every auxiliary measurement is now a sum of group
measurements. For a clause assigned to group $g$, the part from
$S_{t,g}$ is a local linear form, and every other part is a linear
combination of the corresponding group's measurements.
This is the condition in \eqref{eq:outline-separation}.

There are $rhc$ rows in total. Since $hD\le2M\le6n$,
\[
 \sum_{g=1}^r c_{t,g}
 =rhc\le rh\frac{D\tau}{3r}\le2\tau n.
\]
Each row of $C$ has $D$ entries in $\{0,1,-1\}$. Substituting
variables, combining repeated copies, and restricting to a group
cannot increase the sum of absolute coefficients. Hence every
row of $C_{t,g}$ is integral with absolute coefficient sum at most
$D$. Together with the group-size bound, this proves that the
replacement forms admit an $(r,\tau,D)$-design at every point.

\medskip\noindent
\textbf{Step 5: Verify the promised parameter bounds.}\par\nobreak
\smallskip\noindent
The construction needs the two balancing inequalities
\eqref{eq:overview-balance-requirements} and the tail bound
$2e^{-R^2/(8Q)}\le\tau/(3r)$. We now choose parameters of the orders
stated in \eqref{eq:overview-parameter-bounds} and verify these requirements.

Put $\lambda=\lceil\log_2 n\rceil$ and
$\nu=\lceil\log_2\lambda\rceil$, and choose
\begin{equation}\label{eq:overview-explicit-parameters}
 \begin{aligned}
 r&=\left\lfloor\frac{\sqrt\lambda}{\nu^2}\right\rfloor,
 &Q&=\left\lfloor\frac{\lambda}{128\nu}\right\rfloor,
 &R&=4\lceil\sqrt\lambda\rceil,\\
 \tau&=\frac1{r\lambda},
 &D&=r^{2Q}.
 \end{aligned}
\end{equation}
These have the orders stated in \eqref{eq:overview-parameter-bounds}.
For sufficiently large $n$, we have $r\ge2$, $R\ge32$, and
$6R\le Q$, since $R/Q=O(\nu/\sqrt\lambda)\to0$. We check
the remaining requirements in turn:
\begin{itemize}
\item \emph{Interpolation interval.}
With $p=(r-1)/(2r)$ as in Step~2, take
\[
 A_0=\left\lfloor Qp-\frac{R-1}{2}\right\rfloor,\qquad
 \mathcal I=\{A_0,\ldots,A_0+R-1\}.
\]
Since $Q/4\le Qp\le Q/2$ and $6R\le Q$, this interval lies
in $\{0,\ldots,Q\}$. Moreover, $R\ge32$ ensures that it
contains every integer within $R/4$ of $Qp$. The binomial tail
bound therefore gives the estimate
$\Pr[W\notin\mathcal I]\le2e^{-R^2/(8Q)}$ used in Step~2.
\item \emph{Polynomial dimension and balanced schedules.}
Since $\log_2 r\le\nu/2$,
\[
 \log_2 D=2Q\log_2 r\le\lambda/128,\qquad
 D\le(2n)^{1/128}.
\]
For sufficiently large $n$, this gives
\[
 12D^2\le12(2n)^{1/64}\le n\le M,\qquad
 2Qr^2=O(\lambda^2)\le n,
\]
as required for Step~4.
\item \emph{Few measurements.}
We have $R^2/(8Q)\ge256\nu$. Since $\lambda\le2^\nu$ and
$r^2\le\lambda$,
\[
 2e^{-R^2/(8Q)}\le2e^{-256\nu}
 \le\frac1{3\lambda^2}
 \le\frac1{3r^2\lambda}=\frac{\tau}{3r}.
\]
Thus Step~2 supplies the auxiliary measurement bound used
in Step~4.
\end{itemize}

Finally, all construction dimensions are polynomially bounded in
$n$. Lemma~\ref{lem:row-coefficients} gives polynomial construction
time for the matrices and rows in Steps~2--3, and
Lemma~\ref{lem:incidence-labels} does so for the schedules in
Step~4. The transfer uses only $hD\le6n$ coordinate positions.
We have therefore constructed, in polynomial time, replacement
forms that restore every original input at zero, have degree at
most $R-1\le R$, and admit the promised $(r,\tau,D)$-designs
at every $t\in[Q]$. This supplies the bounds used in
Section~\ref{subsec:preview-parameters};
Lemma~\ref{lem:incidence-parameters} records the parameter check
for the more general setting of the full proof.

\subsection{A weaker algorithm for general \texorpdfstring{$\#k$-SAT}{\#k-SAT}}
\label{subsec:preview-general-sat}
The algorithm above already gives a subexponential algorithm for
general $\#k$-SAT: after disjoint sparsification, we reduce each
instance directly to a $3$-CNF in which every variable occurs at
most three times. Both steps preserve the count, as follows.

Fix $k\ge2$. We use the counting-preserving version~\cite[Appendix~A]{DHMTW}
of sparsification~\cite{IPZ}, with quantitative bounds
from~\cite[Section~6]{CIP} and
\cite[Lemma~5.14 and equation~(5.4)]{CalabroThesis}.
As recorded in Lemma~\ref{lem:sparsify}, this expresses the input count as the sum of
the counts of at most
$\operatorname{poly}_k(n,\sigma^{-1})2^{\sigma n}$ formulas $G$.
Each $G$ has the same $n$ declared variables, with at most
\[
 B=O_k\!\left((\sigma^{-1}\log(2/\sigma))^{k-1}\right)
\]
occurrences per variable, and hence at most $Bn$ nonempty clauses.
An empty clause gives count zero immediately.

First turn $G$ into a $3$-CNF without changing its count. Keep
clauses of size at most three. For each longer clause, compute its
disjunction with binary OR gates and require the final output to
be one. For a gate $z=u\vee v$, impose
\[
 (\neg u\vee z)\ \wedge\ (\neg v\vee z)\ \wedge\
 (u\vee v\vee\neg z).
\]
Here $u,v$ are input literals or earlier gate outputs, and $z$ is
fresh. These clauses enforce equality with the OR, so the gate
values are uniquely determined by the original assignment.
Consequently, a satisfying assignment of $G$ has exactly one
extension to the new formula, and an assignment not satisfying
$G$ has none. This uses $O(k)$ gates per clause.

Next reduce the occurrences. If a variable $x$ occurs $s\ge2$
times in this $3$-CNF, replace its occurrences by distinct copies
$x_1,\ldots,x_s$, preserving their signs, and add Tovey's implication
cycle~\cite[p.~86]{Tov84}:
\[
 (\neg x_1\vee x_2)\ \wedge\cdots\wedge\
 (\neg x_{s-1}\vee x_s)\ \wedge\ (\neg x_s\vee x_1).
\]
The cycle forces all copies to agree. Each copy appears in one
clause inherited from the $3$-CNF and two cycle clauses, hence
in exactly three clauses. Variables with at most one occurrence
are kept unchanged, including unused declared variables.
This standard variable-copy reduction~\cite[Proposition~4.7]{Gol08}
therefore also gives a bijection between satisfying assignments.
The final formula $\widehat G$ has $\#\widehat G=\#G$ and
\[
 n\le N:=\#\{\text{variables of }\widehat G\}=O_k(Bn).
\]
All its clauses have size at most three, including the two-literal
cycle clauses, and every variable occurs at most three times.
Thus it is exactly an instance of the setting of this overview.

Apply \eqref{eq:overview-bounded-time} to each $\widehat G$ and add
the counts. When $\sigma^{-1}$ is bounded by a fixed power of
$\log n$, so is $B$, and the resulting time is
\[
 (n+m)^{O_k(1)}
 2^{O_k\!\left(\sigma n+
          Bn(\log\log n)^2/\sqrt{\log n}\right)}.
\]
For example, choosing $\sigma$ within a constant factor of
$(\log n)^{-1/(2k)}$ yields
\[
 (n+m)^{O_k(1)}
 2^{O_k\!\left(n(\log\log n)^{k+1}/(\log n)^{1/(2k)}\right)}
   = (n+m)^{O_k(1)}2^{o(n)}
\]
with polynomial space, processing the sparsification tree and
the reduced instances one at a time. The parameter $\sigma$ may
be chosen rational.

\subsection{A faster algorithm for \texorpdfstring{$\#k$-SAT}{\#k-SAT} via counting solutions to sparse low-degree polynomial equations over \texorpdfstring{$\mathbb F_2$}{F\_2}}
\label{subsec:preview-full-case}

The running-time exponent in Section~\ref{subsec:preview-general-sat}
is $O_k(\sigma n+B\rho(n))$, where
$\rho(n)=n(\log\log n)^2/\sqrt{\log n}$. If sparsification gave
$B=O_k(1)$ at $\sigma=\Theta(\rho(n)/n)$, we would already have a
$2^{O_k(\rho(n))}$-time algorithm for general $\#k$-SAT up to
polynomial factors: copying would use only $O_k(n)$ variables per
leaf, and the number of leaves would fit within the same bound.
At this choice of $\sigma$, however, the guarantee is only
$B=(\log n)^{O_k(1)}$.

We obtain the $2^{O_k(\rho(n))}$ bound in two steps. First, the counting
algorithm of this overview extends to systems of $O(n)$ polynomial
equations over $\mathbb F_2$, each of degree at most $k$ with
polylogarithmically many monomials
(Theorem~\ref{thm:overview-sparse-polynomials}). Second, even if a
leaf $G$ has $Bn$ clauses, we can construct such a system on the
original $n$ variables whose common zeros are exactly the satisfying
assignments of $G$. We illustrate the reduction first with a
self-contained randomized construction, then explain the counting
algorithm.

\medskip\noindent
\textbf{A randomized reduction to sparse polynomial equations.}
Write $v_e(x)=1$ if $x$ violates clause $e$, and $0$ otherwise. A
\emph{parity test} on a set $S$ of clauses is the polynomial equation
$\sum_{e\in S}v_e(x)=0$ over $\mathbb F_2$: it accepts if $x$ violates
an even number of clauses in $S$. Every satisfying assignment passes,
so we need only catch every nonsatisfying one. If $G$ has $m_G\le n$
clauses, one test per clause suffices. Suppose $m_G>n$.

A short test can easily miss a single violated clause, but all
assignments that violate only that clause give identical answers.
Thus there are only $m_G$ singleton patterns to catch. Use $8n$
independent tests. For each, draw $L=2B\lceil\log_2(2m_G)\rceil$
clauses uniformly with replacement. For each draw, independently add
its violation bit to the parity sum with probability $1/2$; two
included copies cancel. Since $m_G\le Bn$, each clause is drawn
at least logarithmically often in expectation overall. For a fixed
set of $w\ge1$ violated clauses, let $u=Lw/m_G$ be the expected number
of hits per test. If the sample hits the set, the coin on the first
hit makes the parity odd with probability $1/2$, even with all other
coins fixed. Thus the rejection probability is
\[
 p_w=\tfrac12\bigl(1-(1-w/m_G)^L\bigr)\ge\tfrac12(1-e^{-u}).
\]

We count \emph{sets} for few violations and \emph{assignments} for many:
\begin{itemize}
\item If $u\le1$, then $p_w\ge u/4$. There are at most $m_G^w$ sets
of size $w$, so the chance that at least one escapes all tests is
at most $m_G^w e^{-8np_w}\le m_G^w e^{-2nLw/m_G}\le16^{-w}$.
Summing over $w\ge1$ gives failure probability at most $1/15$.
\item If $u>1$, then $p_w>1/4$. A union bound over the $2^n$
assignments bounds the chance that any assignment in this case
escapes by $2^n(3/4)^{8n}<1/4$.
\end{itemize}
Thus with probability greater than $2/3$, the common zeros are
exactly the satisfying assignments of $G$. Each $v_e$ is a product
of at most $k$ factors of the form $x_j$ or $1+x_j$, so each test has degree at
most $k$ and at most $2^kL$ monomials, polylogarithmic in $n$.
Section~\ref{sec:hashes} constructs short tests with the same
solution set deterministically.
We first use parity checks from an expander code to ensure that any
nonsatisfying assignment still passing must violate many clauses.
A random short test then catches each such assignment with probability
at least $1/4$. For each candidate test, we count
the assignments that pass both that test and all tests chosen so far.
We append a candidate that minimizes this count: every satisfying assignment
passes every candidate, so this eliminates at least a quarter of the
remaining nonsatisfying assignments.

\medskip\noindent
\textbf{Counting the common zeros.}
Recall from Section~\ref{subsec:preview-encoding} that $\Phi_e(x)$ is
$1$ if $x$ satisfies clause $e$ and $0$ otherwise. What should replace
this factor when we test a whole set $S_i$ of clauses at once? First
count how many clauses in \emph{this test} are violated, using ordinary
integer addition:
\[
 L_i(x)=\sum_{e\in S_i}v_e(x)=\sum_{e\in S_i}\bigl(1-\Phi_e(x)\bigr).
\]
The test passes exactly when $L_i(x)$ is even. Choose $\ell=n+1$, so
that a count of at most $2^n$ is determined by its residue modulo
$2^\ell$. The complemented Beigel--Tarui polynomial $p_\ell$
(Lemma~\ref{lem:rational-idempotent}) is $1$ modulo $2^\ell$ on even
integers and $0$ on odd integers. For example, violating two clauses
in $S_i$ still passes the test: $p_\ell(2)\equiv1\pmod{2^\ell}$.
Writing $m_{\mathrm{test}}$ for the number of tests, our counting expression becomes
\[
 \underbrace{\sum_x\prod_{e\in G}\Phi_e(x)}_{\text{one factor per clause}}
 \qquad\longrightarrow\qquad
 \underbrace{\sum_x\prod_{i=1}^{m_{\mathrm{test}}} p_\ell(L_i(x))}_{\text{one factor per test}}.
\]
The left side is $\#G$. The least nonnegative residue of the right
side modulo $2^\ell$ is the number of assignments passing every test.
When the tests catch every nonsatisfying assignment, this is exactly
$\#G$. The same encoding works for
any sparse polynomial equation $P_i(x)=0$ over $\mathbb F_2$: take
$L_i(x)$ to be the integer sum of its listed monomials. Again the
equation holds exactly when this sum is even.

To reuse the Taylor step, we need a product of input degree $O(n)$.
Multiplying the $m_{\mathrm{test}}$ test factors directly gives only the bound
$O(km_{\mathrm{test}}\ell)$, potentially quadratic in $n$. The key is to truncate
the product \emph{across all tests together}. Section~\ref{subsec:rational-lift}
writes $p_\ell(y)$ as a sum of terms $e_j(y)h(y)^j$, where
$e_j$ has degree at most one and $h(y)=y(y-1)$ is even at every
integer. A product term containing $\ell$ or more copies of $h$ is
therefore zero modulo $2^\ell$ on Boolean assignments, even if those
copies come from different tests. We keep just the terms with fewer
than $\ell$ copies in total, tracking that number as we multiply.
Each retained term has at most $m_{\mathrm{test}}$ linear factors and $\ell-1$
quadratic factors in the $L_i$'s. Since $\deg L_i\le k$, its input
degree is at most $k(m_{\mathrm{test}}+2(\ell-1))=O(n)$.

For the replacement forms, what matters is which variables each factor
reads. Where Section~\ref{subsec:preview-deformation} used one form
for each variable in a clause, we now use one for each variable in a
test, reusing it throughout that test. Each sparse equation reads only
polylogarithmically many variables. Branching on the values of the
$O(n/\sqrt{\log n})$ most frequent variables leaves each remaining
variable in only polylogarithmically many tests, as required by
Section~\ref{sec:construction}. On each branch, fixing the shared
measurements again lets us sum one group at a time. Because the
truncated product has input degree $O(n)$, the degree-$R$ replacements
give $\deg_T H=O(nR)$: the same $O(1+nR/Q)$ Taylor coefficients per
point recover the contributions at $T=0$ with $0,1,\ldots,\ell-1$
copies of $h$. Their sum modulo $2^\ell$, taken as the least nonnegative
residue, is the exact branch count. Adding the branch counts gives the
number of common zeros.

\begin{theorem}[Counting common zeros of sparse polynomials]
\label{thm:overview-sparse-polynomials}
Fix integers $k\ge2$ and $c\ge1$. Let $P_1,\ldots,P_{m_{\mathrm{test}}}$ be polynomials
over $\mathbb F_2$ in $n\ge20$ Boolean variables, with $m_{\mathrm{test}}\le cn$.
Each $P_i$ is given as a list of at most $(\log n)^c$ monomials
of degree at most $k$. The exact number of common zeros in
$\{0,1\}^n$ can be computed deterministically in
$2^{O_{k,c}(n(\log\log n)^2/\sqrt{\log n})}$ bit operations and
$n^{O_{k,c}(1)}$ space.
\end{theorem}
Sections~\ref{sec:counting} and~\ref{sec:construction} supply the
counting routine and the replacement forms; Section~\ref{sec:setup}
uses them to prove the theorem directly for polynomial equations.

For the final system constructed for $G$, the number of common zeros is $\#G$.
Section~\ref{sec:hashes} uses only $2^{(\log n)^{O_k(1)}}$ calls
to the counter per leaf, which preserves the running-time exponent in
Theorem~\ref{thm:overview-sparse-polynomials}. Finally, choosing
$\sigma$ of order $(\log\log n)^2/\sqrt{\log n}$ in
Section~\ref{subsec:general-reduction} keeps $B$ polylogarithmic
and the number of leaves within $2^{O_k(n(\log\log n)^2/\sqrt{\log n})}$.
Their satisfying assignments are disjoint, so adding their counts
gives the bound in Proposition~\ref{prop:interpolation-bound}.

\section{A fast counting algorithm via shared linear summaries}\label{sec:counting}
Sections~\ref{sec:counting}--\ref{sec:setup} prove
Theorem~\ref{thm:overview-sparse-polynomials}. We begin with the sum
from Section~\ref{subsec:preview-encoding}: for each Boolean assignment,
multiply the factors, then add the products over all assignments.
Here the factors can be any rational polynomials. We show how to
compute the sum when the replacement forms and measurements are given.
Section~\ref{sec:construction} constructs them using only the variables
read by each factor. Section~\ref{sec:setup} supplies one factor per
sparse polynomial equation.

\subsection{Polynomial factors and the value to recover}
\label{subsec:product-interface}
Let $\mathcal F$ index the factors, and let $I_f\subseteq[n]$ be the
variables read by $\Phi_f$. With rational coefficients our target is
\begin{equation}\label{eq:general-product-sum}
 Z=\sum_{x\in\{0,1\}^n}\prod_{f\in\mathcal F}\Phi_f((x_v)_{v\in I_f}).
\end{equation}
For clause satisfaction indicators, $Z$ is the number of satisfying
assignments. The proof also works with coefficients in any commutative
$\mathbb Q$-algebra $\mathcal A$: sums and products then take place in
$\mathcal A$, and interpolation uses only rational scalars. Readers may
take $\mathcal A=\mathbb Q$ throughout this section.

Different factors may use different replacements for the same variable.
Give each incidence $(f,v)$ its own indeterminate $Y_{f,v}$ and suppose
\begin{equation}\label{eq:general-product-degree}
 \deg_{\{Y_{f,v}\}}\!
    \left(\prod_{f\in\mathcal F}\Phi_f((Y_{f,v})_{v\in I_f})\right)\le d .
\end{equation}
This is the degree of the whole product computed over $\mathcal A$.
Choose replacement rows $\vec P_{f,v}(T)$ of degree at most $R$ with
$\vec P_{f,v}(0)=\delta_v$, and form
\begin{equation}\label{eq:general-count-polynomial}
 H(T)=\sum_{x\in\{0,1\}^n}\prod_{f\in\mathcal F}
   \Phi_f\bigl((\langle\vec P_{f,v}(T),x\rangle)_{v\in I_f}\bigr)
   \in\mathcal A[T].
\end{equation}
The replacements restore the inputs at zero and multiply the degree by
at most $R$. Thus $H(0)=Z$ and $\deg_T H\le d_H:=dR$. Our application
will have $d=O(n)$, as in the bounded-occurrence example.

\subsection{The required rows, partitions, and measurements}
\label{subsec:layout-interface}
We use the same design as in Section~\ref{subsec:preview-separation},
with a group assignment for each factor in place of each clause.
The final condition below records the coefficient bound needed for
exact arithmetic. Here $\widetilde\xi$ denotes extension by zero
from a group to all $n$ coordinates.

\begin{definition}\label{def:layout}
For the factor scopes $(I_f)_{f\in\mathcal F}$, let $r\ge2$, $D\ge1$,
and $1\le R<Q$ be integers, and let $0<\tau\le1/2$.
We require the following data and properties.
\begin{enumerate}
\item For each $t\in[Q]$, a partition
$[n]=S_{t,1}\sqcup\cdots\sqcup S_{t,r}$, allowing empty parts,
with $|S_{t,g}|\le2n/r$.
\item For every factor $f\in\mathcal F$, a sequence
$\sigma_f\in[r]^Q$. The value $\sigma_f(t)$ assigns factor $f$
to a group at point $t$.
\item For every $t\in[Q]$ and $g\in[r]$, an integer matrix
$C_{t,g}\in\mathbb Z^{[c_{t,g}]\times S_{t,g}}$, where
$c_{t,g}$ is a nonnegative integer. Each row has sum of absolute
values at most $D$, and
\[
 \sum_{g=1}^r c_{t,g}\le2\tau n.
\]
For an assignment $x$, the entries of
$C_{t,g}(x|_{S_{t,g}})$ are the measurements on group $g$.
\item For every $f\in\mathcal F$ and $v\in I_f$, a row
$\vec{P}_{f,v}(T)\in\mathbb Q[T]^{1\times n}$ with
$\vec{P}_{f,v}(0)=\delta_v$ and $\deg \vec{P}_{f,v}\le R$.
For every $t\in[Q]$, $g\in[r]\setminus\{\sigma_f(t)\}$, and
$\xi\in\mathbb Q^{S_{t,g}}$, require
\[
 C_{t,g}\xi=\vec{0}\quad\Longrightarrow\quad
 \langle \vec{P}_{f,v}(t), \widetilde\xi\rangle=0,
\]
where $\widetilde\xi\in\mathbb Q^n$ is the extension of $\xi$ by zero.
\item With $d_{\mathrm{den}}=(R-1)!Q!$, every coefficient of
$d_{\mathrm{den}} \vec{P}_{f,v}$ is an integer with
$O(Q\log Q+\log D)$ bits, with an absolute implied constant.
\end{enumerate}
\end{definition}

To interpret the kernel condition, fix $t$, $f$, and $v\in I_f$,
and put $g=\sigma_f(t)$. Write $x_h=x|_{S_{t,h}}$.
If $x,x'\in\mathbb Q^n$ agree outside $S_{t,h}$ for some $h\ne g$
and satisfy $C_{t,h}x_h=C_{t,h}x'_h$, then
$x'_h-x_h\in\ker C_{t,h}$. The condition gives
\[
 \langle \vec{P}_{f,v}(t), x'\rangle=\langle \vec{P}_{f,v}(t), x\rangle.
\]
Applying this one group at a time shows that the tuple
$(\langle \vec{P}_{f,v}(t), x\rangle)_{v\in I_f}$ is determined by $x_g$ and
$(C_{t,h}x_h)_{h\ne g}$. Fixing all the measurement vectors therefore
makes the entire factor a function of $x_g$. This applies to every
polynomial factor $\Phi_f$, including factors with coefficients in
$\mathcal A$.

Each measurement of a Boolean vector lies in $[-D,D]\cap\mathbb Z$.
We bound the sum of absolute values of the matrix entries because
the construction can place the same Boolean coordinate in several
auxiliary positions. After those positions are identified, entries
of $C_{t,g}$ need not belong to $\{0,1,-1\}$. A rank bound alone
would not control the number of possible measurements: the single
row $(1,2,4,\ldots,2^{n-1})$ distinguishes all $2^n$ Boolean vectors.

\subsection{Separating the sum by fixing measurements}
\label{subsec:measurement-factorization}
Fixing the measurements makes every factor depend on only its assigned
group. The following lemma states the resulting calculation over a
commutative ring, so it applies equally to rational-valued factors and
to factors in $\mathcal A$. The restrictions $x_i=1$ will be needed
for Taylor coefficients and are local to individual groups.

\begin{lemma}\label{lem:measurement-separation}
Let $[n]=S_1\sqcup\cdots\sqcup S_r$ be a partition, allowing empty parts.
For each $g\in[r]$, let $C_g$ be an integer matrix with $c_g$ rows
and columns indexed by $S_g$. Suppose each row has sum of absolute
values at most an integer $D\ge0$, and write $c=\sum_g c_g$.
Let $\mathcal A$ be a commutative ring with identity, and let
$A_g:\mathbb Q^n\to\mathcal A$ satisfy
\[
 A_g(x+\xi)=A_g(x)
 \qquad
 (x\in\mathbb Q^n,\ \xi\in\ker C_h,\ h\ne g),
\]
where $\xi$ is extended by zero outside $S_h$.
For any $E\subseteq[n]$, the sum
\[
 Z_E=\sum_{\substack{x\in\{0,1\}^n\\x_i=1\ (i\in E)}}
           \prod_{g=1}^r A_g(x)
\]
can be evaluated by examining at most
\[
 2(2D+1)^c\sum_{g=1}^r2^{|S_g|}
\]
Boolean vectors, with at most one $A_g$ evaluation,
$\poly(n,r,c,\log(D+2))$ additional bit operations, and $O(1)$ ring
operations per vector. Apart from the evaluators' own storage and
$O(1)$ ring elements, the procedure uses $\poly(n,r,c,\log(D+2))$
bits of space.
\end{lemma}
\begin{proof}
For $y_g\in\mathbb Z^{c_g}$, define
\[
 \mathcal X_g(y_g)=\{u\in\{0,1\}^{S_g}:C_gu=y_g\},
 \qquad
 \mathcal Y=\prod_{g=1}^r\{-D,\ldots,D\}^{c_g}.
\]
Every tuple of measurements of a Boolean assignment belongs to
$\mathcal Y$, and $|\mathcal Y|=(2D+1)^c$.
We first identify the contribution of a fixed measurement tuple
$\vec y=(y_1,\ldots,y_r)$. If every $\mathcal X_g(y_g)$ is nonempty,
let $\bar x_g\in\mathcal X_g(y_g)$ be a representative for each $g$,
and put
\[
 \mathcal X_{g,E}(y_g)=
 \{u\in\mathcal X_g(y_g):u_i=1\text{ for all }i\in E\cap S_g\}.
\]
If $x_h\in\mathcal X_h(y_h)$ for every $h$, then
$x_h-\bar x_h\in\ker C_h$. Applying the invariance hypothesis
successively for $h\ne g$ gives
\[
 A_g\Bigl(\sum_{h=1}^r x_h\Bigr)
 =A_g\Bigl(x_g+\sum_{h\ne g}\bar x_h\Bigr).
\]
The assignments with measurement tuple $\vec y$ and fixed bits indexed
by $E$ form $\prod_g\mathcal X_{g,E}(y_g)$. Define
\begin{equation}\label{eq:group-sum}
 \Sigma_g(\vec y)=\sum_{x_g\in\mathcal X_{g,E}(y_g)}
       A_g\Bigl(x_g+\sum_{h\ne g}\bar x_h\Bigr).
\end{equation}
Distributivity shows that these assignments contribute
$\prod_g\Sigma_g(\vec y)$ to $Z_E$. If $\mathcal X_{g,E}(y_g)$ is empty,
then $\Sigma_g(\vec y)=0$. The representatives $\bar x_g$ themselves
need not satisfy the fixed-bit conditions indexed by $E$.
Every Boolean assignment has a unique measurement tuple, so
\[
 Z_E=\sum_{\vec y\in\mathcal Y}\prod_{g=1}^r\Sigma_g(\vec y),
\]
where the product is taken to be zero if any $\mathcal X_g(y_g)$
is empty.

The algorithm evaluates this identity one measurement tuple at a
time, starting with $Z=0_{\mathcal A}$. For each $\vec y\in\mathcal Y$,
a first scan of each $\{0,1\}^{S_g}$ finds a representative
$\bar x_g\in\mathcal X_g(y_g)$; if any such set is empty, the
algorithm skips this tuple. Otherwise it initializes
$p=1_{\mathcal A}$. To compute $\Sigma_g(\vec y)$, it initializes
$s=0_{\mathcal A}$ and scans $u\in\{0,1\}^{S_g}$ again. Whenever
\[
 C_gu=y_g,\qquad u_i=1\quad(i\in E\cap S_g),
\]
the algorithm performs the update
\[
 s\leftarrow s+A_g\Bigl(u+\sum_{h\ne g}\bar x_h\Bigr).
\]
At the end of this scan, $s=\Sigma_g(\vec y)$, and the algorithm sets
$p\leftarrow ps$. After all groups, it sets $Z\leftarrow Z+p$.
After all tuples $\vec y$ have been processed, $Z=Z_E$.

For each $\vec y$, the scan finding the representatives and the scan
computing the $\Sigma_g(\vec y)$ each examine at most
$\sum_g2^{|S_g|}$ Boolean vectors. This gives the stated bound.
Checking a vector's measurements and fixed bits uses
$\poly(n,r,c,\log(D+2))$ bit operations: each matrix row has sum of
absolute values at most $D$, so its partial sums have
$O(\log(D+2))$ bits. There is at most one factor evaluation per vector.
The retained state is $\vec y$, $(\bar x_1,\ldots,\bar x_r)$, $g$, $u$,
$s$, $p$, and $Z$. The tuple $\vec y$ contains $c$ integers in $[-D,D]$,
the representatives contain $n$ bits in total, and $s,p,Z\in\mathcal A$.
\end{proof}

To evaluate \eqref{eq:general-count-polynomial} at a fixed $t$, group
the transformed factors by $\sigma_f(t)$ and apply the lemma in
$\mathcal A$ with $E=\varnothing$. Definition~\ref{def:layout}
gives its invariance hypothesis, so the sum is $H(t)$. As in the overview, the two exponential costs
are the measurement choices and the Boolean assignments in one group.

\subsection{Taylor coefficients from fixed Boolean substitutions}
\label{subsec:fixed-boolean-substitutions}
The $Q$ values $H(1),\ldots,H(Q)$ need not determine $H$.
Set
\begin{equation}\label{eq:hasse-order}
 q=\left\lfloor\frac{d_H}{Q}\right\rfloor,\qquad J=q+1.
\end{equation}
Since $QJ>d_H$, it suffices to compute
\begin{equation}\label{eq:taylor-truncation}
 \mathcal H_t(z)=\sum_{j=0}^{J-1}([z^j]H(t+z))z^j
 \qquad(t\in[Q]).
\end{equation}
Hermite interpolation recovers $H$, and hence $Z=H(0)$, from these
$QJ$ coefficients in $\mathcal A$. Indeed, the rational Hermite
matrix for polynomials of degree less than $QJ$ is invertible over
$\mathbb Q$. Its inverse acts on elements of $\mathcal A$ by rational
linear combinations.

Fix $t$. The replacement forms at $t+z$ need not respect the design
at $t$. Write
\[
 \Delta\vec P_{f,v}(z)=\vec P_{f,v}(t+z)-\vec P_{f,v}(t).
\]
Every entry is divisible by $z$. For fixed $x\in\mathbb Q^n$,
introduce independent indeterminates $\vec X$ and replace each input by
\begin{equation}\label{eq:jet-substitution}
 \langle\vec P_{f,v}(t),x\rangle
       +\langle\Delta\vec P_{f,v}(z),\vec X\rangle.
\end{equation}
Let
\begin{equation}\label{eq:auxiliary-polynomial}
 \mathcal G_x(\vec X,z)=\prod_{f\in\mathcal F}
 \Phi_f\!\left(
  (\langle\vec P_{f,v}(t),x\rangle+
   \langle\Delta\vec P_{f,v}(z),\vec X\rangle)_{v\in I_f}\right).
\end{equation}
Setting $\vec X=x$ gives
$\sum_x\mathcal G_x(x,z)=H(t+z)$.
Holding $\vec X$ fixed instead makes every correction independent
of $x$, so the design at $t$ still separates the factors.
Moreover, each occurrence of $\vec X$ carries a factor of $z$, giving
\begin{equation}\label{eq:degree-cost}
 \deg_{\vec X}([z^j]\mathcal G_x(\vec X,z))\le j.
\end{equation}
The next identity recovers the substitution $\vec X=x$ from fixed
Boolean substitutions and restrictions on the assignments being summed.

\begin{lemma}\label{lem:boolean-differences}
Let $q\ge0$ be an integer and let $\mathcal A$ be a commutative
ring with identity. For each $x\in\{0,1\}^n$, let
$p_x(X_1,\ldots,X_n)$ be a polynomial over $\mathcal A$ of degree
at most $q$. Then
\begin{align}
 \sum_{x\in\{0,1\}^n}p_x(x)
 &=\sum_{\substack{E\subseteq[n]\\|E|\le q}}
   \sum_{U\subseteq E}(-1)^{|E|-|U|}
   \sum_{\substack{x\in\{0,1\}^n\\x_i=1\ (i\in E)}}
                  p_x(\mathbf1_U).
 \label{eq:boolean-differences}
\end{align}
Here $\mathbf1_U$ is the indicator vector of $U$.
\end{lemma}
\begin{proof}
For fixed $x$, we replace every positive power of $X_i$ by $X_i$.
This leaves Boolean evaluations unchanged and does not increase
the degree. By M\"obius inversion on subsets, the resulting
multilinear polynomial has the expansion
\[
 \widetilde p_x(\vec{X})=\sum_{E\subseteq[n]}c_{x,E}\prod_{i\in E}X_i,
 \qquad
 c_{x,E}=\sum_{U\subseteq E}(-1)^{|E|-|U|}p_x(\mathbf1_U).
\]
The degree bound gives $c_{x,E}=0$ whenever $|E|>q$.
Setting $\vec{X}=x$ and summing over $x$ now gives the claimed identity:
the monomial $\prod_{i\in E}x_i$
selects exactly the assignments with $x_i=1$ for every $i\in E$.
\end{proof}

Apply Lemma~\ref{lem:boolean-differences} to
$[z^j]\mathcal G_x$ over $\mathcal A$ for each $j<J$.
All coefficients can use the same pairs $U\subseteq E$, $|E|\le q$,
so compute them together in
\[
 \mathcal R=\mathcal A[z]/(z^J).
\]
For a fixed pair $(E,U)$, let $\Phi_{f,U}(x;z)$ be factor $f$
in \eqref{eq:auxiliary-polynomial} after setting $\vec X=\mathbf1_U$.
Group these factors by their assignments:
\begin{equation}\label{eq:group-polynomial}
 A_{g,U}(x;z)=\prod_{f:\sigma_f(t)=g}\Phi_{f,U}(x;z).
\end{equation}
Their product is $\mathcal G_x(\mathbf1_U,z)$.
For $h\ne g$, changing $x$ by a vector in $\ker C_{t,h}$ changes
neither the original inputs of these factors nor their fixed
corrections. Lemma~\ref{lem:measurement-separation} therefore
computes the restricted sum with $x_i=1$ for $i\in E$ by examining
at most
\begin{equation}\label{eq:boolean-enumeration}
 2r(2D+1)^{2\tau n}2^{2n/r}
\end{equation}
Boolean vectors. Combining all the pairs gives
\begin{equation}\label{eq:full-taylor-sum}
 H(t+z)\equiv
 \sum_{\substack{E\subseteq[n]\\|E|\le q}}
 \sum_{U\subseteq E}(-1)^{|E|-|U|}
 \sum_{\substack{x\in\{0,1\}^n\\x_i=1\ (i\in E)}}
       \mathcal G_x(\mathbf1_U,z)\pmod{z^J}.
\end{equation}
The group products and sums are formed in $\mathcal R$. The result is
$\mathcal H_t(z)$; repeating at all $t$ supplies the interpolation data.
The algorithm never stores a polynomial in all $n$ indeterminates:
it sets $\vec X=\mathbf1_U$ first and stores only the $J$ coefficients in $\mathcal A$.

\subsection{The three exponential costs}
\label{subsec:three-costs}
For each $t\in[Q]$,
the number of pairs $U\subseteq E\subseteq[n]$ with $|E|\le q$ is
\begin{equation}\label{eq:pair-count}
 C_q=\sum_{s=0}^{\min(q,n)}2^s\binom ns.
\end{equation}
In particular, $C_0=1$ and $C_q=3^n$ for $q\ge n$.
For every $0<\eta\le1$,
\begin{equation}\label{eq:finite-difference-cost}
 \eta^qC_q\le\sum_{s=0}^n\binom ns(2\eta)^s=(1+2\eta)^n,
\end{equation}
because $\eta^q\le\eta^s$ for every retained index $s\le q$.

\begin{proposition}[Common counting routine]\label{prop:general-count}
Let $\mathcal A$ be a commutative $\mathbb Q$-algebra. Suppose the
product of the factors in \eqref{eq:general-product-sum}, computed
over $\mathcal A$, satisfies the degree bound \eqref{eq:general-product-degree},
and that the replacement rows, partitions, and measurements satisfy
Definition~\ref{def:layout}. With $q,J$ as in \eqref{eq:hasse-order},
the routine computes $Z$ by examining at most
\[
 2Qr\,C_q(2D+1)^{2\tau n}2^{2n/r}
\]
Boolean vectors. For each vector it evaluates at most $|\mathcal F|$
factors in $\mathcal A[z]/(z^J)$. The additional operations per
vector and the final interpolation take polynomially many operations
in $\mathcal A$ and over $\mathbb Q$, in the parameters
$n,|\mathcal F|,D,Q,R,J,r$ and the total scope length.
Apart from the factor evaluators' own storage, the routine retains
only polynomially many algebra elements, rational numbers and index bits.
\end{proposition}
\begin{proof}
There are $Q$ points, $C_q$ pairs per point, and at most
\eqref{eq:boolean-enumeration} Boolean vectors per pair.
Forming each group product uses at most $|\mathcal F|$ factor evaluations.
Addition and multiplication modulo $z^J$ cost $O(J^2)$ operations
on coefficients in $\mathcal A$. The preceding Taylor identity
and interpolation prove correctness.
Process the points, pairs, measurement tuples, and local assignments
sequentially, retaining their current indices and accumulators.
Together with the $QJ$ interpolation coefficients, this gives the
stated storage bound. Bit complexity additionally depends on the
cost of evaluating the factors and on coefficient sizes; these are
verified for the sparse polynomial application in
Section~\ref{subsec:one-query-cost}.
\end{proof}

When $d=O(n)$, we have $d_H=O(nR)$ and $q=O(nR/Q)$.
Taking $\eta=R/Q$ in \eqref{eq:finite-difference-cost} gives
\[
 \log C_q\le q\log(Q/R)+n\log(1+2R/Q)
     =O\!\left(n\frac RQ\log\frac{2Q}{R}\right).
\]
Consequently, if factor evaluation and coefficient arithmetic have
polynomial bit cost, the running time is a polynomial factor times
\begin{equation}\label{eq:three-costs}
 2^{O\left(n\left[
       \frac RQ\log\frac{2Q}{R}
       +\tau\log(2D+1)+\frac1r\right]\right)}.
\end{equation}
These are exactly the three costs from the overview. The parameter
choice in Lemma~\ref{lem:incidence-parameters} makes their sum
$O((\log\log n)^2/\sqrt{\log n})$ when factor scopes and their
maximum incidence are bounded by a fixed power of $\log n$.
The routine also applies when $d$ is larger; then one keeps the
actual value $q=\lfloor dR/Q\rfloor$ in the bound of
Proposition~\ref{prop:general-count}.

We have so far assumed that the design is supplied. The next
section constructs it from the factor scopes. The remaining
two sections use the resulting routine first to count the zeros of a
supplied polynomial system and then to choose such a system for a formula.

\section{Constructing low-degree replacement forms}\label{sec:construction}
The counting routine needs one replacement form for each pair $(f,v)$
where factor $f$ reads variable $v$. For the application in
Section~\ref{sec:setup}, $f$ is a polynomial equation and its scope is
the union of the variable sets of its monomials. This section uses
only those scopes.
We construct the rows $\vec{P}_{f,v}(T)$ and measurement matrices $C_{t,g}$
in Definition~\ref{def:layout}, together with the partitions $S_{t,g}$
and factor assignments $\sigma_f$. The main difficulty is to keep
$\deg \vec{P}_{f,v}\le R$ with $R$ much smaller than $Q$. The degree bound
for $H$ grows linearly with $R$, so a small $R/Q$ reduces the number
of Taylor coefficients needed at each point. Choosing the rows
independently at $T=0,1,\ldots,Q$ and interpolating would generally give
degree $Q$. We instead construct their values at all these points together.

The construction first gives polynomial rows on a complete array of
auxiliary coordinates. We then place each factor--variable pair in a
copy of that array. Several positions can contain the same Boolean
variable $x_v$; their values are always equal, and they do not become
independent variables in the counting sum.

\subsection{The auxiliary coordinates}\label{subsec:incidence-layout}
We first specify the larger coordinate set $\mathcal B$ on which
the auxiliary rows $\vec{P}_u(T)$ will act, together with the incidence
bounds needed to place the actual pairs $(f,v)$ into copies of it.
Let $(I_f)_{f\in\mathcal F}$ be the factor scopes, with $I_f\subseteq[n]$,
and write
\begin{equation}\label{eq:factor-incidences}
 \begin{gathered}
 \mathcal A=\{(f,v):f\in\mathcal F,\ v\in I_f\},\qquad M=|\mathcal A|,\\
 |I_f|\le w\quad(f\in\mathcal F),\qquad
 \#\{f:v\in I_f\}\le b\quad(v\in[n]).
 \end{gathered}
\end{equation}
Thus $w$ bounds the number of variables in a factor's scope, and $b$
bounds the number of factors containing one variable. The scope bound
$w$ need not bound the degree of the factor polynomial. A factor with
empty scope is constant and needs no auxiliary position; assign such
a factor to group one at every point. If necessary, adjoin a distinct
constant-one factor with scope $\{v\}$ for every $v\in[n]$. This changes
neither the product nor the count, and increases the maximum incidence
by at most one. With $b$ denoting the bound after this addition, we assume
\[
 n\ge1,\qquad b,w\ge1,\qquad n\le M\le bn.
\]
Throughout this section, $r\ge2$ and $1\le R<Q$ are integers and
$0<\tau\le1/2$.

At each point $t\in[Q]$, the variable $x_v$ will belong to one group,
while a factor containing $v$ may be assigned to another. We will choose
\[
 a_v\in[r]^Q\quad(v\in[n]),\qquad
 d_f\in[r]^Q\quad(f\in\mathcal F),
\]
where $a_v(t)$ specifies the group containing $x_v$ and $d_f(t)$
specifies the group assigned to factor $f$. The position for $(f,v)$
will have label $(a_v,d_f)$. In particular, all positions containing
$x_v$ will have the same first sequence $a_v$.

Before choosing $a_v$ and $d_f$, take the complete set of possible labels:
\begin{equation}\label{eq:auxiliary-labels}
 \mathcal B=([r]^Q)^2,\qquad u=(a_u,d_u),\qquad D=|\mathcal B|=r^{2Q}.
\end{equation}
An auxiliary vector $\zeta\in\mathbb Q^{\mathcal B}$ has one rational
coordinate $\zeta_u$ for each pair $u$. The label $u$ stays fixed as
$\zeta$ varies. For $t\in[Q]$ and $g\in[r]$, define
\begin{equation}\label{eq:auxiliary-groups}
 S^{\mathcal B}_{t,g}=\{u\in\mathcal B:a_u(t)=g\}.
\end{equation}
For fixed $t$, these sets partition $\mathcal B$ into $r$ sets of size
$D/r$.

For each $u\in\mathcal B$, we seek a polynomial row
$\vec{P}_u(T)\in\mathbb Q[T]^{1\times\mathcal B}$ of degree at most $R-1$
with $\vec{P}_u(0)=\delta_u$. At $T=t$, the value $\langle \vec{P}_u(t), \zeta\rangle$ should be
determined by
\[
 \zeta|_{S^{\mathcal B}_{t,d_u(t)}}
 \quad\text{and}\quad C^{\mathcal B}\zeta,
\]
where $C^{\mathcal B}$ is one integer matrix, independent of $u,t$,
with entries in $\{0,1,-1\}$ and few rows. Later, using
$u_{f,v}=(a_v,d_f)$ will make every input of factor $f$ use the group
$d_f(t)$. The choices of $a_v,d_f$ and the placement into copies are
deferred to Sections~\ref{subsec:choosing-labels}
and~\ref{subsec:embedding}, respectively.

\subsection{The matrices $M_0$ and $C^{\mathcal B}$}
To construct the rows $\vec{P}_u(T)$, we seek a matrix
$M_0\in\mathbb Q^{\mathcal B\times\mathcal B}$ that fixes
$\ker C^{\mathcal B}$ and satisfies
\begin{equation}\label{eq:matrix-support-target}
 M_0[u,y]\ne0\quad\Longrightarrow\quad
 \bigl|\{s\in[Q]:a_y(s)\ne d_u(s)\}\bigr|\le R-1.
\end{equation}
The identity
\begin{equation}\label{eq:coordinate-decomposition}
 \zeta_u=((I-M_0)\zeta)_u+
          \sum_{y\in\mathcal B}M_0[u,y]\zeta_y
\end{equation}
explains both requirements. If $M_0$ fixes $\ker C^{\mathcal B}$,
the first term is determined by $C^{\mathcal B}\zeta$; we will leave
it independent of $T$. In the sum, multiply each nonzero
$M_0[u,y]$ by a polynomial that is one at zero and vanishes at every
$t$ with $a_y(t)\ne d_u(t)$. The bound
\eqref{eq:matrix-support-target} permits degree at most $R-1$.
At $T=t$, the sum will then use only the coordinates
$y\in S^{\mathcal B}_{t,d_u(t)}$.

For $s\in[Q]$, let $\vartheta_s:\mathcal B\to\mathcal B$ exchange the
entries $a_u(s)$ and $d_u(s)$, leaving every other entry unchanged.
Define its permutation matrix $\Pi_s$ by
\[
 (\Pi_s\zeta)_u=\zeta_{\vartheta_s(u)}.
\]
The exchanged pair $\vartheta_s(u)$ belongs to $\mathcal B$ because this set
contains every pair of sequences in $[r]^Q$. The matrices $\Pi_s$
commute and satisfy $\Pi_s^2=I$. Their product
\[
 V_0=\prod_{s=1}^Q\Pi_s
\]
exchanges the complete sequences $a_u$ and $d_u$. Thus
$V_0[u,y]\ne0$ implies $a_y(s)=d_u(s)$ for every $s$; it satisfies
\eqref{eq:matrix-support-target} with no mismatches. We will modify
$V_0$ so that the resulting matrix also fixes the kernel of a short
list of integer measurements.

Define
\begin{equation}\label{eq:swap-weight}
 W_0=\frac12\sum_{s=1}^Q(I-\Pi_s).
\end{equation}
On a common eigenvector $\psi$ of the $\Pi_s$, let $j$ be the number
of indices $s$ for which $\Pi_s\psi=-\psi$. Then
\[
 W_0\psi=j\psi,\qquad V_0\psi=(-1)^j\psi,
 \qquad V_0p(W_0)\psi=(-1)^jp(j)\psi
\]
for every polynomial $p$. Therefore $V_0p(W_0)$ fixes $\psi$ whenever
$p(j)=(-1)^j$. We will construct an explicit common eigenbasis in which
the proportion of vectors with a given $j$ is
$\Pr[W=j]$ for $W\sim\operatorname{Bin}(Q,(r-1)/(2r))$.

For an interval
$\mathcal I=\{A_0,\ldots,A_0+R-1\}\subseteq\{0,\ldots,Q\}$,
we can enforce the equalities $f_{\mathcal I}(j)=(-1)^j$
for $j\in\mathcal I$ with a polynomial of degree at most $R-1$.
We use the explicit interpolation formula
\begin{equation}\label{eq:swap-matrix-definition}
 f_{\mathcal I}(z)=(-1)^{A_0}\sum_{j=0}^{R-1}(-2)^j
                         \binom{z-A_0}{j},
 \qquad M_0=V_0f_{\mathcal I}(W_0),
\end{equation}
where
\[
 \binom{z-A_0}{j}=\frac1{j!}\prod_{a=0}^{j-1}(z-A_0-a)
\]
and the empty product is one. For $0\le q<R$, the binomial theorem gives
$f_{\mathcal I}(A_0+q)=(-1)^{A_0}(1-2)^q=(-1)^{A_0+q}$.

\begin{lemma}\label{lem:swaps-matrix}
For $\mathcal B$, $\mathcal I$ and $M_0$ as above, there is a matrix
$C^{\mathcal B}\in\{0,1,-1\}^{[c_{\mathcal B}]\times\mathcal B}$ such that
\[
 c_{\mathcal B}\le D\Pr[W\notin\mathcal I],\qquad
 W\sim\operatorname{Bin}\!\left(Q,\frac{r-1}{2r}\right),
\]
and $M_0\xi=\xi$ for every $\xi\in\ker C^{\mathcal B}$.
\end{lemma}
\begin{proof}
For $(\alpha,\delta)\in[r]^2$, let $e_{\alpha\delta}$ be the
indicator function of that ordered pair. Exchanging its two entries
has the orthogonal eigenbasis
\[
 e_{\alpha\alpha}\quad(\alpha\in[r]),\qquad
 e_{\alpha\delta}+e_{\delta\alpha},\quad
 e_{\alpha\delta}-e_{\delta\alpha}\quad(1\le\alpha<\delta\le r).
\]
The first two types have eigenvalue $+1$, and the third has eigenvalue
$-1$. There are $r(r+1)/2$ vectors with eigenvalue $+1$ and
$r(r-1)/2$ with eigenvalue $-1$.

For each $s\in[Q]$, choose one of these functions
$\psi_s:[r]^2\to\{0,1,-1\}$, and define
\[
 \psi(u)=\prod_{s=1}^Q\psi_s(a_u(s),d_u(s))
 \qquad(u\in\mathcal B).
\]
The $D=r^{2Q}$ choices give nonzero orthogonal vectors: their inner
products factor into the inner products of the functions $\psi_s$.
They form a basis of $\mathbb Q^{\mathcal B}$ with entries in
$\{0,1,-1\}$. If exactly $j$ of the chosen $\psi_s$ have eigenvalue
$-1$, then $W_0\psi=j\psi$ and $V_0\psi=(-1)^j\psi$. Hence $M_0$
fixes $\psi$ whenever $j\in\mathcal I$.

To make $\ker C^{\mathcal B}$ a space fixed by $M_0$, we define
the rows of $C^{\mathcal B}$ to be the transposes of the basis
vectors with $j\notin\mathcal I$.
A fraction $(r-1)/(2r)$ of the choices at each
position have eigenvalue $-1$, independently across positions. The
fraction of the $D$ basis vectors retained as rows is therefore
$\Pr[W\notin\mathcal I]$, proving the row bound. If
$C^{\mathcal B}\xi=\vec{0}$, then $\xi$ is orthogonal to every retained
basis vector. It is a linear combination of the basis vectors with
$j\in\mathcal I$, all of which $M_0$ fixes.
\end{proof}

For a bound $\epsilon>0$, the condition
\begin{equation}\label{eq:incidence-tail}
 \Pr\!\left[\operatorname{Bin}\!\left(Q,\frac{r-1}{2r}\right)
                         \notin\mathcal I\right]\le\epsilon
\end{equation}
thus gives $c_{\mathcal B}\le\epsilon D$. After placing the factor
inputs, we will use $\epsilon=\tau/(rb)$. We next prove the other
requirement on $M_0$.

\begin{lemma}\label{lem:swaps-support}
For all $u,y\in\mathcal B$, if $M_0[u,y]\ne0$, then
\[
 \bigl|\{s\in[Q]:a_y(s)\ne d_u(s)\}\bigr|\le R-1.
\]
\end{lemma}
\begin{proof}
Expand $f_{\mathcal I}(W_0)$ in the commuting matrices $\Pi_s$.
Since $\deg f_{\mathcal I}\le R-1$ and $\Pi_s^2=I$, each resulting
monomial is a scalar multiple of $\prod_{s\in J}\Pi_s$ for some
$J\subseteq[Q]$ with $|J|\le R-1$. Multiplication by $V_0$ gives
\[
 V_0\prod_{s\in J}\Pi_s=\prod_{s\notin J}\Pi_s.
\]
A nonzero $(u,y)$ entry of this permutation matrix requires
$a_y(s)=d_u(s)$ for every $s\notin J$. There are at most $R-1$
other positions. If more than $R-1$ positions disagree, every
summand has zero $(u,y)$ entry, so $M_0[u,y]=0$ as well.
\end{proof}

\subsection{The polynomial rows}
We now use $M_0$ to construct the auxiliary rows $\vec{P}_u(T)$ sought
in Section~\ref{subsec:incidence-layout}.
Lemma~\ref{lem:swaps-matrix} makes $(I-M_0)\zeta$ a function of
$C^{\mathcal B}\zeta$. Lemma~\ref{lem:swaps-support} bounds the number
of points at which a nonzero term $M_0[u,y]\zeta_y$ uses a coordinate
outside $S^{\mathcal B}_{t,d_u(t)}$. We now multiply that term by a
polynomial vanishing at those points and equal to one at zero.

For $M_0[u,y]\ne0$, define
\begin{equation}\label{eq:coefficient-correction}
 E_{u,y}=\{s\in[Q]:a_y(s)\ne d_u(s)\},\qquad
 \varphi_{u,y}(T)=\prod_{s\in E_{u,y}}\left(1-\frac Ts\right).
\end{equation}
The empty product is one. Then $\deg\varphi_{u,y}\le R-1$,
$\varphi_{u,y}(0)=1$, and $\varphi_{u,y}(t)=0$ whenever
$a_y(t)\ne d_u(t)$. Define
\begin{equation}\label{eq:swaps-row}
 \vec{P}_u(T)=\delta_u(I-M_0)+
 \sum_{\substack{y\in\mathcal B\\M_0[u,y]\ne0}}
 M_0[u,y]\varphi_{u,y}(T)\delta_y.
\end{equation}
This row acts as a linear form in $\zeta$, with coefficients that are
polynomials in the single parameter $T$.

\begin{lemma}\label{lem:swaps-forms}
The rows in \eqref{eq:swaps-row} have degree at most $R-1$ and satisfy
$\vec{P}_u(0)=\delta_u$ for every $u\in\mathcal B$. For $t\in[Q]$ and
$g\in[r]$, let $C^{\mathcal B}_{t,g}$ be the restriction of
$C^{\mathcal B}$ to the columns $S^{\mathcal B}_{t,g}$. For every
$u,t,g$ with $g\ne d_u(t)$ and every
$\xi\in\mathbb Q^{S^{\mathcal B}_{t,g}}$, its extension
$\widetilde\xi$ by zero to $\mathcal B$ satisfies
\[
 C^{\mathcal B}_{t,g}\xi=\vec{0}
 \quad\Longrightarrow\quad \langle \vec{P}_u(t), \widetilde\xi\rangle=0.
\]
More generally, $\langle \vec{P}_u(t), \zeta\rangle$ is determined by
$\zeta|_{S^{\mathcal B}_{t,d_u(t)}}$ and $C^{\mathcal B}\zeta$.
\end{lemma}
\begin{proof}
The degree bound follows from that of $\varphi_{u,y}$. At zero,
\[
 \vec{P}_u(0)=\delta_u(I-M_0)+\delta_uM_0=\delta_u.
\]
Applying \eqref{eq:swaps-row} to $\zeta$ gives
\begin{equation}\label{eq:swaps-form-decomposition}
 \langle \vec{P}_u(T), \zeta\rangle=((I-M_0)\zeta)_u+
 \sum_{\substack{y\in\mathcal B\\M_0[u,y]\ne0}}
 M_0[u,y]\varphi_{u,y}(T)\zeta_y.
\end{equation}
At $T=t$, all summands with $a_y(t)\ne d_u(t)$ vanish. If
$\widetilde\xi$ is supported on $S^{\mathcal B}_{t,g}$ with
$g\ne d_u(t)$, each remaining summand is zero on $\widetilde\xi$.
The hypothesis $C^{\mathcal B}_{t,g}\xi=\vec{0}$ also gives
$C^{\mathcal B}\widetilde\xi=\vec{0}$, so
$(I-M_0)\widetilde\xi=\vec{0}$ by Lemma~\ref{lem:swaps-matrix}.
This proves the implication.

For the final assertion, two vectors with the same measurements under
$C^{\mathcal B}$ differ by an element of its kernel. Thus
$(I-M_0)\zeta$ is determined by $C^{\mathcal B}\zeta$. The remaining
terms in \eqref{eq:swaps-form-decomposition} at $T=t$ use only
$\zeta|_{S^{\mathcal B}_{t,d_u(t)}}$.
\end{proof}

Fix $t$ and write $\zeta_g=\zeta|_{S^{\mathcal B}_{t,g}}$. The
restrictions of $C^{\mathcal B}$ satisfy
\begin{equation}\label{eq:auxiliary-measurements}
 C^{\mathcal B}\zeta=\sum_{g=1}^r C^{\mathcal B}_{t,g}\zeta_g.
\end{equation}
Fixing each vector $C^{\mathcal B}_{t,g}\zeta_g$ therefore fixes
$C^{\mathcal B}\zeta$ while imposing separate conditions on the
$r$ auxiliary coordinate groups. When all vectors
$C^{\mathcal B}_{t,g}\zeta_g$ are fixed, $\langle \vec{P}_u(t), \zeta\rangle$ is determined
by $\zeta|_{S^{\mathcal B}_{t,d_u(t)}}$.
We will obtain the corresponding separation on the actual Boolean
variables by placing $(f,v)$ at a coordinate labeled $(a_v,d_f)$.

\begin{remark}
We illustrate how \eqref{eq:swaps-row} confines dependence outside the
assigned group to one linear measurement. Take $Q=R=2$, outside the
regime $R<Q$ used for the running-time bound, and $r=2$. Use
$\{0,1\}$ as the group indices and $\mathcal I=\{0,1\}$, so
$f_{\mathcal I}(z)=1-2z$. Starting with the label $(00,11)$, the
two exchanges generate four coordinates:
\[
 \zeta_0=\zeta_{(00,11)},\quad \zeta_1=\zeta_{(10,01)},\quad
 \zeta_2=\zeta_{(01,10)},\quad \zeta_{12}=\zeta_{(11,00)}.
\]
Both exchanges preserve this set of four coordinates, so we can
restrict the calculation to it. On this restriction,
$M_0=\Pi_1+\Pi_2-\Pi_1\Pi_2$ fixes the kernel of
\[
 c(\zeta)=\zeta_0-\zeta_1-\zeta_2+\zeta_{12}.
\]
The row indexed by $u=(00,11)$ gives
\[
 \langle \vec{P}_u(T), \zeta\rangle=\zeta_0-\frac T2\zeta_1-T\zeta_2.
\]
It equals $\zeta_0$ at zero, while
\[
 \langle \vec{P}_u(1), \zeta\rangle=c(\zeta)+\frac12\zeta_1-\zeta_{12},\qquad
 \langle \vec{P}_u(2), \zeta\rangle=c(\zeta)-\zeta_2-\zeta_{12}.
\]
At $t=1$, the labels of $\zeta_1,\zeta_{12}$ satisfy
$a_y(1)=1=d_u(1)$. At $t=2$, the labels of
$\zeta_2,\zeta_{12}$ satisfy $a_y(2)=1=d_u(2)$.
Fixing $c(\zeta)$ therefore leaves $\langle \vec{P}_u(t), \zeta\rangle$ dependent only on
coordinates in its assigned group. Here $c(\zeta)$ plays the role
of $C^{\mathcal B}\zeta$ on the four-coordinate restriction. The
full construction must give this property for every $u\in\mathcal B$
with at most $\epsilon D$ measurement rows.
\end{remark}

\subsection{Choosing the variable and factor groups}\label{subsec:choosing-labels}
We now choose the families $(a_v)_{v\in[n]}$ and
$(d_f)_{f\in\mathcal F}$ from
Section~\ref{subsec:incidence-layout}, and set
\[
 u_{f,v}=(a_v,d_f)\qquad((f,v)\in\mathcal A).
\]
These choices have two requirements. First, if a label occurs $c_u$
times, its incidences need $c_u$ different positions in copies of the
auxiliary array. Thus the number of copies needed is
\[
 c_u=\#\{(f,v)\in\mathcal A:u_{f,v}=u\},\qquad
 h=\max_{u\in\mathcal B}c_u.
\]
Second, the actual variable group $\{v:a_v(t)=g\}$ must be small.
Bounding $h$ alone would bound the number of incidences in a group,
not give the required bound on its number of Boolean variables.
The next lemma controls both quantities.

\begin{lemma}\label{lem:incidence-labels}
Let $(I_f)_{f\in\mathcal F}$ satisfy \eqref{eq:factor-incidences},
with $n\le M\le bn$, and put $D=r^{2Q}$ for integers $r\ge2$ and
$Q\ge1$. Suppose
\begin{equation}\label{eq:incidence-balance-hypotheses}
 2(b+w)D^2\le M,\qquad 2Qr^2\le n.
\end{equation}
One can deterministically choose $a_v,d_f\in[r]^Q$, with $d_f(t)=1$
for factors of empty scope, so that
\[
 \begin{aligned}
 \max_{u\in\mathcal B}\#\{(f,v)\in\mathcal A:(a_v,d_f)=u\}
 &\le\frac{2M}{D},\\
 \#\{v\in[n]:a_v(t)=g\}&\le\frac{2n}{r}
 \qquad(t\in[Q],\ g\in[r]).
 \end{aligned}
\]
The construction takes
$\poly(n,M,|\mathcal F|,D,Q,r,b,w)$ bit operations.
\end{lemma}
\begin{proof}
We first estimate the effect of random labels; we will then fix
their values deterministically. For this estimate, all $a_v$ and
all $d_f$ with nonempty $I_f$ are independent and uniform on $[r]^Q$.
For empty $I_f$, we set $d_f$ identically one.
Each incidence label $u_{f,v}=(a_v,d_f)$ is uniform on $\mathcal B$.
Put $n_{t,g}=\#\{v:a_v(t)=g\}$, and consider
\[
 \Phi=\sum_{u\in\mathcal B}(c_u-M/D)^2,
 \qquad
 \Xi=\sum_{t=1}^Q\sum_{g=1}^r(n_{t,g}-n/r)^2.
\]
Their expansions as sums of indicators are
\[
 \begin{aligned}
 \Phi&=\sum_{(f,v),(f',v')\in\mathcal A}
       \mathds{1}_{\{(a_v,d_f)=(a_{v'},d_{f'})\}}-\frac{M^2}{D},\\
 \Xi&=\sum_{t=1}^Q\sum_{v,v'\in[n]}
       \mathds{1}_{\{a_v(t)=a_{v'}(t)\}}-\frac{Qn^2}{r}.
 \end{aligned}
\]
Two incidence labels are independent unless they share a factor or a
variable. For each $(f,v)$, there are at most $b+w$ incidences sharing
$f$ or $v$, including $(f,v)$ itself. Independent pairs have equality
probability $1/D$; the other pairs have probability at most one. Hence
\[
 \mathbb E\Phi\le M(b+w).
\]
For each $t$ and $v\ne v'$, the values $a_v(t),a_{v'}(t)$ are independent
and uniform on $[r]$. The second expansion therefore gives
\[
 \mathbb E\Xi=Qn(1-1/r)\le Qn.
\]

To obtain the labels deterministically, we fix the $a_v$ and the
$d_f$ for nonempty $I_f$ one at a time. At each step we choose a
value that does not increase the conditional expectation of
\[
 \frac{\Phi}{M(b+w)}+\frac{\Xi}{Qn}.
\]
Such a choice exists because the current expectation is the average
over the possible values of the next $a_v$ or $d_f$. The final value
is at most two. Since both summands are nonnegative,
\[
 c_u\le\frac MD+\sqrt{2M(b+w)},\qquad
 n_{t,g}\le\frac nr+\sqrt{2Qn}.
\]
The two inequalities in \eqref{eq:incidence-balance-hypotheses} make
the square-root terms at most $M/D$ and $n/r$, respectively.

The following enumeration computes the conditional expectations in
$\poly(n,M,|\mathcal F|,D,Q,r,b,w)$ bit operations.
Put $K=r^Q$, so $D=K^2$. Each indicator in the expansion of
$\Phi$ depends on at most the four independent choices
$a_v,d_f,a_{v'},d_{f'}$; repeated indices contribute just one choice.
Each indicator in $\Xi$ depends on at most $a_v,a_{v'}$. After any
partial fixing, enumerate at most $K^4=D^2$ assignments to the
remaining choices in one indicator. Its conditional probability has
denominator dividing $K^4$. Summing the $M^2+Qn^2$ indicators computes
both expectations. Including the normalizations $M(b+w)$ and $Qn$,
all rational values in these calculations have numerators and
denominators with
\[
 O\!\left(\log(2D)+\log(2M)+\log(2n)+\log(2Q)+\log(2+b+w)\right)
\]
bits. There are at most $n+|\mathcal F|$ choices to fix, each with
$K$ candidate values. Since $K^4=D^2$, the entire construction takes
$\poly(n,M,|\mathcal F|,D,Q,r,b,w)$ bit operations.
\end{proof}

\subsection{Placing copies of the variables in the auxiliary arrays}\label{subsec:embedding}
We now transfer the auxiliary rows $\vec{P}_u(T)$ and matrix
$C^{\mathcal B}$ to the rows $\vec{P}_{f,v}(T)$ and matrices $C_{t,g}$
on the original variables required by Definition~\ref{def:layout}.
Assume \eqref{eq:incidence-balance-hypotheses} and apply
Lemma~\ref{lem:incidence-labels}. With $h=\max_u c_u$, index $h$
copies of the auxiliary coordinates by $[h]\times\mathcal B$.
For each $(f,v)\in\mathcal A$, we assign $c(f,v)\in[h]$ so that all
pairs $(c(f,v),u_{f,v})$ are distinct. This is possible because no
label occurs more than $h$ times, and
\[
 hD\le2M\le2bn.
\]
Define the linear map
$\iota:\mathbb Q^n\longrightarrow\mathbb Q^{[h]\times\mathcal B}$ by
\[
 (\iota x)_{c,u}=
 \begin{cases}
 x_v,&(c,u)=(c(f,v),u_{f,v})\text{ for some }(f,v)\in\mathcal A,\\
 0,&\text{otherwise}.
 \end{cases}
\]
The occupied positions are distinct, so this definition is unambiguous.
Different positions can contain the same $x_v$, and unused positions
are fixed at zero. For $c\in[h]$, define the projection
\[
 \pi_c:\mathbb Q^{[h]\times\mathcal B}\longrightarrow\mathbb Q^{\mathcal B},
 \qquad (\pi_c\eta)_u=\eta_{c,u}.
\]
Now put
\begin{equation}\label{eq:actual-rows}
 \begin{gathered}
 \vec{P}_{f,v}(T)=\vec{P}_{u_{f,v}}(T)\pi_{c(f,v)}\iota,\\
 S_{t,g}=\{v\in[n]:a_v(t)=g\},\qquad \sigma_f(t)=d_f(t).
 \end{gathered}
\end{equation}
The row $\vec{P}_{f,v}(T)$ acts on the actual variables $x\in\mathbb Q^n$.
At $T=0$, it extracts the value in position $(c(f,v),u_{f,v})$,
which is $x_v$. Thus $\vec{P}_{f,v}(0)=\delta_v$, and its degree is at most
$R-1$. Lemma~\ref{lem:incidence-labels} gives $|S_{t,g}|\le2n/r$.

Define the measurement matrices by
\begin{equation}\label{eq:actual-measurements}
 \widetilde C=\operatorname{diag}
   \bigl(\underbrace{C^{\mathcal B},\ldots,C^{\mathcal B}}_{h\text{ copies}}\bigr),
 \qquad \widehat C=\widetilde C\iota,
 \qquad C_{t,g}=\widehat C|_{S_{t,g}}.
\end{equation}
The restriction keeps the columns in $S_{t,g}$ and all rows, including
zero rows. Thus $\widehat Cx$ records the auxiliary measurements in
each copy after its coordinates have been filled from $x$.
The matrices $C_{t,g}$ are integral. Their entries need not belong to
$\{0,1,-1\}$, because coefficients at several positions containing
the same $x_v$ are added. Each row of $\widetilde C$ has at
most $D$ nonzero entries, all equal to $1$ or $-1$. Multiplication by
$\iota$ adds entries in a common column and discards unused positions,
so it cannot increase
the sum of their absolute values. Consequently every row of $C_{t,g}$
has absolute row sum at most $D$, and its value on a Boolean assignment
lies in $[-D,D]\cap\mathbb Z$.

If \eqref{eq:incidence-tail} holds, each $C_{t,g}$ has
$c_{t,g}=hc_{\mathcal B}$ rows. Hence
\begin{equation}\label{eq:incidence-measurement-count}
 \sum_{g=1}^r c_{t,g}=rh c_{\mathcal B}
 \le rh\epsilon D\le2r\epsilon M\le2r\epsilon bn.
\end{equation}
Setting $\epsilon=\tau/(rb)$ makes this at most $2\tau n$.

To verify separation, fix $t\in[Q]$, $g\in[r]$ and
$(f,v)\in\mathcal A$ with $g\ne\sigma_f(t)$. Suppose
$\xi\in\mathbb Q^{S_{t,g}}$ satisfies $C_{t,g}\xi=\vec{0}$, and extend it
by zero to $\widetilde\xi\in\mathbb Q^n$. Equation
\eqref{eq:actual-measurements} gives
$\widetilde C\iota\widetilde\xi=\vec{0}$. Thus, for every $c\in[h]$,
\[
 C^{\mathcal B}\pi_c\iota\widetilde\xi=\vec{0}.
\]
Every nonzero coordinate of $\pi_c\iota\widetilde\xi$ contains a
variable $v'$ with $a_{v'}(t)=g$. Its auxiliary label has first
sequence $a_{v'}$, so this vector is supported on
$S^{\mathcal B}_{t,g}$. Lemma~\ref{lem:swaps-forms}, applied in copy
$c(f,v)$ with $d_{u_{f,v}}(t)=d_f(t)=\sigma_f(t)$, gives
\[
 \langle \vec{P}_{f,v}(t), \widetilde\xi\rangle
 =\langle \vec{P}_{u_{f,v}}(t), \pi_{c(f,v)}\iota\widetilde\xi\rangle=0.
\]
This is the kernel condition in Definition~\ref{def:layout}.
All inputs of factor $f$ use the same assigned group $d_f(t)$, and
the counting sum still ranges over exactly the $n$ Boolean bits.

\subsection{Coefficient bounds and the completed construction}
The substitution rows $\vec{P}_{f,v}(T)\in\mathbb Q[T]^{1\times n}$ in
\eqref{eq:actual-rows} have polynomial entries with rational
coefficients. We now bound the bits needed to store those coefficients;
these bounds will control exact arithmetic in
Section~\ref{subsec:one-query-cost}.
We first give a common denominator and coefficient bounds for the
auxiliary rows $\vec{P}_u(T)$ defined in \eqref{eq:swaps-row}.
Passing from $\vec{P}_u(T)$ to $\vec{P}_{f,v}(T)$ by \eqref{eq:actual-rows} only
adds coefficients in common columns or discards unused columns,
so the same denominator and bound on the sum of absolute values apply.

\begin{lemma}\label{lem:row-coefficients}
Let $d_{\mathrm{den}}=(R-1)!Q!$. Then
$d_{\mathrm{den}}\vec{P}_u(T)\in\mathbb Z[T]^{1\times D}$ for every $u\in\mathcal B$. The sum of the absolute values of all coefficients
in each row $d_{\mathrm{den}}\vec{P}_u(T)$ is at most $2^{O(Q\log Q)}$.
The same bound holds for $d_{\mathrm{den}}\vec{P}_{f,v}(T)$.
The matrices $M_0,C^{\mathcal B}$ and the rows $\vec{P}_u(T)$ can be
constructed in $\poly(D,Q,r)$ bit operations.
\end{lemma}
\begin{proof}
For $0\le j<R$, the corresponding summand of
$f_{\mathcal I}(W_0)$ equals
\[
 (-1)^{A_0}(-2)^j\binom{W_0-A_0I}{j}
 =\frac{(-1)^{A_0+j}}{j!}
   \prod_{a=0}^{j-1}\bigl(2W_0-2(A_0+a)I\bigr).
\]
Each matrix factor on the right is integral because
$2W_0=QI-\sum_s\Pi_s$. Also $j!$ divides $(R-1)!$.
Multiplication by the permutation matrix $V_0$ therefore shows that
$(R-1)!M_0$ is integral. The coefficients of $\varphi_{u,y}$ have
denominators dividing $\prod_{s\in E_{u,y}}s$, which divides $Q!$.
Equation~\eqref{eq:swaps-row} proves the asserted common denominator.

For the coefficient estimates, we use the matrix norm
$\|A\|_\infty=\max_i\sum_j|A[i,j]|$ and
the polynomial norm $\|\sum_j a_jT^j\|_1=\sum_j|a_j|$.
Since $\|W_0\|_\infty\le Q$ and $0\le A_0+a\le Q$ for all
factors above, each $2W_0-2(A_0+a)I$ has norm at most $4Q$.
It follows that
\[
 \|M_0\|_\infty\le R(4Q)^{R-1},\qquad
 \|\varphi_{u,y}\|_1
 \le\prod_{s\in E_{u,y}}(1+1/s)\le2^Q.
\]
The sum of the absolute values of all coefficients in the row
$d_{\mathrm{den}}\vec{P}_u$ is therefore at most
\[
 d_{\mathrm{den}}\bigl(1+(1+2^Q)R(4Q)^{R-1}\bigr).
\]
Its logarithm is $O(Q\log Q)$ because $R<Q$.
For $u=u_{f,v}$, multiplication of $d_{\mathrm{den}}\vec{P}_u(T)$ by
$\pi_{c(f,v)}\iota$ adds coefficients in common columns and discards
unused columns. By \eqref{eq:actual-rows}, the resulting row is
$d_{\mathrm{den}}\vec{P}_{f,v}(T)$, so it satisfies the same bound.

Enumerating the eigenbasis in Lemma~\ref{lem:swaps-matrix}, evaluating
$f_{\mathcal I}(W_0)$, and forming the polynomials $\varphi_{u,y}$
require $\poly(D,Q,r)$ arithmetic operations. Using the common
denominators above, the coefficients stored during these matrix
and polynomial calculations have numerators and denominators with
$O(Q\log Q)$ bits. Thus the construction takes $\poly(D,Q,r)$ bit
operations.
\end{proof}

The construction has three quantitative requirements. The two
inequalities in \eqref{eq:incidence-balance-hypotheses} bound the number
of auxiliary copies and the number of actual variables in each group.
The tail bound with $\epsilon=\tau/(rb)$ gives the total measurement
bound through \eqref{eq:incidence-measurement-count}. We collect the
result for use in the counting algorithm.

\begin{lemma}\label{lem:layout}
Let $n,b,w\ge1$ be integers, and let $(I_f)_{f\in\mathcal F}$ be
subsets of $[n]$ of size at most $w$,
with each $v\in[n]$ belonging to at most $b$ sets. Put
$M=\sum_f|I_f|$ and assume $n\le M\le bn$. Let $r\ge2$ and
$1\le R<Q$ be integers, let $0<\tau\le1/2$, and put $D=r^{2Q}$.
Suppose
\[
 2(b+w)D^2\le M,\qquad 2Qr^2\le n,
\]
and an interval
$\mathcal I=\{A_0,\ldots,A_0+R-1\}\subseteq\{0,\ldots,Q\}$ satisfies
\[
 \Pr[W\notin\mathcal I]\le\frac{\tau}{rb},\qquad
 W\sim\operatorname{Bin}\!\left(Q,\frac{r-1}{2r}\right).
\]
One can deterministically construct all the data in
Definition~\ref{def:layout} in
$\poly(n,M,|\mathcal F|,D,Q,r,b,w)$ bit operations.
\end{lemma}
\begin{proof}
Lemma~\ref{lem:swaps-matrix} constructs $C^{\mathcal B}$ with
$c_{\mathcal B}\le\tau D/(rb)$. Lemmas~\ref{lem:swaps-support}
and~\ref{lem:swaps-forms} give the auxiliary polynomial rows.
Lemma~\ref{lem:incidence-labels} chooses the variable and factor
groups with $hD\le2M$ and $|S_{t,g}|\le2n/r$.
The maps in \eqref{eq:actual-rows} and \eqref{eq:actual-measurements}
then give rows with $\vec{P}_{f,v}(0)=\delta_v$, degree at most $R-1\le R$,
and the required kernel implication. Every row of $C_{t,g}$ has
absolute row sum at most $D$, and \eqref{eq:incidence-measurement-count}
gives $\sum_{g=1}^r c_{t,g}\le2\tau n$ for each $t\in[Q]$.
Lemma~\ref{lem:row-coefficients} supplies the common denominator and
coefficient bounds. Together, the constructions take
$\poly(n,M,|\mathcal F|,D,Q,r,b,w)$ bit operations, and the resulting
arrays occupy $\poly(n,M,|\mathcal F|,D,Q,r,b,w)$ bits.
\end{proof}

\subsection{Choosing the parameters}\label{subsec:incidence-parameters}
In the application, both the largest scope $w$ and the maximum number
$b$ of factors containing a variable will be bounded by a fixed power
of $\log n$. We now choose parameters satisfying
Lemma~\ref{lem:layout} in that regime. The exponent of the counting
cost depends on the three quantities
\[
 \frac RQ\log\frac{2Q}{R},\qquad
 \tau\log(2D+1),\qquad \frac1r.
\]
They account respectively for recovering Taylor coefficients,
enumerating measurement values, and enumerating assignments in one
group. The following choices bound all three at once.

\begin{lemma}\label{lem:incidence-parameters}
Fix an integer $\beta\ge1$. Let $n\ge20$, put
$\lambda=\lceil\log_2 n\rceil$ and $\nu=\lceil\log_2\lambda\rceil$,
and suppose $b,w\le\lambda^\beta$ and $n\le M\le bn$.
For all sufficiently large $n$, the parameters
\begin{equation}\label{eq:parameter-QR}
 r=\left\lfloor\frac{\sqrt\lambda}{\nu^2}\right\rfloor,
 \qquad Q=\left\lfloor\frac{\lambda}{128\nu}\right\rfloor,
 \qquad R=(\beta+3)\lceil\sqrt\lambda\rceil,
\end{equation}
\[
 \tau=\frac1{r\lambda},\qquad
 \epsilon=\frac1{br^2\lambda},\qquad D=r^{2Q},
\]
together with the interval specified in the proof, satisfy all
numerical hypotheses of Lemma~\ref{lem:layout}. They also satisfy
\[
 R\ge32,\qquad 6R\le Q,\qquad D\le2^{\lambda/128},
\]
and
\begin{equation}\label{eq:balanced-cost}
 \frac RQ\log\frac{2Q}{R}+\tau\log(2D+1)+\frac1r
 =O_\beta\!\left(\frac{\nu^2}{\sqrt\lambda}\right).
\end{equation}
Given the numerical values $n,M,b,w$, the parameters and numerical
hypotheses can be computed and checked exactly in
$\poly_\beta(\log n)$ bit operations. For fixed $\beta$, only finitely
many $n$ fail these checks.
\end{lemma}
\begin{proof}
For sufficiently large $n$, the parameters have orders
\[
 r=\Theta(\sqrt\lambda/\nu^2),\qquad
 Q=\Theta(\lambda/\nu),\qquad R=\Theta_\beta(\sqrt\lambda).
\]
In particular, eventually $r\ge2$, $R\ge32$, and $6R\le Q$.
Since $\log_2 r\le\nu/2$,
\[
 \log_2 D=2Q\log_2 r
 \le2\frac{\lambda}{128\nu}\frac\nu2=\frac{\lambda}{128}.
\]
The two balance inequalities follow for sufficiently large $n$:
\[
 2(b+w)D^2\le4\lambda^\beta2^{\lambda/64}\le n\le M,
 \qquad 2Qr^2\le n.
\]
For the second, $Q,r$ are bounded by fixed powers of $\lambda$,
whereas $n>2^{\lambda-1}$. The first follows from the same comparison.

Put
\[
 \mu=\frac{Q(r-1)}{2r},\qquad
 A_0=\left\lfloor\mu-\frac{R-1}{2}\right\rfloor,
 \qquad \mathcal I=\{A_0,\ldots,A_0+R-1\}.
\]
Here $Q/4\le\mu\le Q/2$. Since $R\le Q/6$, the interval lies in
$\{0,\ldots,Q\}$. Its center differs from $\mu$ by less than one,
and $R\ge32$ ensures that it contains every integer within $R/4$
of $\mu$. For $W\sim\operatorname{Bin}(Q,(r-1)/(2r))$, Hoeffding's
inequality gives
\[
 \Pr[W\notin\mathcal I]
 \le2e^{-R^2/(8Q)}
 \le2e^{-16(\beta+3)^2\nu}
 \le2^{-(\beta+2)\nu}
 \le\lambda^{-(\beta+2)}
 \le\frac1{br^2\lambda}.
\]
The last inequality uses $b\le\lambda^\beta$ and $r^2\le\lambda$.
This proves \eqref{eq:incidence-tail} with
$\epsilon=\tau/(rb)$. Also $0<\tau\le1/2$ once $r\ge2$.

Finally,
\[
 \frac RQ=O_\beta(\nu/\sqrt\lambda),\qquad
 \log(2Q/R)=O(\nu),\qquad
 \tau\log(2D+1)=O(1/r).
\]
Together with $1/r=O(\nu^2/\sqrt\lambda)$, these prove
\eqref{eq:balanced-cost}.

We finish by showing that the parameters in \eqref{eq:parameter-QR}
can be constructed exactly within the stated bit bound.
The algorithm finds $\lambda=\lceil\log_2 n\rceil$ as the least
integer with $n\le2^\lambda$, and then finds
$\nu=\lceil\log_2\lambda\rceil$ in the same way. It obtains $r$ as
the largest integer satisfying $r^2\nu^4\le\lambda$, computes $Q$
by integer division, and finds $\lceil\sqrt\lambda\rceil$ by an
integer square-root search to obtain $R$.
If $r<2$ or $Q\le R$, the algorithm reports failure at this stage.
Otherwise it constructs $\tau,\epsilon,D$ and the endpoints of
$\mathcal I$ using integer or rational arithmetic. It then checks
$\mathcal I\subseteq\{0,\ldots,Q\}$, the two balance inequalities,
$R\ge32$, and $6R\le Q$. The tail probability in
\eqref{eq:incidence-tail} has denominator $(2r)^Q$, so its required
bound can also be checked by integer arithmetic. These computations
take $\poly_\beta(\log n)$ bit operations. The preceding estimates
show that all checks pass for sufficiently large $n$.
\end{proof}

\section{Counting common zeros of sparse polynomial equations}\label{sec:setup}
We now prove Theorem~\ref{thm:overview-sparse-polynomials}. The input
is a system $\mathcal P$ of $m_{\mathrm{test}}\le cn$ polynomial equations
$P_i(x)=0$ over $\mathbb F_2$ in $n$ Boolean variables. Each $P_i$ is a
list of at most $(\log n)^c$ monomials of degree at most $k$, for fixed
$k,c$. Our target is the integer
\begin{equation}\label{eq:common-zero-count}
 N(\mathcal P)=\#\{x\in\{0,1\}^n:P_i(x)=0\text{ for every }i\}.
\end{equation}
First we build a product with one factor per equation whose value on
the Boolean cube records the common-zero indicator. The difficulty is
keeping its total input degree linear in $n$. Next we construct the
replacement forms for these factors and use Section~\ref{sec:counting}
to sum the product. Section~\ref{sec:hashes} uses the resulting
algorithm for arbitrary supplied systems, including systems that still
accept nonsatisfying assignments of a formula.

\subsection{An integer polynomial for one equation}\label{subsec:rational-lift}
On Boolean inputs we may replace each positive power $x_v^j$ by $x_v$.
Combine duplicate monomials modulo two. If $\mathcal M_i$ is the
resulting list of variable sets for $P_i$, define its integer lift by
\[
 L_i(\vec X)=\sum_{M\in\mathcal M_i}\prod_{v\in M}X_v .
\]
The empty monomial is $1$ and the empty sum is $0$. The value $L_i(x)$
counts the monomials equal to one, so $P_i(x)=0$ precisely when
$L_i(x)$ is even. Write $I_i=\bigcup_{M\in\mathcal M_i}M$. Although
$L_i$ can read $k(\log n)^c$ variables, it still has degree at most $k$.

Set $\ell=n+1$. Since $0\le N(\mathcal P)\le2^n<2^\ell$, it suffices
to obtain its residue modulo $2^\ell$. We first represent the
evenness indicator by an integer polynomial modulo this power of two.
Multiplying $m_{\mathrm{test}}$ such indicators directly would give
only a quadratic degree bound; the form of the next lemma will let us
control the degree across all equations together.

Put $h(Y)=Y(Y-1)$. Its value is even at every integer $Y$.
Writing the indicator in powers of $h$ exposes one factor of two for
each copy of $h$ in the product.

\begin{lemma}\label{lem:rational-idempotent}
For every integer $\ell\ge1$, one can construct polynomials
$e_0,\ldots,e_{\ell-1}\in\mathbb Z[Y]$, each of degree at most one,
such that
\begin{equation}\label{eq:idempotent-expansion}
 p_\ell(Y)=\sum_{j=0}^{\ell-1}e_j(Y)h(Y)^j,
 \qquad
 p_\ell(y)\equiv\mathds{1}_{\{2\mid y\}}\pmod{2^\ell}
 \quad(y\in\mathbb Z).
\end{equation}
The coefficients of the $e_j$ have $\poly(\ell)$ bits, and the
construction uses $\poly(\ell)$ bit operations and $\poly(\ell)$
bits of space.
\end{lemma}
\begin{proof}
Let $F_\ell$ be the modulus-amplifying polynomial of Beigel and
Tarui~\cite[Section~2.3]{BT94}. Chan and Williams apply $F_\ell$ to
sums of clause-violation indicators to count satisfying assignments
deterministically~\cite[Theorem~2.5 and proof of Theorem~1.6]{CW21}.
We need the indicator of even parity, so we take its complement:
\begin{equation}\label{eq:binary-indicator}
 p_\ell(Y)=1-F_\ell(Y)=(1-Y)^\ell
       \sum_{j=0}^{\ell-1}\binom{\ell+j-1}{j}Y^j.
\end{equation}
The finite sum is the inverse of $(1-Y)^\ell$ modulo $Y^\ell$.
Indeed, the coefficient of $Y^j$ in $(1+Y+Y^2+\cdots)^\ell$
counts weak compositions of $j$ into $\ell$ parts and equals
$\binom{\ell+j-1}{j}$. Therefore
\[
 p_\ell(Y)\equiv1\pmod{Y^\ell},
 \qquad
 p_\ell(Y)\equiv0\pmod{(1-Y)^\ell}.
\]
For even $y$, the first congruence gives $p_\ell(y)\equiv1\pmod{2^\ell}$.
For odd $y$, the second gives $p_\ell(y)\equiv0\pmod{2^\ell}$.

The polynomial $p_\ell$ has integer coefficients and degree less
than $2\ell$. Successive division by the monic quadratic
$h=Y^2-Y$ writes it uniquely as
$\sum_{j<\ell}e_jh^j$, with integer remainders $e_j$ of degree
less than two. Lemma~\ref{lem:rational-lift-height} in
Appendix~\ref{app:arithmetic} bounds their coefficients and proves
the $\poly(\ell)$ bit-operation bound for this construction.
\end{proof}

\subsection{Keeping the product degree linear}
The full product $\prod_{i=1}^{m_{\mathrm{test}}} p_\ell(L_i(\vec{X}))$ has degree at most
$km_{\mathrm{test}}(2\ell-1)$. Each factor $h(y)$ contributes a factor of two at
integer arguments, so a term containing at least $\ell$ such factors
can be discarded modulo $2^\ell$. This lets us retain only terms
whose total power of $h$ is less than $\ell$, across all equations together.
Introduce a formal variable $V$ to record that power, using the same
$V$ for every equation. Its exponent records a guaranteed power of two
dividing the corresponding term at integer arguments. It is not an
additional Boolean variable to be summed over.
This is where we choose the coefficient algebra of
Section~\ref{subsec:product-interface}:
\[
 \mathcal A_\ell=\mathbb Q[V]/(V^\ell).
\]
In this algebra every multiplication discards powers $V^s$ with
$s\ge\ell$. Once the product is formed, we add its retained
coefficients using the linear map
\[
 \mathcal S_\ell\!\left(\sum_{s=0}^{\ell-1}b_sV^s\right)
 =\sum_{s=0}^{\ell-1}b_s .
\]
This map need not preserve products, so it is applied only after the
factors have been multiplied. We use the same notation for polynomial
coefficients $b_s$.

\begin{lemma}\label{lem:total-order}
Let $m_{\mathrm{test}}\ge0$ and $\ell\ge1$ be integers. For integers
$y_1,\ldots,y_{m_{\mathrm{test}}}$, put
\[
 B_i(V)=\sum_{j=0}^{\ell-1}e_j(y_i)h(y_i)^jV^j.
\]
Then
\[
 \mathcal S_\ell\!\Bigl(\prod_{i=1}^{m_{\mathrm{test}}} B_i(V)\bmod V^\ell\Bigr)
 \equiv\prod_{i=1}^{m_{\mathrm{test}}}\mathds{1}_{\{2\mid y_i\}}\pmod{2^\ell}.
\]
For any nonnegative integer $d_*$, if the $y_i$ are instead
polynomials over $\mathbb Q$ of total degree at most $d_*$,
then each retained coefficient of $V^s$, and hence their sum, has
total input degree at most
$d_*(m_{\mathrm{test}}+2(\ell-1))$.
\end{lemma}
\begin{proof}
Before truncation, a term contributing to the coefficient of $V^s$
has the form
\[
 \prod_{i=1}^{m_{\mathrm{test}}} e_{j_i}(y_i)h(y_i)^{j_i},
 \qquad \sum_{i=1}^{m_{\mathrm{test}}} j_i=s.
\]
At integer arguments it is divisible by $2^s$. Dropping every
coefficient with $s\ge\ell$ therefore leaves the sum of coefficients
unchanged modulo $2^\ell$. Without truncation, that sum is
$\prod_i p_\ell(y_i)$, which has the required congruence by
Lemma~\ref{lem:rational-idempotent}.

For polynomial arguments, every retained term has
$\sum_i j_i\le\ell-1$. Since $\deg e_{j_i}\le1$ and $\deg h=2$,
its degree is at most
\[
 \sum_{i=1}^{m_{\mathrm{test}}} d_*(1+2j_i)
 \le d_*(m_{\mathrm{test}}+2(\ell-1)).
\]
The bound holds coefficient by coefficient, as well as for their sum.
\end{proof}

To see why the truncation uses the total order across all equations,
take $\ell=2$. Then
\[
 p_2(Y)=1-3Y^2+2Y^3=(1-Y)+(2Y-1)h(Y).
\]
For two equations, multiplication modulo $V^2$, followed by
$\mathcal S_2$, retains
\[
 (1-y_1)(1-y_2)
 +(2y_1-1)h(y_1)(1-y_2)
 +(1-y_1)(2y_2-1)h(y_2).
\]
Its degree is at most four. The omitted term
$(2y_1-1)(2y_2-1)h(y_1)h(y_2)$ has degree six, but is divisible
by four at integer inputs.

\subsection{Counting with supplied replacement forms}\label{subsec:count-polynomial}
For equation $i$ supply Section~\ref{sec:counting} with the factor
\begin{equation}\label{eq:lifted-factor}
 \mathcal B_i((X_v)_{v\in I_i},V)
 =\sum_{j=0}^{\ell-1}e_j(L_i(\vec X))h(L_i(\vec X))^j V^j
 \quad\text{in }\mathcal A_\ell[(X_v)_{v\in I_i}].
\end{equation}
Within a factor, every occurrence of $X_v$ uses the same replacement
form; different factors may use different forms for $X_v$. Even if
each factor receives its own independent inputs, $L_i$ has degree at
most $k$ in those inputs. Lemma~\ref{lem:total-order} bounds the input
degree of the product \emph{in $\mathcal A_\ell$} by
$d=k(m_{\mathrm{test}}+2(\ell-1))$. Thus the product satisfies precisely
the degree hypothesis \eqref{eq:general-product-degree} of the common
routine. Adding factors equal to one with scope $\{v\}$ ensures that
all declared variables occur in the construction.

Let $H(T)\in\mathcal A_\ell[T]$ be \eqref{eq:general-count-polynomial}
for these factors. Its $V$-coefficients at $T=0$ are integers because
all replacements restore their Boolean inputs at zero. By the same
lemma, summing their values gives
\begin{equation}\label{eq:origin-residue}
 \deg_T H\le d_H:=kR(m_{\mathrm{test}}+2(\ell-1)),\qquad
 \mathcal S_\ell(H(0))\equiv N(\mathcal P)\pmod{2^\ell}.
\end{equation}
Consequently the least nonnegative residue of $\mathcal S_\ell(H(0))$
is the exact count. Interpolation takes place over the rationals;
the congruence is needed only on Boolean inputs at $T=0$.

\subsection{Cost of evaluating the factors}\label{subsec:one-query-cost}
\begin{proposition}\label{prop:count}
Let a list of degree-at-most-$k$ polynomial equations on $n$ variables
and a design satisfying Definition~\ref{def:layout} for their factors
be given. Let $S\ge1$ bound the total length of the monomial lists and
factor scopes, and use any $\ell$ with $2^\ell>2^n$. With $d_H$ from
\eqref{eq:origin-residue} and $q,J$ from \eqref{eq:hasse-order},
$N(\mathcal P)$ can be computed deterministically in
\[
 \poly(n,m_{\mathrm{test}},\ell,D,Q,R,J,r,k,S)\,
 C_q(2D+1)^{2\tau n}2^{2n/r}
\]
bit operations and $\poly(n,m_{\mathrm{test}},\ell,D,Q,R,J,r,k,S)$
bits of working space.
\end{proposition}
\begin{proof}
Apply Proposition~\ref{prop:general-count} with coefficients in
$\mathcal A_\ell$. At an evaluation point $t$, the routine uses
$\mathcal A_\ell[z]/(z^J)$, so a stored element has just $J\ell$
rational coefficients. To evaluate factor $i$ at a fixed Boolean
substitution $\vec X=\mathbf1_U$ in \eqref{eq:jet-substitution}, first
evaluate each listed monomial by multiplying its at most $k$ substituted
inputs, then add the results to get $L_i$. Use this value in
\eqref{eq:lifted-factor}, successively multiplying by $h(L_i)$ to
obtain its powers. This takes polynomially many rational operations in
the displayed parameters and never enumerates assignments to the entire
scope $I_i$. The polynomials $e_j$ are computed once by
Lemma~\ref{lem:rational-idempotent}.

For bit complexity, the rows have common denominator
$d_{\mathrm{den}}=(R-1)!Q!$. Each substituted monomial has denominator
dividing $\Delta=d_{\mathrm{den}}^k$, every lifted factor has denominator
dividing $\Gamma=\Delta^{2\ell-1}$, and their product has denominator
dividing $\Omega=\Gamma^{m_{\mathrm{test}}}$. Thus exponentially many
summands can be accumulated over one denominator.
Appendix~\ref{app:arithmetic} bounds the bit lengths in these sums by
\begin{equation}\label{eq:sum-bit-bound}
 B_{\mathrm{sum}}=\poly(n,m_{\mathrm{test}},\ell,k,Q,\log(D+2),\log(S+2)).
\end{equation}
For each $0\le s<\ell$ we interpolate the rational polynomial
$[V^s]H(T)$ from its $QJ$ Taylor coefficients. The appendix verifies
polynomial bit cost for this interpolation and the final integer
remainder in \eqref{eq:origin-residue}. The $O(QJ\ell)$ stored
coefficients, the design and the sequential enumerations in
Proposition~\ref{prop:general-count} give the stated space bound.
\end{proof}

\subsection{Constructing the forms and completing the proof}\label{subsec:sparse-queries}
Each sparse polynomial reads few variables, but one variable might
occur in many equations. We first fix the values of the few variables
with the largest numbers of occurrences. On each resulting branch we
can construct the design required by Proposition~\ref{prop:count}.

\begin{proof}[Proof of Theorem~\ref{thm:overview-sparse-polynomials}]
Let $\mathcal P$ be the supplied polynomial system. An empty list of
equations gives $2^n$ common zeros; a constant equation $1=0$ gives
none. Discard equations $0=0$. Include a neutral factor equal to one
with scope $\{v\}$ for each declared variable $v$, and write
\[
 M=\sum_{f\in\mathcal F}|I_f|
\]
for the total number of factor--variable incidences. The input
bounds imply $M=n(\log n)^{O_{k,c}(1)}$, and every scope has
$(\log n)^{O_{k,c}(1)}$ variables. A particular variable, however,
may occur in many of these scopes.

Put $\lambda=\lceil\log_2 n\rceil$ and
\[
 b_0=\left\lceil\frac Mn\right\rceil\lceil\sqrt\lambda\rceil.
\]
Let $S\subseteq[n]$ be the variables belonging to more than $b_0$
scopes. For each $b\in\{0,1\}^S$, we fix $x|_S=b$ and count the
completions on $[n]\setminus S$; we call this restricted problem a
branch. Since $|S|\le M/b_0\le n/\sqrt\lambda$, there are at most
$2^{n/\sqrt\lambda}$ branches.
Each branch has the same number $n'$ of free variables, with
\[
 n'\ge n-\frac n{\sqrt\lambda}\ge\frac n2
 \qquad(n\ge20).
\]
Substitute the fixed bits in every $P_i$ over $\mathbb F_2$ and
combine duplicate monomials modulo two before forming its integer
lift. Neither degree nor the number of monomials increases. A constant
equation can again be handled immediately. The branches partition the
Boolean cube, so their common-zero counts add to $N(\mathcal P)$.

To apply Section~\ref{sec:construction}, remove the fixed variables from the
scopes and relabel the free variables by $[n']$.
Write $I'_f\subseteq[n']$ for the restricted
scopes and $M'=\sum_f|I'_f|$ for their total incidence count.
Let $b$ be the maximum factor incidence of a free variable
and let $w=\max_f|I'_f|$. Then $b\le b_0$,
and both $b$ and $w$ are bounded by a fixed power of $\log n'$.
The remaining neutral factors ensure $M'\ge n'$.
Set
\[
 \lambda'=\lceil\log_2 n'\rceil,\qquad
 \nu'=\lceil\log_2\lambda'\rceil,
\]
and choose the smallest integer $\beta\ge1$ with
$b,w\le(\lambda')^\beta$. For fixed $k,c$, the possible values
of $\beta$ are bounded by a constant for all sufficiently large
$n$. We apply Lemma~\ref{lem:incidence-parameters} to the restricted
scopes $(I'_f)$ on $[n']$, with incidence count $M'$, using
\[
 r=\left\lfloor\frac{\sqrt{\lambda'}}{(\nu')^2}\right\rfloor,
 \qquad Q=\left\lfloor\frac{\lambda'}{128\nu'}\right\rfloor,
 \qquad R=(\beta+3)\lceil\sqrt{\lambda'}\rceil.
\]
If $r<2$ or $Q\le R$, use the exhaustive-search fallback below
before forming $\tau$, $\epsilon$, or the parity interpolation
interval $\mathcal I$.
Otherwise set
\[
 \tau=\frac1{r\lambda'},\qquad
 \epsilon=\frac1{br^2\lambda'},\qquad D=r^{2Q},
\]
and carry out the remaining feasibility checks from that lemma.
For all sufficiently large $n$, Lemma~\ref{lem:layout} supplies
the required rows and measurement matrices, with
\[
 r=\Theta\!\left(\frac{\sqrt{\log n'}}{(\log\log n')^2}\right),
 \qquad Q=\Theta\!\left(\frac{\log n'}{\log\log n'}\right),
 \qquad R=O_{k,c}(\sqrt{\log n'}),
 \qquad D\le(2n')^{1/128}.
\]

On every branch we may use the original precision $\ell=n+1$,
since even the unrestricted count is smaller than $2^\ell$. As
$n'\ge n/2$, both $\ell$ and $m_{\mathrm{test}}$ are $O_c(n')$.
Thus $d_H=O_{k,c}(n'R)$, $J=O_{k,c}(n'R/Q)+1$, and
\eqref{eq:three-costs}, in dimension $n'$, has exponent
\[
 O_{k,c}\!\left(\frac{n'(\log\log n')^2}{\sqrt{\log n'}}\right)
 =O_{k,c}\!\left(\frac{n(\log\log n)^2}{\sqrt{\log n}}\right).
\]
All substitution data, coefficient arrays, and interpolation systems
have total representation length $n^{O_{k,c}(1)}$ bits.
Multiplying the per-branch running time by at most
$2^{n/\sqrt\lambda}$ leaves the displayed exponential bound
unchanged, so summing the branch answers gives the required running time.

To implement the construction for every input size, the algorithm
checks its numerical hypotheses using integer arithmetic.
In addition to the preliminary guards above, it checks
$2(b+w)D^2\le M'$ and $2Qr^2\le n'$ from
Lemma~\ref{lem:incidence-labels}, the endpoints of $\mathcal I$,
$R\ge32$, $6R\le Q$, and the binomial tail bound in
\eqref{eq:incidence-tail}, which can be tested exactly.
If any check fails, the algorithm abandons the branched computation
and checks the original equations directly on all $2^n$ assignments. For fixed
$k,c$, the bounds just proved and
Lemma~\ref{lem:incidence-parameters} show that a failure can occur
only for finitely many $n$. This fallback is therefore absorbed
in the theorem's constants.

To combine the branch counts within the stated space bound, we
process the branches one at a time. We initialize an integer
accumulator $Z=0$ and add each branch's answer to it. The construction and
Proposition~\ref{prop:count} use $n^{O_{k,c}(1)}$ bits of space on
each branch.
Disjointness gives $0\le Z\le2^n$ throughout, and the final value
is $N(\mathcal P)$, as claimed.
\end{proof}

\section{Reducing \texorpdfstring{$\#k$-SAT}{\#k-SAT} to counting common zeros}\label{sec:hashes}\label{subsec:sparse-hashes}
Given a sparse $k$-CNF $F$ with at most $Bn$ clauses, where $B$ is
polylogarithmic in $n$, we construct $O(n)$ sparse polynomial
equations on its original $n$ variables whose common zeros are exactly
its satisfying assignments. One equation per clause could require
$Bn$ equations. Instead, each equation will test the parity of the
violations of a short list of clauses. We use
Theorem~\ref{thm:overview-sparse-polynomials} both to choose these
equations and to obtain the final count.

Let $m$ be the number of indexed clauses and $v_e(x)$ the violation bit
of clause $e$. As a polynomial over $\mathbb F_2$, $v_e$ is a product
of the factors $1+x_v$ for positive literals and $x_v$ for negative
literals. A tautological clause has $v_e=0$ and an empty clause has
$v_e=1$. After removing repeated literals, $\deg v_e\le k$ and $v_e$
expands to at most $2^k$ monomials. Put $v(x)=(v_1(x),\ldots,v_m(x))$.
For a binary matrix $A$ with $m$ columns, row $i$ specifies the equation
\begin{equation}\label{eq:hash-query}
 P_i(x):=\sum_{e:A_{ie}=1} v_e(x)=0\qquad\text{over }\mathbb F_2.
\end{equation}
Write $\mathcal P_A$ for this system and $N(A)=N(\mathcal P_A)$ for its
number of common zeros. Every satisfying assignment passes every row.
Hence $N(A)=\#F+D(A)$, where $D(A)$ counts the nonsatisfying assignments
still passing. We do not know $\#F$, but it is the same for every
candidate next row: the row minimizing $N$ also minimizes $D$.

We represent a test row by a list of pairs $(e,c)$ with
$e\in[m]$ and $c\in\{0,1\}$, summing coefficients modulo $2$ if a
clause index is repeated. The length of this list counts all pairs,
including repeated indices and pairs with coefficient zero. A row of
list length $s$ thus reads at most $ks$ variables before cancellation.

\subsection{Initial tests that exclude small violation sets}

If an assignment violates only one of many clauses, a test sampling
a short list of clauses is unlikely to notice it. We therefore first
construct a matrix $A^{(0)}$ that rejects every nonzero violation
vector with small support. Every nonsatisfying assignment that passes
these initial tests must violate many clauses. A further test that
samples a short list of clauses can then reject each such assignment
with constant probability.

We use the standard edge-based Tanner code: bits are assigned to
the edges of an expander, and the bits incident to each vertex
must form a word of a prescribed local linear code
(see
Tanner~\cite[Section~II]{Tanner81} for the local constraints and
Sipser and Spielman~\cite[Sections~IV and~VI]{SS96} for the expander construction).
The usual local-distance and expansion argument gives the needed
lower bound on the weight of a nonzero codeword. The proof below
constructs the graph and local code deterministically, with parameters
that meet our bounds on the number and length of the tests.

\begin{lemma}\label{lem:sparse-checks}
Let $n,m,B$ be positive integers with $m\le Bn$, and put
\[
 \mu=\lfloor\log_2 m\rfloor+1,\qquad
 P=20000B^2\mu^2,\qquad D_0=320000B^2\mu^3.
\]
There is a deterministic construction of a binary matrix
$A^{(0)}$ with $m$ columns and at most $3n$ rows such that every row
has at most $D_0$ nonzero entries and
\[
 z\in\{0,1\}^m\setminus\{\vec{0}\},\quad
 A^{(0)}z=\vec{0}\pmod2
 \quad\Longrightarrow\quad
 |\operatorname{supp}z|\ge m/P.
\]
The construction uses $\exp(\poly(B,\log(m+2)))$
bit operations and $\poly(n,m,B)$ bits of working space.
\end{lemma}

\begin{proof}
We construct a bipartite graph with between $m$ and $2m$ edges,
using its edges as temporary binary coordinates. Checks at each vertex
will force every vertex touched by a nonzero edge to have many nonzero
incident edges; a mixing bound will then force large total weight.
At the end, we keep $m$ edge coordinates and fix the rest to zero.
Let
\[
 d_G=\min(m,D_0),
 \qquad
 q_G=\min\{2^a:a\in\mathbb Z_{\ge0},\ 2^a d_G\ge m\}.
\]
Then $m\le q_Gd_G<2m$. Write $q_G=2^{\ell_G}$ and take two copies
of $\{0,1\}^{\ell_G}$ as the vertex sets. For each left vertex $u$
and each port $j\in[d_G]$, put an edge from $u$ to $u\oplus s_j$,
where $\oplus$ denotes bitwise addition modulo $2$ and the shifts
$s_1,\ldots,s_{d_G}\in\{0,1\}^{\ell_G}$ will be chosen below.
Edges are indexed by the pairs $(u,j)$; parallel edges remain
distinct. Every vertex on either side has one incident edge at
each port $j$, so the graph is $d_G$-regular.

To obtain the mixing estimate \eqref{eq:hash-mixing}, we choose
the shifts so that every parity of a nonempty set of coordinates
is nearly balanced. For a nonzero vector
$b\in\{0,1\}^{\ell_G}$, the bit $b\cdot s_j\bmod2$ is the parity
of those coordinates of $s_j$ where $b$ equals $1$.
With $\varepsilon=1/(200B\mu)$, we require
\begin{equation}\label{eq:hash-walsh}
 \Bigl|\sum_{j=1}^{d_G}(-1)^{b\cdot s_j}\Bigr|
 \le\varepsilon d_G
 \qquad
 \bigl(b\in\{0,1\}^{\ell_G}\setminus\{\vec{0}\}\bigr).
\end{equation}
The sum in \eqref{eq:hash-walsh} is the number of indices $j$
with even parity minus the number with odd parity. Thus, for
every nonzero $b$, each parity occurs at a fraction of indices
between $(1-\varepsilon)/2$ and $(1+\varepsilon)/2$.
A list of shifts with this property is called
$\varepsilon$-biased~\cite[Definitions~2.1--2.2]{NN93}.

If $q_G=1$, there is no condition to check. Otherwise $d_G=D_0$.
To show that suitable shifts exist, we choose them independently
and uniformly at random. For each fixed nonzero $b$, the signs
$(-1)^{b\cdot s_j}$ are independent and uniform in $\{-1,1\}$.
Hoeffding's inequality bounds the probability of violating
\eqref{eq:hash-walsh} for this $b$ by
$2\exp(-\varepsilon^2d_G/2)$. A union bound over $b$ gives total
failure probability at most
\[
 2q_G\exp(-\varepsilon^2d_G/2)
 =2q_G\exp(-4\mu)<1,
\]
where $q_G<2m<2^{\mu+1}$. Exhaustively enumerating the shift tuples
and checking \eqref{eq:hash-walsh} therefore finds a valid tuple in
$\exp(O(d_G\log(m+2)))$ time.

We next derive the mixing estimate from \eqref{eq:hash-walsh}.
Let $\mathsf A_G$ be the $q_G\times q_G$ matrix with
$\mathsf A_G[u,v]=|\{j\in[d_G]:u\oplus s_j=v\}|$; its entries
count edges from left vertices $u$ to right vertices $v$.
Both sides have the same index set $\{0,1\}^{\ell_G}$, on which
the functions $\chi_b(u)=(-1)^{b\cdot u}$ form an orthogonal basis.
For every $b,u\in\{0,1\}^{\ell_G}$,
\[
 (\mathsf A_G\chi_b)(u)
 =\sum_{j=1}^{d_G}\chi_b(u\oplus s_j)
 =\chi_b(u)\sum_{j=1}^{d_G}(-1)^{b\cdot s_j}.
\]
Thus each $\chi_b$ is an eigenvector: the constant function
$\chi_{\vec{0}}$ has eigenvalue $d_G$, while
\eqref{eq:hash-walsh} bounds all other eigenvalues in absolute value
by $\varepsilon d_G$.
For sets $U$ of left vertices and $V$ of right vertices, let
$e_G(U,V)$ count the edges between them, including multiplicity.
Decomposing the indicator vectors of $U,V$
into their constant and orthogonal parts and applying
Cauchy--Schwarz gives
\begin{equation}\label{eq:hash-mixing}
 e_G(U,V)\le
 \frac{d_G|U||V|}{q_G}
 +\varepsilon d_G\sqrt{|U||V|}.
\end{equation}

To specify the local code, we put
\[
 c_G=\left\lceil\frac{d_G}{8B}\right\rceil,
 \qquad \delta=\frac1{100B\mu}.
\]
We need a binary matrix $A_{\mathrm{loc}}$ with $c_G$ rows and
$d_G$ columns such that every nonzero word in its kernel modulo $2$
has weight at least $\delta d_G$. To prove that such a matrix exists,
we consider a matrix whose entries are independent uniform bits.
For each fixed nonzero word, one of
its nonzero coordinates makes the parity in each row uniform;
independence of the rows therefore gives probability $2^{-c_G}$
that the word lies in the kernel.
Set $h=\lceil\delta d_G\rceil-1$. If $h=0$, there are
no nonzero words of weight less than $\delta d_G$. Otherwise their
number is at most
\[
 \sum_{j=1}^{h}\binom{d_G}{j}
 \le(h+1)(2d_G)^h
 \le(2d_G)^{2h}
 <2^{d_G/(25B)}.
\]
For the last inequality, use $h<\delta d_G$, $d_G\le m<2^\mu$,
and $\mu+1\le2\mu$. Since $c_G\ge d_G/(8B)$, a union bound shows
that a suitable $A_{\mathrm{loc}}$ exists. Enumerating the
$2^{c_Gd_G}$ binary matrices and testing all words of weight less
than $\delta d_G$ finds one in
$\exp(\poly(B,\log(m+2)))$ bit operations.

At every vertex on both sides, impose the $c_G$ rows of
$A_{\mathrm{loc}}$ on its incident edge coordinates, ordered by
their ports. These constraints define a Tanner code with local
code $C_{\mathrm{loc}}=\ker_{\mathbb F_2}A_{\mathrm{loc}}$.
Its incidence graph has one bit node for every edge of our graph
and one local-code node for every vertex; each bit participates
in the constraints at its two endpoints.
Consider a nonzero edge word accepted by all these
checks. Let $U,V$ be the vertices touched by its nonzero edges on
the two sides, and let $h'$ be its weight. Each vertex in $U\cup V$
is incident to at least $\delta d_G$ nonzero edges, so
$h'\ge\delta d_G\max(|U|,|V|)$. Therefore
\[
 \delta d_G\sqrt{|U||V|}
 \le h'\le e_G(U,V)
 \le\frac{d_G|U||V|}{q_G}
       +\varepsilon d_G\sqrt{|U||V|}.
\]
Both $U$ and $V$ are nonempty. Dividing by
$d_G\sqrt{|U||V|}$ yields
$\sqrt{|U||V|}\ge(\delta-\varepsilon)q_G$, and hence
\[
 h'\ge\delta(\delta-\varepsilon)q_Gd_G
 =\frac{q_Gd_G}{20000B^2\mu^2}\ge\frac mP.
\]

Shorten this Tanner code by keeping any $m$ of the $q_Gd_G$ edge
coordinates, identifying them with $[m]$, and setting the remaining
coordinates to zero. Restricting all
the vertex checks to the retained coordinates gives $A^{(0)}$.
Any word accepted by $A^{(0)}$ extends by zeros to an accepted edge
word, so it has the required weight. Every row has at most
$d_G\le D_0$ nonzero entries. There are $2q_Gc_G$ rows. If $q_G=1$,
then $d_G=m$ and
\[
 2c_G\le\frac{m}{4B}+2\le\frac n4+2\le3n.
\]
If $q_G>1$, then $d_G=D_0\ge8B$, and
\[
 2q_Gc_G\le\frac{q_Gd_G}{4B}+2q_G
 \le\frac{q_Gd_G}{2B}<\frac mB\le n.
\]
The searches over shifts, local matrices, and test words are
sequential. Storing the current choices and the final rows uses
$\poly(n,m,B)$ bits of working space.
\end{proof}

\subsection{Choosing additional equations by counting common zeros}
After the initial checks, every nonsatisfying assignment still passing
violates at least $m/P$ clauses. This lets a short random test catch
each such assignment with constant probability. To make the choice
deterministic we use the averaging principle underlying conditional
expectations~\cite{Raghavan88}.

\begin{lemma}\label{lem:greedy-hashes}
With $P,D_0$ and $A^{(0)}$ from Lemma~\ref{lem:sparse-checks}, a
deterministic procedure appends $3n$ rows of list length $P$ and
obtains a matrix $A$ with $N(A)=\#F$. It uses at most $3n(2m)^P$
common-zero counts. Every candidate system has at most $6n$ equations,
each involving at most $2^k\max(D_0,P)$ monomials of degree at most $k$.
\end{lemma}
\begin{proof}
At a stage with current matrix $A$, enumerate the ordered lists
\[
 \gamma=((e_1,c_1),\ldots,(e_P,c_P))
 \in\mathcal C:=([m]\times\{0,1\})^P.
\]
The list $\gamma$ represents the binary row $h_\gamma$ with
\[
 (h_\gamma)_e=
 \Bigl(\sum_{j:e_j=e}c_j\Bigr)\bmod2
 \qquad(e\in[m]).
\]
There are $(2m)^P$ lists; distinct lists are still counted separately
when they represent the same row. Write $A;h_\gamma$ for the matrix obtained by appending $h_\gamma$ to $A$.

Fix a nonsatisfying assignment $x$ accepted by $A$. The initial
rows remain in $A$, so
$|\operatorname{supp}v(x)|\ge m/P$.
For a uniform list $\gamma$, the probability that none of
$e_1,\ldots,e_P$ belongs to this support is at most
\[
 (1-1/P)^P\le e^{-1}<1/2.
\]
Conditional on the indices hitting the support, choose one hit
position $j$. After fixing every coefficient except $c_j$, the
uniform bit $c_j$ makes $h_\gamma\cdot v(x)$ uniform modulo $2$.
This remains true when some clause indices are repeated.
Thus, for each such $x$, at least a quarter of the candidate lists
give a row that rejects $x$.

Summing this bound over the nonsatisfying assignments still passing,
we find
\[
 \mathbb E_\gamma D(A;h_\gamma)\le\tfrac34 D(A).
\]
For every candidate, compute $N(A;h_\gamma)$ by counting the common
zeros of its polynomial system. Append a candidate attaining the
minimum, breaking ties by enumeration order. Since
$N(A;h_\gamma)=\#F+D(A;h_\gamma)$ for every $\gamma$, the chosen row
leaves at most $\tfrac34 D(A)$ nonsatisfying assignments. After $3n$
rounds at most $(3/4)^{3n}2^n=(27/32)^n<1$ remain; their number is
an integer, so it is zero. The procedure runs for a fixed number of
rounds and never needs to know $D(A)$ or $\#F$.

The initial matrix has at most $3n$ rows, and every candidate is
evaluated with at most $3n$ additional rows. A row listing $s$
clauses expands, by \eqref{eq:hash-query}, to at most $2^k s$
monomials on the original variables; duplicates cancel over
$\mathbb F_2$. These observations give the claimed size and query
bounds.
\end{proof}

\subsection{Counting one sparse formula}\label{subsec:count-sparse}
Suppose $n\ge20$ and $1\le m\le Bn$, where $B$ is bounded by a fixed
power of $\log n$ depending only on $k$. Construct the initial matrix
by Lemma~\ref{lem:sparse-checks}. This uses
$\exp((\log n)^{O_k(1)})$ bit operations and polynomial space.
Both $P$ and $D_0$ are $(\log n)^{O_k(1)}$, so every candidate in
Lemma~\ref{lem:greedy-hashes} is an instance of
Theorem~\ref{thm:overview-sparse-polynomials} with a single fixed
$c=c(k)$. This applies to discarded candidates as well as the final
system: the counter requires only the number, degree and sparsity of
the equations. Expanding each row and combining monomials costs
polynomial time and space for fixed $k$.

At most $3n(2m)^P+1=\exp((\log n)^{O_k(1)})$ calls suffice, including
one final count. Each call takes
$2^{O_k(n(\log\log n)^2/\sqrt{\log n})}$ bit operations. Since any
fixed power of $\log n$ is $o(n(\log\log n)^2/\sqrt{\log n})$, the
total time, including construction and candidate comparisons, is
\begin{equation}\label{eq:sparse-formula-cost}
 (n+m)^{O_k(1)}2^{O_k(n(\log\log n)^2/\sqrt{\log n})}.
\end{equation}
The final count is $\#F$ by the greedy lemma. A formula with no clauses
or containing an empty clause is handled directly. Candidates are
examined sequentially; only the current rows, a candidate, the best
row and its count need be kept in addition to the counter's polynomial
working space.

\subsection{Returning to a general formula}\label{subsec:general-reduction}

We use disjoint sparsification to partition the satisfying
assignments among sparse formulas on the same $n$ declared
variables. The preceding algorithm counts each of these formulas.
The parameter $\sigma$ controls a tradeoff: making it smaller reduces
the number of formulas but increases their occurrence bound $B$.
Our solver permits $B$ to grow as a fixed power of $\log n$, so we
can let $\sigma$ tend to zero while keeping both the number of
formulas and the cost per formula within the desired time bound.

\begin{lemma}\label{lem:sparsify}
Fix $k\ge2$. Given a $k$-CNF on $n$ declared variables with $m$
clauses and a rational $0<\sigma\le1$, a deterministic algorithm
constructs a tree of $k$-CNFs on the same variables. Let $L_\sigma$
be the total binary encoding length of the supplied numerator and
denominator of $\sigma$.
An assignment satisfies the input exactly when it satisfies one
leaf formula, and it cannot satisfy two distinct leaves.
The tree has
\[
 \operatorname{poly}_k(n,\sigma^{-1})\,2^{\sigma n}
\]
nodes and depth $\poly_k(n,\sigma^{-1})$.
In every leaf, each variable occurs at most $B$ times, where $B$
is an explicitly computed integer satisfying
\[
 B=O_k\!\Bigl(\bigl[\sigma^{-1}\log(2/\sigma)\bigr]^{k-1}\Bigr).
\]
Input normalization uses $\poly_k(n,m)$ bit operations.
Constructing the numerical parameters uses $\poly_k(L_\sigma)$
bit operations. Thereafter, processing each node uses
$\poly_k(n,\log(2/\sigma))$ bit operations.
The input count is the sum of the leaf counts.
\end{lemma}
Appendix~\ref{app:sparsify} proves the lemma, including the
disjointness that justifies adding the leaf counts.

\begin{proposition}\label{prop:interpolation-bound}
For each fixed $k\ge2$, the interpolation algorithm counts the
satisfying assignments of a $k$-CNF on $n\ge20$ declared variables
with $m$ clauses in $(n+m)^{O_k(1)}2^{O_k(\rho(n))}$ bit operations
and $(n+m)^{O_k(1)}$ bits of space.
\end{proposition}
\begin{proof}
We first normalize the input in $(n+m)^{O_k(1)}$ time by deleting repeated
literals, tautological clauses, duplicate clauses, and clauses
containing another clause. We retain all $n$ declared variables.
An empty clause gives count zero, and a formula with no clauses
gives count $2^n$. We handle $n<20$ by exhaustive search.
For $n\ge20$, we next select the sparsification parameter. Define
\[
 \lambda_n=\lceil\log_2 n\rceil,\qquad
 \nu_n=\lceil\log_2\lambda_n\rceil,\qquad
 s=\left\lfloor\frac{\sqrt{\lambda_n}}{\nu_n^2}\right\rfloor.
\]
We compute $s$ by integer comparisons, taking the largest
nonnegative integer satisfying $s^2\nu_n^4\le\lambda_n$.
If $s<2$, we use exhaustive search;
$\sqrt{\lambda_n}/\nu_n^2$ tends to infinity, so there are only
finitely many such sizes. Otherwise we apply Lemma~\ref{lem:sparsify}
with $\sigma=1/s$. The tree has at most
$2^{n/s}\operatorname{poly}_k(n,s)$ nodes, and its leaves have
occurrence bound
\[
 B=O_k\bigl((s\log s)^{k-1}\bigr)=(\log n)^{O_k(1)}.
\]
Each leaf uses the original $n$ variables and has at most $Bn$
nonempty clauses. We count each leaf by the sparse-formula algorithm
of Section~\ref{subsec:count-sparse}, whose running time is given by
\eqref{eq:sparse-formula-cost}. Leaves with no clauses or containing
an empty clause are handled directly.
The clause count in that application is the number of clauses in
the leaf; $m$ in the final bound remains the input clause count.

For $s\ge2$, the floor in its definition gives
\[
 \frac ns=O\!\left(\frac{n\nu_n^2}{\sqrt{\lambda_n}}\right)
 =O(\rho(n)).
\]
Thus both the number of leaves and the time to count each leaf
have exponent $O_k(\rho(n))$. Their polynomial factors, together
with normalization and the work at the tree nodes, are bounded by
$(n+m)^{O_k(1)}$. The total number of bit operations is therefore
\[
 (n+m)^{O_k(1)}2^{O_k(\rho(n))}.
\]
The finite exhaustive-search cases are absorbed in the constants.
All parameters, initial checks, and additional rows are computed
by the deterministic procedures above; every counting query uses
the common-zero algorithm of Theorem~\ref{thm:overview-sparse-polynomials}.

To bound the space used by the full algorithm, we traverse the
sparsification tree depth first and count one leaf at a time.
The current path has $\poly_k(n,s)$ nodes, and each normalized
formula has a $\poly_k(n)$-bit encoding. Since
$s\le\sqrt{\lceil\log_2 n\rceil}$, storing this path and counting one
leaf use $\poly_k(n,m)$ bits. Disjointness keeps the sum of the
processed leaf counts between zero and $2^n$, so its accumulator
uses at most $n+1$ bits. Thus the total space is $\poly_k(n,m)$ bits.
\end{proof}

\appendix

\section{Partitioning the satisfying assignments}\label{app:sparsify}

Fix $k\ge2$ and a rational $0<\sigma\le1$.
We prove Lemma~\ref{lem:sparsify} by repeatedly splitting a formula
into two cases. Both children use the same $n$ variables, and every
satisfying assignment of the parent satisfies exactly one child.
We follow the rule for choosing a shared set of literals and the
insertion accounting of~\cite[Section~6]{CIP}.
The refinement that makes the two cases disjoint is standard in exact
counting~\cite[Appendix~A]{DHMTW}.

Throughout this appendix, a clause is a set of literals and denotes their
disjunction. Its \emph{width} is the number of literals it contains.
We delete tautological clauses, repeated clauses, and clauses
containing another clause. Thus the remaining clauses form an antichain
under inclusion. We keep all $n$ declared variables and do not propagate
unit clauses. An empty clause gives count zero, and the empty formula gives
count $2^n$.

\subsection{The branching rule}

Fix an integer $M\ge2$. We will obtain an occurrence bound
$B=O_k(M^{k-1})$ at every leaf, then choose $M$ so that the tree has
at most $\poly_k(n,\sigma^{-1})2^{\sigma n}$ nodes. Put
\[
 \theta_j=M^j\qquad(0\le j<k).
\]
Writing $F$ for the current family of clauses, define
\[
 \deg_c(H)=\#\{C\in F:|C|=c,\ H\subseteq C\}
\]
for each literal set $H$. We branch whenever a nonempty proper subset
$H$ of a width-$c$ clause satisfies
\begin{equation}\label{eq:spar-violation}
 \deg_c(H)\ge\theta_{c-|H|}.
\end{equation}
The algorithm chooses the smallest possible $c$, and then the largest possible $|H|$;
break any remaining ties deterministically.
Thus a nonempty shared literal set $H$ leaving $j=c-|H|$ other
literals must occur in at least $M^j$ clauses before we branch on it.

Let $H\cup P_1,\ldots,H\cup P_z$ be all the width-$c$ clauses containing
the chosen $H$, and let $G$ consist of the other clauses. Put
$j=c-|H|$. Here $P_a$ is the set of literals left after removing
$H$ from the $a$th selected clause, so each $P_a$ has width $j$
and $z\ge\theta_j$.
The two children are
\begin{equation}\label{eq:spar-children}
 F_A=G\wedge H,\qquad
 F_B=G\wedge\bigwedge_{a=1}^zP_a
          \wedge\bigwedge_{\ell\in H}\{\neg\ell\}.
\end{equation}
We restore the antichain condition in each child by removing
clauses made redundant by its new clauses.
The sets $P_a$ may overlap.
The satisfying assignments of the children are disjoint:
$F_A$ requires some literal of $H$ to be true, whereas $F_B$
requires every literal of $H$ to be false.

\begin{lemma}\label{lem:spar-branch}
The children in \eqref{eq:spar-children} partition the satisfying
assignments of their parent. Every new clause has width less than $c$.
The $A$-child inserts one new clause, and the $B$-child inserts at least
$\theta_j$ new clauses of width $j$. All newly inserted clauses survive
the immediate normalization. Every old clause removed in either child
contains a newly inserted strict subset.
\end{lemma}
\begin{proof}
Every assignment satisfies exactly one of the conditions
\emph{some literal of $H$ is true} and
\emph{every literal of $H$ is false}.
In the first case, all selected clauses are satisfied, leaving
$G\wedge H$. In the second, each selected clause reduces to $P_a$,
and the unit clauses $\{\neg\ell\}$ enforce this case.
Thus the two children partition the parent's satisfying assignments.

The old antichain contains no clause included in $H$ or in any $P_a$:
such a clause would be a strict subset of $H\cup P_a$.
Thus $H$ and the distinct equal-width clauses $P_a$ are new.
No $P_a$ contains a variable of $H$, since its parent is nontautological.
Consequently, none of the unit clauses $\{\neg\ell\}$, $\ell\in H$,
is a subset of any $P_a$.
Any unit clause $\{\neg\ell\}$ already present is retained and
is not counted as a new insertion.
The remaining new unit clauses and the clauses $P_a$ all survive.
Each selected old clause contains the newly inserted clause $H$
for child $A$, or its newly inserted subset $P_a$ for child $B$.
Every other removed clause contains a newly inserted strict subset
by the normalization rule.
\end{proof}

\subsection{Counting insertions}
To bound the tree, we count every clause introduced along one path,
including clauses later deleted. Clauses present in the input are
excluded from this count. By Lemma~\ref{lem:spar-branch}, each step
inserts a clause, so bounding the total number of insertions also
bounds the path length.

For this accounting, a clause is marked when a branch introduces it.
First we bound how many
marked clauses can still be present and contain a given literal set.
The smallest-width priority controls those present before a branch;
the largest-$|H|$ priority controls those introduced by that branch.

\begin{lemma}\label{lem:spar-marked-degree}
At every node, for $1\le i<j<k$ and every literal set $S$ of size $i$,
fewer than $2\theta_{j-i}$ marked clauses of width $j$ that are
still present contain $S$.
\end{lemma}
\begin{proof}
Initially there are no marked clauses. It suffices to consider a branch
that inserts clauses of width $j$. Its selected width $c$ is larger than
$j$. Before insertion, fewer than $\theta_{j-i}$ current width-$j$
clauses contain $S$: otherwise the smallest-width priority would select
a width at most $j$.

Choosing child $A$ inserts only one clause.
Suppose child $B$ inserts clauses $P_a$ of width $j$.
If none of the $P_a$ contains $S$, the number of new width-$j$ clauses
containing $S$ is zero. Otherwise $S$ lies in a petal and is therefore
disjoint from $H$. In this case $P_a$ contains $S$ exactly when the
selected clause $H\cup P_a$ contains $H\cup S$. Since $0<i<j$,
$H\cup S$ is larger than $H$ and is a proper subset of a selected
width-$c$ clause.
The priority for the largest shared set therefore gives
\[
 \#\{a:S\subseteq P_a\}
 =\deg_c(H\cup S)<\theta_{c-|H\cup S|}
 =\theta_{j-i}.
\]
The other new clauses $\{\neg\ell\}$ have width one.
Thus the old and new clauses of width $j$ together satisfy the
asserted bound. Deletion cannot increase it.
\end{proof}

\begin{lemma}\label{lem:spar-insertion-bound}
Along any path or path prefix, the total number $T_j$ of width-$j$
insertions satisfies $T_j\le4(3M)^{j-1}n$ for $1\le j<k$.
\end{lemma}
\begin{proof}
The case $n=0$ is immediate, so assume $n\ge1$.
For the current path prefix, let $L_j$ be the number of marked
width-$j$ clauses still present, and let $D_j$ be the number of
width-$j$ insertions whose clauses have since been deleted.
Then $T_j=L_j+D_j$.
Units are never deleted, so $T_1\le2n\le4n$.
For $j\ge2$, sum Lemma~\ref{lem:spar-marked-degree} over the $2n$
single literals. This gives $L_j\le4n\theta_{j-1}$.

Whenever a marked clause of width $j$ is deleted, assign that deletion
to one newly introduced strict subset contained in it;
Lemma~\ref{lem:spar-branch} guarantees such a subset.
If the new clause has width $i<j$, Lemma~\ref{lem:spar-marked-degree}
shows that it was contained in fewer than $2\theta_{j-i}$ marked
clauses of width $j$ immediately before the branch.
Thus one insertion of a width-$i$ clause receives at most that
many deletions. Summing over the widths $i$ of the new clauses gives
$D_j\le2\sum_{i=1}^{j-1}\theta_{j-i}T_i$. Therefore
\begin{equation}\label{eq:spar-insertions}
 T_j=L_j+D_j\le4n\theta_{j-1}
       +2\sum_{i=1}^{j-1}\theta_{j-i}T_i.
\end{equation}
The first term counts clauses still present; the sum counts those that
were deleted. Dividing by $nM^{j-1}$ and applying induction gives
\[
 \frac{T_j}{nM^{j-1}}
 \le4+2\sum_{i=1}^{j-1}4\cdot3^{i-1}
 =4\cdot3^{j-1},
\]
as required.
\end{proof}

\subsection{The size of the tree}
We now convert Lemma~\ref{lem:spar-insertion-bound} into a bound on
the number of tree nodes. It controls both the length of a path
and the number of times that path chooses the $B$-child in
\eqref{eq:spar-children}. Write these bounds as $Cn$ and
$\Gamma n/M$, respectively, where
\[
 C=4\sum_{j=0}^{k-2}(3M)^j,\qquad
 \Gamma=4\sum_{j=0}^{k-2}3^j=2(3^{k-1}-1).
\]
Lemma~\ref{lem:spar-insertion-bound} gives depth at most $Cn$.
A choice of child $B$ with $|P_a|=j$ inserts at least $M^j$
clauses of width $j$, so a path contains at most
$4\cdot3^{j-1}n/M$ such choices.
In total, a path chooses $B$ at most $\Gamma n/M$ times.

A path with few choices of $B$ has a short description.
Because the branching rule is deterministic, a node is determined
by its depth and the positions at which its path chooses $B$;
every other position chooses $A$.
For $M\ge\Gamma$, this bounds the number of nodes by
\[
 (Cn+1)\sum_{a\le\lfloor\Gamma n/M\rfloor}\binom{Cn}{a}
 \le (Cn+1)^2
       2^{(\Gamma n/M)\log_2(4CM)}.
\]
Here $\Gamma n/M\le n\le Cn/4$.
For a positive integer $a$, use
$\binom{Cn}{a}\le(4Cn/a)^a$; this upper bound increases for
$a\le Cn/4$.
There are at most $Cn+1$ summands.
The case $\Gamma n/M<1$ is immediate.

We choose $M$ to make the exponent in this bound at most $\sigma n$.
Test powers of two $M\ge\Gamma$ in increasing order.
For each choice, compute $C$ and $h=\lceil\log_2(4CM)\rceil$,
and stop when
\[
 \Gamma h\le\sigma M.
\]
All comparisons are exact. Since $C=O_k(M^{k-2})$ and $\Gamma$
depends only on $k$, the first successful choice satisfies
\[
 M=O_k\bigl(\sigma^{-1}\log(2/\sigma)\bigr).
\]
The tree therefore has at most $(Cn+1)^2\,2^{\sigma n}$ nodes.

At a leaf, \eqref{eq:spar-violation} fails for every nonempty proper
subset of a clause.
A fixed literal belongs to fewer than $\theta_{c-1}$ width-$c$
clauses when $c\ge2$, and to at most one unit clause. Hence each variable
occurs at most
\[
 B=2\sum_{j=0}^{k-1}M^j
   \le4M^{k-1}
   =O_k\Bigl(\bigl[\sigma^{-1}\log(2/\sigma)\bigr]^{k-1}\Bigr).
\]
Thus every leaf has the required bound on occurrences per variable.
The repeated two-case partition also shows that each original
satisfying assignment occurs at exactly one leaf, so summing the
leaf counts gives the original count.

To implement the branching rule at a node, we compute $\deg_c(H)$
for its current formula. For each width-$c$ clause, we enumerate
its nonempty proper subsets $H$ and increment the counter indexed
by $(c,H)$. There are $O_k(n^k)$ possible nonempty normalized clauses,
each with at most $2^k$ subsets. The clause counters use
$O_k(\log(n+2))$ bits, and the thresholds use $O_k(\log M)$ bits.
Computing the counts, choosing a branch, and normalizing its children
therefore use $\poly_k(n,\log M)$ bit operations and bits of working
space per node. The bound on $M$ gives
$\log M=O_k(\log(2/\sigma))$.

With $L_\sigma$ as in Lemma~\ref{lem:sparsify}, the parameter search
examines $O_k(L_\sigma)$ powers of two. Its integer operands have
$O_k(L_\sigma)$ bits, so constructing the numerical parameters uses
$\poly_k(L_\sigma)$ bit operations and bits of working space.

\section{Exact arithmetic and space}\label{app:arithmetic}
Section~\ref{sec:construction} bounds the rational coefficients of the
substitution rows $\vec{P}_{f,v}(T)$. We complete the bit-cost and space
estimates in Proposition~\ref{prop:count} by bounding the lifted factors,
the sums used to compute the Taylor polynomials of $H$, and the final
interpolation. The essential point is that each sum uses a fixed
denominator. Its numerator grows with the number of summands, so its
bit length grows only with the logarithm of that number.
For any polynomial $G=\sum_\alpha c_\alpha \vec{X}^{\alpha}$ in finitely
many indeterminates, write $\|G\|_1=\sum_\alpha|c_\alpha|$ for its
coefficient norm.

\subsection{Integer coefficients of the lifted indicator}
\label{subsec:rational-lift-height}
We first bound the coefficients of the parity polynomials supplied
by Lemma~\ref{lem:rational-idempotent}. They occur in every equation
factor $\mathcal B_i$ in \eqref{eq:lifted-factor}, so their sizes
enter the bit-cost bounds for evaluating those factors.
For an integer $\ell\ge1$, recall $h(Y)=Y(Y-1)$ and the polynomials
from Lemma~\ref{lem:rational-idempotent}:
\[
 p_\ell(Y)=(1-Y)^\ell\sum_{j=0}^{\ell-1}
                    \binom{\ell+j-1}{j}Y^j
          =\sum_{j=0}^{\ell-1}e_j(Y)h(Y)^j,
 \qquad \deg e_j\le1.
\]
That lemma proves the parity congruence and constructs the $e_j$ by
successive monic division by $h$. Here we bound the integers occurring
in this construction.

\begin{lemma}\label{lem:rational-lift-height}
Write $e_j(Y)=a_j+b_jY$ for $0\le j<\ell$. Then $a_j,b_j\in\mathbb Z$ and
\[
 |a_j|,|b_j|\le2^{C\ell^2}\qquad(0\le j<\ell)
\]
for an absolute constant $C$.
Successive division of $p_\ell$ by $h$ constructs these polynomials
using $\poly(\ell)$ bit operations and bits of working space.
\end{lemma}
\begin{proof}
The coefficient-norm inequality
$\|fg\|_1\le\|f\|_1\|g\|_1$, together with the binomial identity
\[
 \sum_{j=0}^{\ell-1}\binom{\ell+j-1}{j}
 =\binom{2\ell-1}{\ell-1}
\]
gives
\[
 \|p_\ell\|_1\le2^\ell\binom{2\ell-1}{\ell-1}\le2^{3\ell}.
\]
Monic division by $h=Y^2-Y$ preserves integer coefficients. Each
leading-term elimination increases the sum of the coefficient norms
of the current quotient and remainder by at most a factor of three.
There are $O(\ell^2)$ eliminations in all the successive divisions.
Thus every intermediate coefficient has absolute value at most
$2^{O(\ell^2)}$, which proves the stated bound for $a_j,b_j$.
Its signed binary encoding consequently uses $O(\ell^2)$ bits.
Each coefficient vector has $O(\ell)$
entries. The successive divisions use $O(\ell^2)$ integer arithmetic
operations on integers of $O(\ell^2)$ bits, giving the claimed
$\poly(\ell)$ bit-operation and space bounds.
\end{proof}

\subsection{Bit complexity of the sums over Boolean assignments}
\label{subsec:rational-streaming-height}
We now bound every intermediate value in the computation of
$\mathcal H_t(z)=H(t+z)\bmod z^J$ from \eqref{eq:full-taylor-sum}.
Starting with the substitution rows $\vec{P}_{f,v}(T)$, we bound the
substituted factors, their sums over each group of Boolean variables,
and the accumulator $T_t$ for the Taylor data in
Proposition~\ref{prop:count}.
Fix a polynomial system $\mathcal P$ in $n$ Boolean variables, with
$m_{\mathrm{test}}$ equations of degree at most $k$, precision
$\ell$ such that $2^\ell>2^n$, and a replacement design for its
equation factors. Suppose the rows $\vec{P}_{f,v}$,
partitions $S_{t,g}$, and matrices $C_{t,g}$ satisfy
Definition~\ref{def:layout}, with parameters $Q,R,r,D,\tau$.
Recall the degree bound for $H$ and the number of Taylor coefficients
retained at each node:
\[
 d_H=kR\bigl(m_{\mathrm{test}}+2(\ell-1)\bigr),\qquad
 J=\left\lfloor\frac{d_H}{Q}\right\rfloor+1.
\]
All polynomials in the Taylor variable $z$ and the shared truncation
marker $V$ are stored in their unique representative modulo
$(z^J,V^\ell)$. Removing terms outside these degree ranges cannot
increase the coefficient norm.

The substitution rows have common denominator
\[
 d_{\mathrm{den}}=(R-1)!Q!.
\]
We use an integer $B_P\ge1$ such that every integer coefficient of every
row $d_{\mathrm{den}}\vec{P}_{f,v}(T)$ has absolute value at most $2^{B_P}$.
Definition~\ref{def:layout} gives $B_P=O(Q\log Q+\log D)$.
At a fixed node $t\in[Q]$ and for a fixed correction set $U\subseteq[n]$,
the input to factor $f$ at variable $v$ is
\[
 \theta_{f,v}(z;x)=\langle \vec{P}_{f,v}(t), x\rangle+
       \bigl\langle \vec{P}_{f,v}(t+z)-\vec{P}_{f,v}(t),\mathbf1_U\bigr\rangle,
 \qquad x\in\{0,1\}^n.
\]
Let $L_i(z;x)$ be the sum of the listed monomials of equation $i$
after these substitutions. Each $d_{\mathrm{den}}\theta_{i,v}(z;x)$
is an integer polynomial of coefficient norm at most
\[
 B_0=d_{\mathrm{den}}+3n(R+1)2^{B_P}(Q+1)^R .
\]
Indeed, each of the three row evaluations in $\theta_{i,v}$
contributes at most $n(R+1)2^{B_P}(Q+1)^R$ after denominators are
cleared. The bound holds also for the representatives in the group sums.

Put $\Delta=d_{\mathrm{den}}^k$. For a monomial of degree $u\le k$,
multiplying its substituted value by $\Delta$ gives an integer
polynomial of norm at most $d_{\mathrm{den}}^{k-u}B_0^u\le B_0^k$,
including the constant monomial. As $S$ bounds the total list length,
\[
 B=\max\{\Delta,SB_0^k\}
 \quad\text{satisfies}\quad \|\Delta L_i(z;x)\|_1\le B .
\]
Consequently $\log d_{\mathrm{den}}=O(Q\log(Q+2))$,
$\log B_0=O(Q\log(Q+2)+\log(nD+2))$, and
$\log B=O(k\log B_0+\log(S+2))$.

The substituted factor of equation $i$ is
\[
 \mathcal B_i(z,V;x)=\sum_{j=0}^{\ell-1}
       e_j\bigl(L_i(z;x)\bigr)h\bigl(L_i(z;x)\bigr)^jV^j
       \pmod{(z^J,V^\ell)}.
\]
Since $e_j$ is integral and has degree at most one, its substitution
has denominator dividing $\Delta$; the denominator of
$h(L_i)^j$ divides $\Delta^{2j}$. Thus, with
\[
 \Gamma=\Delta^{2\ell-1},
\]
every coefficient of $\Gamma\mathcal B_i(z,V;x)$ is an integer.
To bound the resulting integer numerators, put
\[
 E_\ell=\max\{1,\|e_0\|_1,\ldots,\|e_{\ell-1}\|_1\},\qquad
 B_1=\ell E_\ell(B+\Delta+2)^{2\ell-1}.
\]
For $A_i=\Delta L_i$, the two substituted factors have integer
numerators $\Delta e_j(L_i)$ and $A_i(A_i-\Delta)$, with norms at most
$E_\ell(B+\Delta)$ and $B(B+\Delta)$, respectively. Padding each term
to denominator $\Gamma$ therefore gives
\[
 \|\Gamma\mathcal B_i\|_1\le B_1,\qquad B_1\ge\Gamma,
 \qquad
 \log B_1=O\!\left(\ell^2+
       \ell\log(B+\Delta+2)+\log(\ell+1)\right).
\]

We next apply these estimates to the actual group sums.
Write $S_g=S_{t,g}$ and $C_g=C_{t,g}$, and let $c_g$ be the number
of rows of $C_g$. Thus $c=\sum_g c_g\le2\tau n$, and every coordinate
of a Boolean measurement $C_gx_g$ lies in $[-D,D]\cap\mathbb Z$.
Let $m_{\mathrm{test},g}$ be the number of equation factors assigned
to group $g$ at $t$, so $\sum_g m_{\mathrm{test},g}=m_{\mathrm{test}}$.
Their product $A_{g,U}(x;z)$ from \eqref{eq:group-polynomial} is
represented in $\mathbb Q[z,V]/(z^J,V^\ell)$. It has denominator
dividing $\Gamma^{m_{\mathrm{test},g}}$ and numerator norm, over that
denominator, at most $B_1^{m_{\mathrm{test},g}}$. The neutral
constant-one factors do not affect this bound.

For a pair $U\subseteq E\subseteq[n]$ with $|E|<J$ and an attainable
measurement tuple $\vec y=(y_1,\ldots,y_r)$, choose Boolean representatives
$\bar x_h$ with $C_h\bar x_h=y_h$. The group sum in
\eqref{eq:group-sum} is
\[
 \Sigma_g(\vec y)=
 \sum_{\substack{x_g\in\{0,1\}^{S_g}\\ C_gx_g=y_g\\
                  (x_g)_v=1\ (v\in E\cap S_g)}}
 A_{g,U}\!\Bigl(x_g+\sum_{h\ne g}\bar x_h;z\Bigr).
\]
Here vectors on individual groups are extended by zero.
The sum has at most $2^{|S_g|}$ terms, all over the same denominator,
so
\[
 \left\|\Gamma^{m_{\mathrm{test},g}}\Sigma_g(\vec y)\right\|_1
 \le 2^{|S_g|}B_1^{m_{\mathrm{test},g}}.
\]
For $1\le g\le r$, define the partial product
$\Pi_g(\vec y)=\prod_{h=1}^g\Sigma_h(\vec y)$, with truncation after each
multiplication. Its denominator divides
\[
 \Gamma^{\sum_{h\le g}m_{\mathrm{test},h}}.
\]
Consequently every full contribution $\Pi_r(\vec y)$ can be placed over
the fixed denominator
\[
 \Omega=\Gamma^{m_{\mathrm{test}}},
\]
and it satisfies
\[
 \|\Omega\Pi_r(\vec y)\|_1
 \le2^nB_1^{m_{\mathrm{test}}}.
\]

Let $T_t(z,V)$ be the accumulator that adds these full
contributions with sign $(-1)^{|E|-|U|}$ over all pairs and measurement
tuples. By \eqref{eq:full-taylor-sum}, its final value is the
$\mathcal A_\ell$-valued Taylor polynomial $\mathcal H_t(z)$.
The number $M_*$ of signed updates at one node is bounded by
\[
 M_*\le
 \biggl(\sum_{s=0}^{\min(J-1,n)}2^s\binom ns\biggr)(2D+1)^c
 \le3^n(2D+1)^c.
\]
Every intermediate value of $T_t$, not just its final value,
therefore satisfies
\[
 \|\Omega T_t\|_1
 \le M_*\,2^nB_1^{m_{\mathrm{test}}}.
\]
Each coefficient of the integer polynomial $\Omega T_t$ has
\[
 O\!\left(\log(M_*+1)+n+m_{\mathrm{test}}\log B_1\right)
\]
bits. This estimate also bounds the integer numerators of all group
sums and partial products with the fixed denominators given above.
The denominator satisfies
\[
 \log\Omega
 =k m_{\mathrm{test}}(2\ell-1)\log d_{\mathrm{den}}
 =O\!\left(k(m_{\mathrm{test}}\ell+1)Q\log(Q+2)\right).
\]

Each contribution multiplies at most $m_{\mathrm{test}}$ lifted equation factors. Processing further pairs or measurement tuples adds
new contributions; it does not multiply them into the previous ones.
This is why exponentially many iterations contribute only
$\log(M_*+1)$ to the bit estimate. Each stored polynomial has at most
$J\ell\le(d_H+1)\ell$ coefficients. The enumeration retains its current
indices and Boolean representatives, one group sum, one partial
product, and the accumulator $T_t$, without storing a table of
all assignments or all measurement tuples. These estimates give
\eqref{eq:sum-bit-bound} and polynomial bit cost per rational operation.
The $QJ\ell$ Taylor coefficients and the working state fit in
$\poly(n,m_{\mathrm{test}},\ell,D,Q,R,J,r,k,S)$ bits.

\subsection{Interpolation and the integer answer}
\label{subsec:rational-readout}
For $0\le s<\ell$, let $H_s(T)=[V^s]H(T)\in\mathbb Q[T]$.
Section~\ref{subsec:rational-streaming-height} bounds the computed data
$[z^jV^s]\mathcal H_t(z)=[z^j]H_s(t+z)$ for $t\in[Q]$, $0\le j<J$.
Fix $s$. We interpolate this coordinate, using the same rational
Hermite matrix for all $\ell$ coordinates. Put $M_H=QJ>d_H$.
In the monomial basis $1,T,\ldots,T^{M_H-1}$, the Hermite interpolation
matrix is the integer matrix
\[
 \mathsf V_{(t,j),u}=
 \begin{cases}\binom uj t^{u-j},&u\ge j,\\0,&u<j,\end{cases}
 \qquad t\in[Q],\quad 0\le j<J,\quad 0\le u<M_H.
\]
It is nonsingular by the Hermite interpolation statement in
Section~\ref{sec:counting}. Its entries have
$O(M_H\log(Q+2))$ bits.
Let $\mathbf y$ be the vector of computed coefficients
$[z^jV^s]\mathcal H_t(z)$, ordered by $(t,j)$, and let $\mathbf h$ be
the monomial coefficient vector of $H_s$, padded with zeros to length
$M_H$. Thus $\mathsf V\mathbf h=\mathbf y$.
The vector $\mathbf b=\Omega\mathbf y$ is integral; write
$B_{\mathrm{data}}$ for a bound on its entries' bit lengths.
The bounds in Section~\ref{subsec:rational-streaming-height} give
\[
 B_{\mathrm{data}}
 \le\poly(n,m_{\mathrm{test}},\ell,k,Q,\log(D+2),\log(S+2)).
\]

Only the constant coefficient $h_0=H_s(0)$ is needed. Let
$\mathsf V^{(0)}$ be obtained from $\mathsf V$ by replacing its
column indexed by $u=0$ with $\mathbf b$, and put
\[
 N_H=\det\mathsf V^{(0)},\qquad D_H=\det\mathsf V\ne0.
\]
Cramer's rule for $\mathsf V(\Omega\mathbf h)=\mathbf b$ gives
\begin{equation}\label{eq:exact-readout}
 H_s(0)=h_0=\frac{N_H}{\Omega D_H}.
\end{equation}
We compute these two determinants by fraction-free Gaussian
elimination~\cite[Sections~I--II and~IV--V]{Bareiss68}. For an
$M_H\times M_H$ integer matrix, this algorithm uses $O(M_H^3)$
integer arithmetic operations; pivoting allows it to handle
singular matrices as well. The retained elimination entries are
signed minors of the input matrix. Each update forms products
and a difference of such entries, followed by an exact integer
division. Consequently, bounds on the minors of $\mathsf V$ and
$\mathsf V^{(0)}$ also bound the intermediate integers used to
compute $D_H$ and $N_H$.
Every minor of $(\mathsf V\mid\mathbf b)$ has absolute value at most
\[
 2^{O\left(M_H\left(B_{\mathrm{data}}+
                M_H\log(Q+2)+\log(M_H+1)\right)\right)}.
\]
Indeed, its determinant is a sum of at most $M_H!$ products of at
most $M_H$ entries. The intermediate integers in fraction-free
elimination therefore have
\[
 O\!\left(M_H\bigl(B_{\mathrm{data}}+
                   M_H\log(Q+2)+\log(M_H+1)\bigr)\right)
\]
bits in signed binary notation. Computing $N_H,D_H$ thus uses
$\poly(M_H,B_{\mathrm{data}})$ bit operations and bits of working space.

At $T=0$ every $H_s(0)$ is an integer by construction, so the
division in \eqref{eq:exact-readout} is exact for each $s$. After
computing these $\ell$ integers, put $u=\sum_{s=0}^{\ell-1}H_s(0)$.
By \eqref{eq:origin-residue}, the least nonnegative residue
\[
 u-2^\ell\left\lfloor\frac{u}{2^\ell}\right\rfloor=N(\mathcal P)
\]
is the exact count. Reusing the same workspace for successive
coordinates, all $\ell$ interpolations, the sum and the remainder
use $\poly(M_H,B_{\mathrm{data}},\log(\Omega+1),\ell)$ bit operations
and polynomially many bits of working space.

\subsection{Arithmetic for the technique overview}
\label{subsec:overview-arithmetic}
We also justify the bit-complexity and space bounds for the
bounded-occurrence algorithm in Section~\ref{sec:technical-overview}.
Lemma~\ref{lem:row-coefficients} bounds the bit lengths of the
replacement coefficients by a polynomial in $n$. Solving the
polynomial-size rational linear systems in
Section~\ref{subsec:preview-separation} gives measurement
coefficients $\vec\lambda_{e,v,h}$ of polynomial bit length as well.
Let $\delta$ be the product of the denominators of all these
coefficients and all replacement coefficients, over all evaluation
points. There are only polynomially many, so $\delta$ also has
polynomial bit length. Every clause product uses at most $M\le3n$
linear inputs; consequently, all coefficients in the restricted
sums can be accumulated with common denominator $\delta^{3n}$.
Products of polynomially many input coefficients of polynomial
bit length, and sums of exponentially many such terms over this
common denominator, still have polynomial bit length. The exact
Hermite interpolation above therefore has polynomial bit cost
for these Taylor data as well. Finally, the enumerations can be
performed sequentially, retaining only the construction, current
indices, coefficient arrays, running sums, and the polynomially
many Taylor coefficients needed for interpolation. This gives
polynomial space and only polynomial bit-operation overhead.

\raggedbottom

\section{Additional Consequences of Refuting ETH}\label{app:consequences}
Theorem~\ref{thm:main} gives a circuit lower bound and
subexponential-time algorithms for inverting Boolean maps with constant
output locality. The fixed-density case gives the quantitative circuit
lower bound in Corollary~\ref{cor:quantitative-circuits}. Both circuit arguments use
only the decision version of our $3$-SAT algorithm. Exact preimage
counting uses its full counting guarantee.

\subsection{Circuit lower bounds for $\mathrm E^{\mathrm{NP}}$}\label{subsec:circuit-lower-bounds}
For the qualitative bound below, write $\mathrm{SIZE}(O(n))$ for the
languages having nonuniform circuits with $O(n)$ bounded-fan-in AND,
OR, and NOT gates.

\begin{corollary}\label{cor:consequence-circuits}
We have
\[
 \mathrm E^{\mathrm{NP}}\not\subseteq\mathrm{SIZE}(O(n)).
\]
\end{corollary}
\begin{proof}
Williams proved that if ETH is false, then
$\mathrm E^{\mathrm{NP}}$ does not have linear-size
circuits~\cite[Theorem~6.1]{Wil13}. Apply this implication to the
deterministic subexponential-time $3$-SAT algorithm supplied by
Theorem~\ref{thm:main}.
\end{proof}

The connection is an instance of deriving circuit lower bounds from
faster satisfiability algorithms. To encode a Boolean circuit with $s$
gates and $n$ inputs, introduce a variable for each gate, enforce its
value from its inputs, and add a unit clause requiring the output bit
to equal $1$. The resulting $3$-CNF has $O(n+s)$ variables and clauses
and is satisfiable exactly when the circuit is. Our theorem therefore
decides satisfiability of linear-size circuits in $2^{o(n)}$ time.
Williams's argument combines
such a speedup with hypothetical small circuits for witnesses to
contradict a nondeterministic time hierarchy. The corollary gives a
language in $\mathrm E^{\mathrm{NP}}$ without a linear-size circuit
family; it does not assert a superpolynomial circuit lower bound for NP.

\input{quantitative-circuits}

\subsection{Inverting Boolean maps with constant output locality}\label{subsec:local-inversion}
Fix a constant $d$. Consider a Boolean map
$G:\{0,1\}^n\to\{0,1\}^m$ whose $i$th output bit has the form
\[
 G(\vec{x})_i=g_i(\vec{x}|_{S_i}),
 \qquad S_i\subseteq[n],\quad |S_i|\le d.
\]
The input description of $G$ lists the sets $S_i$ and the truth
tables of the Boolean functions $g_i$. Thus each output inspects
only constantly many input bits, although the sets $S_i$ may overlap
arbitrarily. Given a target $\vec{b}\in\{0,1\}^m$, inversion asks
for any $\vec{x}$ with $G(\vec{x})=\vec{b}$.

\begin{corollary}\label{cor:consequence-local-inversion}
For every fixed $d$ and $n\ge20$, the number
$|G^{-1}(\vec{b})|$ can be computed exactly, and a preimage can be
found whenever one exists, in deterministic time
\[
 (n+m)^{O_d(1)}2^{O_d(\rho(n))}
\]
and space $(n+m)^{O_d(1)}$.
\end{corollary}
\begin{proof}
For each $i$ and each local assignment
$\vec{\alpha}\in\{0,1\}^{S_i}$ with $g_i(\vec{\alpha})\ne b_i$,
include the clause
\[
 \bigvee_{j\in S_i}\ell_{j,\alpha_j},
 \qquad
 \ell_{j,0}=X_j,\quad \ell_{j,1}=\neg X_j.
\]
This clause forbids exactly the local assignment $\vec{\alpha}$.
If $S_i$ is empty, its constraint is constant and can be checked
directly. The conjunction of the remaining clauses is a CNF on the
original $n$ declared variables, with width at most $d$ and at most
$2^d m$ clauses. Its satisfying assignments are exactly
$G^{-1}(\vec{b})$; no auxiliary variables or multiplicity corrections
are needed. Apply Theorem~\ref{thm:main} with $k=\max\{2,d\}$.
The usual variable-by-variable self-reduction finds a preimage using
at most $n$ further counting queries, which only changes the
polynomial factor. Each query may be discarded before the next,
preserving polynomial space.
\end{proof}

Conditional counts also allow an exactly uniform preimage to be
sampled, when the preimage set is nonempty, with the same bound in
expected time up to polynomial factors~\cite{JVV86}.
In particular, the corollary applies to constant-locality versions
of Goldreich's candidate one-way functions, which evaluate local
predicates on overlapping subsets of input bits~\cite{Gol00}.
For polynomially many output bits, it gives a $2^{o(n)}$-time
inversion algorithm for every output in the image, ruling out
$2^{\Omega(n)}$ inversion hardness for these families. This does not
rule out one-wayness against polynomial-time algorithms.

\input{quantitative-reduction}
\input{quantitative-contraction}

\begin{thebibliography}{CHKX06}

\bibitem[ABHS19]{ABHS19}
Amir Abboud, Karl Bringmann, Danny Hermelin, and Dvir Shabtay.
\href{https://doi.org/10.1137/1.9781611975482.3}
{\emph{SETH-Based Lower Bounds for Subset Sum and Bicriteria Path}}.
30th ACM--SIAM Symposium on Discrete Algorithms, 2019, 41--57.

\bibitem[AW14]{AW14}
Amir Abboud and Virginia Vassilevska Williams.
\href{https://doi.org/10.1109/FOCS.2014.53}
{\emph{Popular Conjectures Imply Strong Lower Bounds for Dynamic Problems}}.
55th IEEE Symposium on Foundations of Computer Science, 2014, 434--443.

\bibitem[AGP23]{AGP23}
Josh Alman, Yunfeng Guan, and Ashwin Padaki.
\href{https://arxiv.org/abs/2211.05217}
{\emph{Smaller Low-Depth Circuits for Kronecker Powers}}.
34th ACM--SIAM Symposium on Discrete Algorithms, 2023, 4159--4187.

\bibitem[AW15]{AW15}
Josh Alman and Ryan Williams.
\href{https://arxiv.org/abs/1507.05106}
{\emph{Probabilistic Polynomials and Hamming Nearest Neighbors}}.
56th IEEE Symposium on Foundations of Computer Science, 2015, 136--150.

\bibitem[AW17]{AW17}
Josh Alman and Ryan Williams.
\href{https://arxiv.org/abs/1611.05558}
{\emph{Probabilistic Rank and Matrix Rigidity}}.
49th ACM Symposium on Theory of Computing, 2017, 641--652.

\bibitem[AR94]{AR94}
Noga Alon and Yuval Roichman.
\href{https://doi.org/10.1002/rsa.3240050203}
{\emph{Random Cayley Graphs and Expanders}}.
Random Structures \& Algorithms \textbf{5}(2), 1994, 271--284.

\bibitem[BI16]{BI16}
Arturs Backurs and Piotr Indyk.
\href{https://doi.org/10.1109/FOCS.2016.56}
{\emph{Which Regular Expression Patterns Are Hard to Match?}}
57th IEEE Symposium on Foundations of Computer Science, 2016, 457--466.

\bibitem[BI18]{BackursIndyk18}
Arturs Backurs and Piotr Indyk.
\href{https://doi.org/10.1137/15M1053128}
{\emph{Edit Distance Cannot Be Computed in Strongly Subquadratic Time
(unless SETH is false)}}.
SIAM Journal on Computing \textbf{47}(3), 2018, 1087--1097.
Conference version in STOC 2015.

\bibitem[Bar23]{Bar23}
Boaz Barak.
\href{https://introtcs.org/public/lec_13_Cook_Levin.html}
{\emph{Introduction to Theoretical Computer Science}}.
Online textbook, 2023. Chapter~15, Lemmas~15.9--15.10.
\href{https://github.com/boazbk/tcs/releases/tag/v0.95}{Archived 2023 edition (v0.95)}.

\bibitem[Bar68]{Bareiss68}
Erwin H. Bareiss.
\href{https://doi.org/10.1090/S0025-5718-1968-0226829-0}
{\emph{Sylvester's Identity and Multistep Integer-Preserving Gaussian Elimination}}.
Mathematics of Computation \textbf{22}(103), 1968, 565--578.

\bibitem[BI13]{BeckImp13}
Chris Beck and Russell Impagliazzo.
\href{https://doi.org/10.1145/2488608.2488669}
{\emph{Strong ETH Holds for Regular Resolution}}.
45th ACM Symposium on Theory of Computing, 2013, 487--494.

\bibitem[BT94]{BT94}
Richard Beigel and Jun Tarui.
\href{https://doi.org/10.1007/BF01263423}
{\emph{On ACC}}.
Computational Complexity \textbf{4}(4), 1994, 350--366.

\bibitem[BGKM23]{BGKM23}
Vishwas Bhargava, Sumanta Ghosh, Mrinal Kumar, and Chandra Kanta Mohapatra.
\href{https://doi.org/10.1145/3625226}
{\emph{Fast, Algebraic Multivariate Multipoint Evaluation in Small
Characteristic and Applications}}.
Journal of the ACM \textbf{70}(6), 2023, 42:1--42:46.
Conference version in STOC 2022.

\bibitem[Bj\"o16]{Bjo16}
Andreas Bj\"orklund.
\href{https://doi.org/10.4230/LIPIcs.SWAT.2016.17}
{\emph{Below All Subsets for Some Permutational Counting Problems}}.
15th Scandinavian Symposium and Workshops on Algorithm Theory,
LIPIcs \textbf{53}, 2016, 17:1--17:11.

\bibitem[BKW19]{BKW19}
Andreas Bj\"orklund, Petteri Kaski, and Ryan Williams.
\href{https://doi.org/10.1007/s00453-018-0513-7}
{\emph{Generalized Kakeya Sets for Polynomial Evaluation and Faster
Computation of Fermionants}}.
Algorithmica \textbf{81}, 2019, 4010--4028.
Conference version in IPEC 2017.

\bibitem[Bri14]{Bri14}
Karl Bringmann.
\href{https://doi.org/10.1109/FOCS.2014.76}
{\emph{Why Walking the Dog Takes Time: Fr\'echet Distance Has No Strongly
Subquadratic Algorithms Unless SETH Fails}}.
55th IEEE Symposium on Foundations of Computer Science, 2014, 661--670.

\bibitem[BK15]{BK15}
Karl Bringmann and Marvin K\"unnemann.
\href{https://doi.org/10.1109/FOCS.2015.15}
{\emph{Quadratic Conditional Lower Bounds for String Problems and
Dynamic Time Warping}}.
56th IEEE Symposium on Foundations of Computer Science, 2015, 79--97.

\bibitem[Cal09]{CalabroThesis}
Chris Calabro.
\href{https://cseweb.ucsd.edu/~ccalabro/dissertation_single_spaced.pdf}
{\emph{The Exponential Complexity of Satisfiability Problems}}.
Ph.D. dissertation, University of California, San Diego, 2009.
Chapter~5.

\bibitem[CIP06]{CIP}
Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi.
\href{https://cseweb.ucsd.edu/~paturi/myPapers/pubs/CalabroImpagliazzoPaturi_2006_ccc.pdf}
{\emph{A Duality between Clause Width and Clause Density for SAT}}.
21st IEEE Conference on Computational Complexity, 2006, 252--260.

\bibitem[CGI$^{+}$16]{CGIMPS16}
Marco L. Carmosino, Jiawei Gao, Russell Impagliazzo, Ivan Mihajlin,
Ramamohan Paturi, and Stefan Schneider.
\href{https://doi.org/10.1145/2840728.2840746}
{\emph{Nondeterministic Extensions of the Strong Exponential Time
Hypothesis and Consequences for Non-reducibility}}.
7th Innovations in Theoretical Computer Science Conference, 2016, 261--270.

\bibitem[CCK$^{+}$20]{CCK20}
Parinya Chalermsook, Marek Cygan, Guy Kortsarz, Bundit Laekhanukit,
Pasin Manurangsi, Danupon Nanongkai, and Luca Trevisan.
\href{https://doi.org/10.1137/18M1166869}
{\emph{From Gap-Exponential Time Hypothesis to Fixed Parameter Tractable
Inapproximability: Clique, Dominating Set, and More}}.
SIAM Journal on Computing \textbf{49}(4), 2020, 772--810.
Conference version in FOCS 2017.

\bibitem[CW21]{CW21}
Timothy M. Chan and R. Ryan Williams.
\href{https://doi.org/10.1145/3402926}
{\emph{Deterministic APSP, Orthogonal Vectors, and More:
Quickly Derandomizing Razborov--Smolensky}}.
ACM Transactions on Algorithms \textbf{17}(1), Article~2, 2021, 1--14.
\href{https://people.csail.mit.edu/rrw/derand-apsp-ov-cr-talg.pdf}{Authors' manuscript}, Theorems~1.6 and~2.5.

\bibitem[CHKX06]{CHKX06}
Jianer Chen, Xiuzhen Huang, Iyad A. Kanj, and Ge Xia.
\href{https://doi.org/10.1016/j.jcss.2006.04.007}
{\emph{Strong Computational Lower Bounds via Parameterized Complexity}}.
Journal of Computer and System Sciences \textbf{72}(8), 2006, 1346--1367.

\bibitem[CLWYY25]{CLWYY25}
Zongchen Chen, Aditya Lonkar, Chunyang Wang, Kuan Yang, and Yitong Yin.
\href{https://doi.org/10.1145/3717823.3718163}
{\emph{Counting Random $k$-SAT near the Satisfiability Threshold}}.
57th ACM Symposium on Theory of Computing, 2025, 867--878.
Theorem~1.2 is numbered as in the \href{https://wcysai.com/publication/randomksat/randomkSAT.pdf}{authors' full version}.

\bibitem[Coo71]{Cook71}
Stephen A. Cook.
\href{https://www.cs.utoronto.ca/~sacook/homepage/1971.pdf}
{\emph{The Complexity of Theorem-Proving Procedures}}.
3rd ACM Symposium on Theory of Computing, 1971, 151--158.

\bibitem[Cur18]{Cur18}
Radu Curticapean.
\href{https://doi.org/10.1016/j.ic.2018.02.008}
{\emph{Block Interpolation: A Framework for Tight Exponential-Time
Counting Complexity}}.
Information and Computation \textbf{261}, Part~2, 2018, 265--280.
Conference version in ICALP 2015.

\bibitem[CDL$^{+}$16]{CDL16}
Marek Cygan, Holger Dell, Daniel Lokshtanov, D\'aniel Marx,
Jesper Nederlof, Yoshio Okamoto, Ramamohan Paturi, Saket Saurabh,
and Magnus Wahlstr\"om.
\href{https://doi.org/10.1145/2925416}
{\emph{On Problems as Hard as CNF-SAT}}.
ACM Transactions on Algorithms \textbf{12}(3), Article~41, 2016, 1--24.

\bibitem[DHM$^{+}$14]{DHMTW}
Holger Dell, Thore Husfeldt, D\'aniel Marx, Nina Taslaman, and Martin Wahl\'en.
\href{https://arxiv.org/abs/1206.1775}
{\emph{Exponential Time Complexity of the Permanent and the Tutte Polynomial}}.
ACM Transactions on Algorithms \textbf{10}(4), Article~21, 2014, 1--32.

\bibitem[Din16]{Din16}
Irit Dinur.
\href{https://eccc.weizmann.ac.il/report/2016/128/}
{\emph{Mildly Exponential Reduction from Gap 3SAT to Polynomial-Gap
Label-Cover}}.
Electronic Colloquium on Computational Complexity, Report TR16-128, 2016.

\bibitem[DL20]{DL20}
Zeev Dvir and Allen Liu.
\href{https://theoryofcomputing.org/articles/v016a020/}
{\emph{Fourier and Circulant Matrices are Not Rigid}}.
Theory of Computing \textbf{16}(20), 2020, 1--48.

\bibitem[vzGG13]{vzGG13}
Joachim von zur Gathen and J\"urgen Gerhard.
\href{https://doi.org/10.1017/CBO9781139856065}{\emph{Modern Computer Algebra}}.
3rd edition, Cambridge University Press, 2013.

\bibitem[Gol00]{Gol00}
Oded Goldreich.
\href{https://eccc.weizmann.ac.il/eccc-reports/2000/TR00-090/index.html}
{\emph{Candidate One-Way Functions Based on Expander Graphs}}.
Electronic Colloquium on Computational Complexity, Report TR00-090, 2000.

\bibitem[Gol08]{Gol08}
Oded Goldreich.
\href{https://www.wisdom.weizmann.ac.il/~oded/CC/bc-1.pdf}
{\emph{P, NP, and NP-Completeness: The Basics of Computational Complexity}}.
Author's draft, June 14, 2008, Proposition~4.7.
The Cambridge University Press edition appeared in 2010.

\bibitem[HKZZ19]{HKZZ19}
Thomas Dueholm Hansen, Haim Kaplan, Or Zamir, and Uri Zwick.
\href{https://doi.org/10.1145/3313276.3316359}
{\emph{Faster $k$-SAT Algorithms Using Biased-PPSZ}}.
51st ACM Symposium on Theory of Computing, 2019, 578--589.

\bibitem[Her14]{Hertli14}
Timon Hertli.
\href{https://doi.org/10.1137/120868177}
{\emph{3-SAT Faster and Simpler---Unique-SAT Bounds for PPSZ Hold in General}}.
SIAM Journal on Computing \textbf{43}(2), 2014, 718--729.
Conference version in FOCS 2011.

\bibitem[Hus11]{Hus11}
Thore Husfeldt.
\href{https://doi.org/10.1007/978-3-642-22012-8_3}
{\emph{Invitation to Algorithmic Uses of Inclusion--Exclusion}}.
38th International Colloquium on Automata, Languages, and Programming,
Part II, Lecture Notes in Computer Science \textbf{6756}, 2011, 42--59.

\bibitem[IMP12]{IMP12}
Russell Impagliazzo, William Matthews, and Ramamohan Paturi.
\href{https://cseweb.ucsd.edu/~paturi/myPapers/pubs/ImpagliazzoMatthewsPaturi_2012_soda.pdf}
{\emph{A Satisfiability Algorithm for $AC^0$}}.
23rd ACM--SIAM Symposium on Discrete Algorithms, 2012, 961--972.
\href{https://doi.org/10.1137/1.9781611973099.77}{Publisher's version}.

\bibitem[IP01]{IP01}
Russell Impagliazzo and Ramamohan Paturi.
\href{https://doi.org/10.1006/jcss.2000.1727}
{\emph{On the Complexity of $k$-SAT}}.
Journal of Computer and System Sciences \textbf{62}(2), 2001, 367--375.

\bibitem[IPZ01]{IPZ}
Russell Impagliazzo, Ramamohan Paturi, and Francis Zane.
\href{https://doi.org/10.1006/jcss.2001.1774}
{\emph{Which Problems Have Strongly Exponential Complexity?}}
Journal of Computer and System Sciences \textbf{63}(4), 2001, 512--530.

\bibitem[JMV13]{JMV13}
Hamid Jahanjou, Eric Miles, and Emanuele Viola.
\href{https://eccc.weizmann.ac.il/report/2013/099/revision/2/download/}
{\emph{Local Reductions}}.
Electronic Colloquium on Computational Complexity, Report TR13-099,
revision 2, 2013. Conference version in ICALP 2015, 749--760.

\bibitem[JVV86]{JVV86}
Mark R. Jerrum, Leslie G. Valiant, and Vijay V. Vazirani.
\href{https://doi.org/10.1016/0304-3975(86)90174-X}
{\emph{Random Generation of Combinatorial Structures from a Uniform Distribution}}.
Theoretical Computer Science \textbf{43}(2--3), 1986, 169--188.

\bibitem[JC26]{JC26}
Tao Jiang and Shaowei Cai.
\href{https://arxiv.org/abs/2607.10697}
{\emph{A Better Analysis For PPSZ For 3-SAT}}.
arXiv:2607.10697, 2026.

\bibitem[Koi06]{Koi06}
Mikko Koivisto.
\href{https://doi.org/10.1016/j.ipl.2005.11.013}
{\emph{Optimal 2-Constraint Satisfaction via Sum--Product Algorithms}}.
Information Processing Letters \textbf{98}(1), 2006, 24--28.

\bibitem[KSY14]{KSY14}
Swastik Kopparty, Shubhangi Saraf, and Sergey Yekhanin.
\href{https://doi.org/10.1145/2629416}
{\emph{High-Rate Codes with Sublinear-Time Decoding}}.
Journal of the ACM \textbf{61}(5), 2014, 28:1--28:20.

\bibitem[KW16]{KW16}
Ioannis Koutis and Ryan Williams.
\href{https://doi.org/10.1145/2742544}
{\emph{Algebraic Fingerprints for Faster Algorithms}}.
Communications of the ACM \textbf{59}(1), 2016, 98--105.

\bibitem[Kut26]{Kutzkov26}
Konstantin Kutzkov.
\href{https://doi.org/10.24963/ijcai.2026/254}
{\emph{Complementary Branching for \#SAT: Bounded-Degree Bounds and Faster \#3-SAT}}.
35th International Joint Conference on Artificial Intelligence, 2026, 2282--2290.

\bibitem[Li21]{Li21}
Ray Li.
\href{https://arxiv.org/abs/2008.05106}
{\emph{Settling SETH vs. Approximate Sparse Directed Unweighted Diameter
(up to (NU)NSETH)}}.
53rd ACM Symposium on Theory of Computing, 2021, 1684--1696.

\bibitem[Liu18]{Liu18}
Sixue Liu.
\href{https://doi.org/10.4230/LIPIcs.ICALP.2018.88}
{\emph{Chain, Generalization of Covering Code, and Deterministic Algorithm for $k$-SAT}}.
45th International Colloquium on Automata, Languages, and Programming,
LIPIcs \textbf{107}, 2018, 88:1--88:13.

\bibitem[LMS18]{LMS18}
Daniel Lokshtanov, D\'aniel Marx, and Saket Saurabh.
\href{https://doi.org/10.1145/3170442}
{\emph{Known Algorithms on Graphs of Bounded Treewidth Are Probably Optimal}}.
ACM Transactions on Algorithms \textbf{14}(2), Article~13, 2018, 1--30.
Conference version in SODA 2011.

\bibitem[MR17]{MR17}
Pasin Manurangsi and Prasad Raghavendra.
\href{https://doi.org/10.4230/LIPIcs.ICALP.2017.78}
{\emph{A Birthday Repetition Theorem and Complexity of Approximating
Dense CSPs}}.
44th International Colloquium on Automata, Languages, and Programming,
LIPIcs \textbf{80}, 2017, 78:1--78:15.

\bibitem[Mar10]{Marx10}
D\'aniel Marx.
\href{https://doi.org/10.4086/toc.2010.v006a005}
{\emph{Can You Beat Treewidth?}}
Theory of Computing \textbf{6}, 2010, 85--112.

\bibitem[NN93]{NN93}
Joseph Naor and Moni Naor.
\href{https://doi.org/10.1137/0222053}
{\emph{Small-Bias Probability Spaces: Efficient Constructions and Applications}}.
SIAM Journal on Computing \textbf{22}(4), 1993, 838--856.

\bibitem[Ope26]{OpenAIUGC26}
OpenAI, \emph{The Unique Games Theorem},
OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-Unique-Games-Theorem-September-23-2026/paper.pdf}{OAI:The-Unique-Games-Theorem-September-23-2026},
2026.

\bibitem[PPSZ05]{PPSZ05}
Ramamohan Paturi, Pavel Pudl\'ak, Michael E. Saks, and Francis Zane.
\href{https://doi.org/10.1145/1066100.1066101}
{\emph{An Improved Exponential-Time Algorithm for $k$-SAT}}.
Journal of the ACM \textbf{52}(3), 2005, 337--364.
Conference version in FOCS 1998.

\bibitem[Rag88]{Raghavan88}
Prabhakar Raghavan.
\href{https://doi.org/10.1016/0022-0000(88)90003-7}
{\emph{Probabilistic Construction of Deterministic Algorithms:
Approximating Packing Integer Programs}}.
Journal of Computer and System Sciences \textbf{37}(2), 1988, 130--143.

\bibitem[Rag08]{Rag08}
Prasad Raghavendra.
\href{https://doi.org/10.1145/1374376.1374414}
{\emph{Optimal Algorithms and Inapproximability Results for Every CSP?}}
40th ACM Symposium on Theory of Computing, 2008, 245--254.

\bibitem[RV13]{RV13}
Liam Roditty and Virginia Vassilevska Williams.
\href{https://doi.org/10.1145/2488608.2488673}
{\emph{Fast Approximation Algorithms for the Diameter and Radius of Sparse Graphs}}.
45th ACM Symposium on Theory of Computing, 2013, 515--524.

\bibitem[Sch24]{Scheder24}
Dominik Scheder.
\href{https://doi.org/10.46298/theoretics.24.5}
{\emph{PPSZ is better than you think}}.
TheoretiCS \textbf{3}, Article~5, 2024, 1--37.

\bibitem[Sch99]{Schon99}
Uwe Sch\"oning.
\href{https://doi.org/10.1109/SFFCS.1999.814612}
{\emph{A Probabilistic Algorithm for $k$-SAT and Constraint Satisfaction
Problems}}.
40th IEEE Symposium on Foundations of Computer Science, 1999, 410--414.

\bibitem[SS09]{SS09}
Alexander D. Scott and Gregory B. Sorkin.
\href{https://doi.org/10.1145/1597036.1597049}
{\emph{Polynomial Constraint Satisfaction Problems, Graph Bisection,
and the Ising Partition Function}}.
ACM Transactions on Algorithms \textbf{5}(4), 2009, 45:1--45:27.

\bibitem[SKC94]{SKC94}
Bart Selman, Henry A. Kautz, and Bram Cohen.
\href{https://cdn.aaai.org/AAAI/1994/AAAI94-051.pdf}
{\emph{Noise Strategies for Improving Local Search}}.
12th National Conference on Artificial Intelligence, 1994, 337--343.

\bibitem[SS96]{SS96}
Michael Sipser and Daniel A. Spielman.
\href{https://doi.org/10.1109/18.556667}
{\emph{Expander Codes}}.
IEEE Transactions on Information Theory \textbf{42}(6), 1996, 1710--1722.

\bibitem[Tan81]{Tanner81}
R. Michael Tanner.
\href{https://doi.org/10.1109/TIT.1981.1056404}
{\emph{A Recursive Approach to Low Complexity Codes}}.
IEEE Transactions on Information Theory \textbf{27}(5), 1981, 533--547.

\bibitem[Tov84]{Tov84}
Craig A. Tovey.
\href{https://doi.org/10.1016/0166-218X(84)90081-7}
{\emph{A Simplified NP-Complete Satisfiability Problem}}.
Discrete Applied Mathematics \textbf{8}(1), 1984, 85--89.

\bibitem[Val77]{Val77}
Leslie G. Valiant.
\href{https://doi.org/10.1007/3-540-08353-7_135}
{\emph{Graph-Theoretic Arguments in Low-Level Complexity}}.
Mathematical Foundations of Computer Science 1977,
Lecture Notes in Computer Science \textbf{53}, 1977, 162--176.

\bibitem[Val79]{Val79}
Leslie G. Valiant.
\href{https://doi.org/10.1137/0208032}
{\emph{The Complexity of Enumeration and Reliability Problems}}.
SIAM Journal on Computing \textbf{8}(3), 1979, 410--421.

\bibitem[VW19]{VW19}
Virginia Vassilevska Williams.
\href{https://doi.org/10.1142/9789813272880_0188}
{\emph{On Some Fine-Grained Questions in Algorithms and Complexity}}.
Proceedings of the International Congress of Mathematicians (ICM 2018),
World Scientific, 2019, 3447--3487.

\bibitem[VW21]{VW21}
Nikhil Vyas and Ryan Williams.
\href{https://doi.org/10.1613/jair.1.11859}
{\emph{On Super Strong ETH}}.
Journal of Artificial Intelligence Research \textbf{70}, 2021, 473--495.

\bibitem[Wah08]{Wahlstrom08}
Magnus Wahlstr\"om.
\href{https://doi.org/10.1007/978-3-540-79723-4_19}
{\emph{A Tighter Bound for Counting Max-Weight Solutions to 2SAT Instances}}.
3rd International Workshop on Parameterized and Exact Computation,
Lecture Notes in Computer Science \textbf{5018}, 2008, 202--213.

\bibitem[Wil05]{Wil05}
Ryan Williams.
\href{https://doi.org/10.1016/j.tcs.2005.09.023}
{\emph{A New Algorithm for Optimal 2-Constraint Satisfaction and Its Implications}}.
Theoretical Computer Science \textbf{348}(2--3), 2005, 357--365.

\bibitem[Wil13]{Wil13}
Ryan Williams.
\href{https://doi.org/10.1137/10080703X}
{\emph{Improving Exhaustive Search Implies Superpolynomial Lower Bounds}}.
SIAM Journal on Computing \textbf{42}(3), 2013, 1218--1244.
Conference version in STOC 2010. The numbering of Lemma~3.2 and Theorem~6.1 follows the
\href{https://people.csail.mit.edu/rrw/improved-algs-lbs2.pdf}{author's full version}.

\bibitem[Wil14]{Wil14}
Richard Ryan Williams.
\href{https://doi.org/10.4230/LIPIcs.FSTTCS.2014.47}
{\emph{The Polynomial Method in Circuit Complexity Applied to Algorithm
Design (Invited Talk)}}.
34th International Conference on Foundation of Software Technology and
Theoretical Computer Science, LIPIcs \textbf{29}, 2014, 47--60.

\bibitem[Wil16]{Wil16}
Richard Ryan Williams.
\href{https://doi.org/10.4230/LIPIcs.CCC.2016.2}
{\emph{Strong ETH Breaks With Merlin and Arthur: Short Non-Interactive
Proofs of Batch Evaluation}}.
31st Conference on Computational Complexity, LIPIcs \textbf{50}, 2016,
2:1--2:17.

\bibitem[WY07]{WY07}
David Woodruff and Sergey Yekhanin.
\href{https://doi.org/10.1137/06065773X}
{\emph{A Geometric Approach to Information-Theoretic Private Information
Retrieval}}.
SIAM Journal on Computing \textbf{37}(4), 2007, 1046--1056.

\bibitem[\v{Z}\'ak83]{Zak83}
Stanislav \v{Z}\'ak.
\href{https://doi.org/10.1016/0304-3975(83)90015-4}{\emph{A Turing
Machine Time Hierarchy}}.
Theoretical Computer Science \textbf{26}(3), 1983, 327--333.

\end{thebibliography}
\end{document}