% A 2^{o(n)} Time Algorithm for 3-SAT. % Compile with pdfLaTeX (or LuaLaTeX): two runs, three after changes to labels. No BibTeX run is needed. % Needs only standard packages of TeX Live (tested with TeX Live 2025). The file inputs nothing; all figures are TikZ code. % All numbers (sections, statements, equations, figures, Algorithm 1, steps, parts) are generated; % refer to them with \ref / \eqref. % Labels: sec:*, def:*, lem:*, prop:*, cor:*, thm:*, eq:*, alg:*, ov:* and fig:ov-* (the overview, Section 2: its subsections, displays, table and figures), % obs:* (observations after Definition 1), good:* ((G1), (G2)), app:*, intro:* (the introduction), lean:* (the propositions in the appendix on Lean). \documentclass[11pt]{amsart} \usepackage{iftex} \ifPDFTeX \usepackage[T1]{fontenc}\usepackage{lmodern} \fi % Latin Modern (the scalable Computer Modern); LuaLaTeX uses it by default \usepackage[letterpaper,hmargin=1.15in,vmargin=1.05in]{geometry} \usepackage[dvipsnames,svgnames,x11names]{xcolor} \usepackage{amssymb,mathtools} \usepackage{microtype} \usepackage{enumitem} \usepackage{flafter} \usepackage{tikz} \usetikzlibrary{calc,positioning,decorations.pathreplacing} \usepackage{hyperref} \hypersetup{colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue}\hypersetup{pdftitle={A 2\textasciicircum\{o(n)\} Time Algorithm for 3-SAT},pdfauthor={Claude}} % links are blue text, without boxes % ---- statements: Lemma, Proposition, Corollary share one counter; Definitions have their own. % To number statements and equations within sections (Lemma 2.1, (3.1), ...), change "false" to "true" in the next line. \newif\ifwithinsections \withinsectionsfalse \theoremstyle{plain} \newtheorem{maintheorem}{Theorem} % Theorems 1 and 2, on their own counter \ifwithinsections \newtheorem{lemma}{Lemma}[section] \else \newtheorem{lemma}{Lemma} \fi \newtheorem{proposition}[lemma]{Proposition} \newtheorem{corollary}[lemma]{Corollary} \newtheorem{apptheorem}{Theorem} \newtheorem*{eightsquare}{Eight-square identity} \newtheorem*{lemma*}{Lemma}\makeatletter\AddToHook{env/lemma*/begin}{\@beginparpenalty\@M}\makeatother % no page break between an unnumbered lemma and the line before it (the run-in head of 2.4) \renewcommand{\theapptheorem}{\Alph{apptheorem}} \theoremstyle{definition} \ifwithinsections \newtheorem{definition}{Definition}[section] \else \newtheorem{definition}{Definition} \fi \ifwithinsections \numberwithin{equation}{section} \fi \renewcommand{\qedsymbol}{\(\blacksquare\)} % ---- run-in heads and numbered run-in markers (each marker takes a label and prints its number) \newcommand{\runin}[1]{\par\smallskip\noindent\textbf{#1}\enspace} \newcounter{condc}\renewcommand{\thecondc}{(\roman{condc})} % conditions (i)-(iii) of Definition 2 \newcommand{\cond}[1]{\refstepcounter{condc}\label{#1}\thecondc} \newcounter{goodc}\renewcommand{\thegoodc}{(G\arabic{goodc})} % conditions (G1), (G2) of a good grouping \newcommand{\goodcond}[1]{\refstepcounter{goodc}\label{#1}\thegoodc} \newcounter{partc}\renewcommand{\thepartc}{(\alph{partc})} % parts (a), (b), ... of a statement \newcommand{\resetparts}{\setcounter{partc}{0}} \newcommand{\pt}[1]{\refstepcounter{partc}\label{#1}\textup{\thepartc}} \newcounter{appstep} % numbered steps in the appendices \newcommand{\appstep}[2]{\refstepcounter{appstep}\label{#1}\emph{Step \theappstep: #2.}} \newcommand{\secref}[1]{\hyperref[#1]{\S\ref*{#1}}} % prints "§7" as one link \newcommand{\citekey}[1]{\hyperlink{cite.#1}{#1}} % a citation label without brackets % ---- notation \newcommand{\bx}{\boldsymbol{x}}\newcommand{\by}{\boldsymbol{y}}\newcommand{\bu}{\boldsymbol{u}}\newcommand{\bv}{\boldsymbol{v}} \newcommand{\Urow}{U_{\mathrm{row}}}\newcommand{\Ucol}{U_{\mathrm{col}}} \newcommand{\poly}{\operatorname{poly}} % ---- pseudocode (Algorithm 1): \al{indent level}{text} prints one numbered line; % \kw keyword, \pr procedure name, \cm comment \newcounter{algorithm} \newcounter{algline}\newlength{\algind}\setlength{\algind}{1.5em} \newcommand{\al}[2]{\stepcounter{algline}\par\noindent\hangindent=\dimexpr2.1em+#1\algind+1.5em\relax\hangafter=1\makebox[1.5em][r]{\scriptsize\arabic{algline}}\hspace{0.6em}\hspace{#1\algind}#2} \newcommand{\kw}[1]{\textbf{#1}} \newcommand{\pr}[1]{\textsc{#1}} \newcommand{\cm}[1]{\quad{\footnotesize\color{black!60}\(\triangleright\)~#1}} % ---- colors of the figures; float and line-breaking parameters \definecolor{ourbar}{HTML}{1F5F8B} \definecolor{ourbg}{HTML}{EAF1F7} \emergencystretch=3em \allowdisplaybreaks \renewcommand{\topfraction}{0.8}\renewcommand{\textfraction}{0.1} \setlength{\captionindent}{0pt} \raggedbottom \title{A $2^{o(n)}$ Time Algorithm for 3-SAT} \author[Claude]{Claude\\ {\normalfont\footnotesize\scshape Anthropic}} \date{October 26, 2026} \subjclass[2020]{68Q25, 68W40, 68Q17} \keywords{3-SAT, Exponential Time Hypothesis, exact algorithms, tensor networks, rank} \newcounter{partgroup}\renewcommand{\resetparts}{\stepcounter{partgroup}\setcounter{partc}{0}}\renewcommand{\theHpartc}{\arabic{partgroup}.\arabic{partc}} \newcounter{eqgroup}\AddToHook{env/equation/before}{\stepcounter{eqgroup}}\renewcommand{\theHequation}{\arabic{eqgroup}.\arabic{equation}} % keeps the link targets of equations distinct % ---- notation of the appendices \newcommand{\Z}{\mathbb Z}\newcommand{\Q}{\mathbb Q}\newcommand{\zz}{\mathsf z}\newcommand{\mult}{\operatorname{mult}}\newcommand{\coef}[1]{[t^{#1}]}\newcommand{\Id}{\mathrm{Id}}\newcommand{\kHR}{c_{\mathrm{HR}}}\newcommand{\crow}{c^{\mathrm{row}}}\newcommand{\ccol}{c^{\mathrm{col}}}\newcommand{\Rrow}{R^{\mathrm{row}}}\newcommand{\Rcol}{R^{\mathrm{col}}} % ---- the exponent of the bound in n (Theorem D), defined here, once: the time is 2^{O(\expn)} \newcommand{\expn}{n\log\log n/\sqrt{\log n}} % ---- notation of Appendix D \newcommand{\nb}{\bar n}\newcommand{\rb}{\bar r}\newcommand{\sbar}{\bar s}\newcommand{\tb}{\bar t}\newcommand{\LL}{\boldsymbol\Lambda}\newcommand{\col}{\operatorname{load}}\newcommand{\ev}[1]{[\,|V_{#1}(\xi)|\text{\upshape\ even}\,]} % ---- the Lean listing of the appendix on Lean: each non-ASCII character is printed as a math symbol in a box one typewriter character wide (letters are narrowed to fit; operators, which stand between spaces, may stick out); the PDF records the original character, so that copying from the PDF gives the Lean text \usepackage{fvextra} \newsavebox{\leansave} \ifPDFTeX \newcommand{\leanlit}[1]{\pdfliteral page{#1}} \else \newcommand{\leanlit}[1]{\pdfextension literal page{#1}} \fi \newcommand{\leanact}[2]{\leanlit{/Span<>>BDC}\ensuremath{#2}\leanlit{EMC}} \newcommand{\leanbox}[2]{\sbox{\leansave}{\leanact{#1}{#2}}\ifdim\wd\leansave>\fontcharwd\font`x \resizebox{\fontcharwd\font`x}{\ht\leansave}{\usebox{\leansave}}\else\makebox[\fontcharwd\font`x][c]{\usebox{\leansave}}\fi} \newcommand{\leanop}[2]{\makebox[\fontcharwd\font`x][c]{\leanact{#1}{#2}}} \ifPDFTeX \newcommand{\leanchar}[2]{\DeclareUnicodeCharacter{#1}{#2}} \else \newcommand{\leanchar}[2]{\catcode"#1=\active \begingroup\lccode`\~="#1 \lowercase{\endgroup\protected\def~}{#2}} \fi \leanchar{00D7}{\leanop{00D7}{\times}} \leanchar{0393}{\leanbox{0393}{\Gamma}} \leanchar{03B1}{\leanbox{03B1}{\alpha}} \leanchar{03C6}{\leanbox{03C6}{\varphi}} \leanchar{208A}{\leanbox{208A}{{}_{+}}} \leanchar{2115}{\leanbox{2115}{\mathbb N}} \leanchar{211D}{\leanbox{211D}{\mathbb R}} \leanchar{2192}{\leanop{2192}{\to}} \leanchar{2200}{\leanbox{2200}{\forall}} \leanchar{2203}{\leanbox{2203}{\exists}} \leanchar{2208}{\leanop{2208}{\in}} \leanchar{2227}{\leanop{2227}{\wedge}} \leanchar{2264}{\leanop{2264}{\le}} \leanchar{230A}{\leanbox{230A}{\lfloor}} \leanchar{230B}{\leanbox{230B}{\rfloor}} \leanchar{27E8}{\leanbox{27E8}{\langle}} \leanchar{27E9}{\leanbox{27E9}{\rangle}} \leanchar{2194}{\leanop{2194}{\leftrightarrow}} \leanchar{00AC}{\leanop{00AC}{\neg}} \leanchar{00B2}{\leanbox{00B2}{{}^{2}}} \leanchar{00B7}{\leanop{00B7}{\cdot}} \leanchar{03B4}{\leanbox{03B4}{\delta}} \leanchar{1D4F}{\leanbox{1D4F}{{}^{k}}} \leanchar{1D62}{\leanbox{1D62}{{}_{i}}} \leanchar{201C}{\leanbox{201C}{\textrm{\textquotedblleft}}} \leanchar{201D}{\leanbox{201D}{\textrm{\textquotedblright}}} \leanchar{2026}{\leanbox{2026}{\ldots}} \leanchar{207F}{\leanbox{207F}{{}^{n}}} \leanchar{2080}{\leanbox{2080}{{}_{0}}} \leanchar{2081}{\leanbox{2081}{{}_{1}}} \leanchar{2082}{\leanbox{2082}{{}_{2}}} \leanchar{2083}{\leanbox{2083}{{}_{3}}} \leanchar{2099}{\leanbox{2099}{{}_{n}}} \leanchar{2212}{\leanop{2212}{-}} \leanchar{221A}{\leanbox{221A}{\text{\textsurd}}} \leanchar{221E}{\leanbox{221E}{\infty}} \leanchar{2265}{\leanop{2265}{\ge}} \leanchar{2A05}{\leanbox{2A05}{\sqcap}} \begin{document} \begin{abstract} We refute the Exponential Time Hypothesis (ETH) by presenting a deterministic algorithm for 3-SAT on \(n\) variables that runs in \(2^{o(n)}\) time. Our algorithm in fact solves the harder problem \#3-SAT, providing a count of the number of satisfying assignments. The result was discovered by an internal research Claude model and has been formalized in Lean~4. \end{abstract} \maketitle \section{Introduction}\label{sec:intro} A central question in the theory of computing is the P vs NP problem \cite{Coo71,Lev73,Kar72,Coo06}. Roughly, it asks if, for all problems with easily-verifiable solutions, is it easy to find such solutions? NP is the class of problems whose solutions can be verified in polynomial time and P is the class of problems that can be decided in polynomial time. The canonical example of an NP problem is 3-SAT. An instance of the 3-SAT problem has \(n\) Boolean variables \(x_1,\dots,x_n\) and a formula consisting of the AND of \(m\) clauses, with each clause consisting of the OR of at most 3 literals -- a literal is either a variable \(x_i\) or its negation \(\neg x_i\). The question is whether or not there exists an assignment of the variables that satisfies the formula -- i.e., each clause has at least one literal that is true. Given an assignment of the variables it is easy to validate whether or not the formula is satisfied. Thus the 3-SAT problem can be solved by enumerating all \(2^n\) possible settings of the \(n\) variables and checking whether the formula is satisfied. Since the 1980s, a series of works have improved on brute force enumeration and reduced the exponent by constant factors \cite{MS85,Sch99,PPSZ05,MS11,Her14,Sch21}; the prior record is \(O(1.328^n)\) time for deterministic 3-SAT algorithms \cite{Liu18} and \(O(1.308^n)\) for randomized algorithms \cite{PPSZ05,Her14,SS17,HKZZ19,Sch21}. Since 3-SAT is NP-complete \cite{Coo71,Kar72}, the P vs NP problem is equivalent to asking whether or not we can solve 3-SAT in time polynomial in the size parameters \(n\) and \(m\). It is widely conjectured that \(\mathrm P\ne\mathrm{NP}\), i.e., that it is \emph{not} possible to solve 3-SAT in polynomial time. An even stronger conjecture is that 3-SAT requires exponential time -- i.e. there is a constant \(\delta>0\) such that 3-SAT cannot be solved in \(O(2^{\delta n})\) time -- this is the exponential time hypothesis (ETH) of Impagliazzo and Paturi \cite{IP01}. We show that this stronger conjecture is not true. However, our result does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems. Our result also extends to \(k\)-SAT (3-SAT but with clauses containing at most \(k\) literals; such a formula is called a \(k\)-CNF) and to the \#\(k\)-SAT problem, which asks for the \emph{number} of satisfying assignments of a \(k\)-CNF; in contrast \(k\)-SAT only asks whether that number is zero or nonzero. We now state the general form of our main theorem. \begin{maintheorem}[Main Theorem]\label{intro:thm:strong} There is a deterministic algorithm that, given a \(k\)-CNF with \(m\) clauses in which \(n\) variables occur, computes the number of satisfying assignments of these \(n\) variables in time \begin{equation}\label{intro:bound} 2^{O(\min\{k^2\expn,\;km/\sqrt{\log m}\})}, \end{equation} where the \(O(\cdot)\) hides an absolute constant. \end{maintheorem} \noindent Our main theorem refutes the exponential time hypothesis, and it goes slightly further: we give a universal \(2^{o(n)}\) time algorithm (refuting ETH only requires that, for every \(\delta>0\), there exists an \(O(2^{\delta n})\)-time algorithm), and we specify a particular \(o(n)\) rate. Our algorithm gives a runtime bound of \(2^{O(km/\sqrt{\log m})}\), where \(m\) is the number of clauses. The bound in terms of the number of variables \(n\) then follows by combining it with sparsification techniques \cite{IPZ01,Cal09,DHMTW14}, which reduce the general case to formulas in which each variable occurs in few clauses, and some further ideas (Appendix~\ref{app:onelog}).\footnote{Note our main theorem implies that in the case the input is already sparse, the runtime is \(2^{O(kn/\sqrt{\log n})}\) without the \(\log\log n\) factor in the exponent.} \runin{Consequences.} Theorem~\ref{intro:thm:strong} implies faster algorithms for many other NP-complete problems: Independent Set, Clique, Vertex Cover and Dominating Set on graphs with \(n\) vertices can be solved in time \(O(2^{\delta n})\) for every \(\delta>0\) (see Corollary~\ref{cor:graphs} for Dominating Set; the other improvements follow from prior work \cite{IPZ01,FG04}), for example. Moreover, \(\mathrm E^{\mathrm{NP}}\) does not have Boolean circuits of linear size (this follows from Theorem~\ref{intro:thm:strong} by prior work \cite{Wil13,Wil14b,JMV15}). See \secref{sec:consequences} for these and more consequences. The exponential time hypothesis, and its even-stronger twin the strong exponential time hypothesis (SETH) \cite{IP01,CIP09}, are standard hardness assumptions in the literature \cite{LMS11,CFKLMPPS15}. SETH is a conjecture about \(k\)-SAT, which states that for every \(\delta<1\) there is a large enough \(k=k(\delta)\) such that \(k\)-SAT cannot be solved in \(O(2^{\delta n})\) time. SETH is known to imply ETH \cite{IP01,IPZ01}, so Theorem~\ref{intro:thm:strong}'s refutation of ETH also refutes SETH (Corollary~\ref{cor:eth}). However, Theorem~\ref{intro:thm:strong} does \emph{not} refute the Orthogonal Vectors hypothesis, which SETH implies and on which many lower bounds in fine-grained complexity rest \cite{Wil05,BI18,Vas18}. In a literature search carried out by Claude, we found more than 800 papers that prove at least one result of their own only under ETH or under a hypothesis that implies it, such as SETH or Gap-ETH; we did not count results that are also proved under a hypothesis that we do not refute, such as Orthogonal Vectors. Our result is purely asymptotic: for arbitrary 3-CNF formulas with \(m=5n\) clauses, the bound we prove does not improve on the \(2^n\) of exhaustive search unless \(n>10^{10\,000}\), and the bound in \(n\) alone, which holds for any number of clauses, does not unless \(n>10^{10^8}\) (see the ends of Appendices~\ref{app:rate} and~\ref{app:onelog}). Our general approach seems unlikely to yield any general improvement unless \(n>10^{7}\), however it is instantiated. Brute force enumeration is already impractical for \(n=100\), so the improvement of our result does not appear in practical settings. Thus our result says nothing about solving formulas in practice. \runin{Provenance.} The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input. Anthropic researchers worked with Claude to improve the presentation, resulting in this paper. Independently and concurrently, an internal model at OpenAI claims to have proven a similar result \cite{Ope26}. \subsection{Organization}\label{intro:results} For simplicity, the main body only proves a weaker version of the main theorem -- see Theorem~\ref{thm:main} in \secref{sec:overview} -- this suffices to refute ETH and explains the key ideas that go into the proof, but does not attain the strongest bound. \secref{sec:overview} gives an overview of the proof. \secref{sec:networks}, \secref{sec:crossing} and \secref{sec:level} contain its core (Lemma~\ref{lem:grouping}, Lemma~\ref{lem:pieces} and Proposition~\ref{prop:level}), \secref{sec:proof} proves Theorem~\ref{thm:main}, \secref{sec:consequences} derives the consequences, and \secref{sec:pseudocode} gives the algorithm in pseudocode. The \hyperref[intro:thm:strong]{Main Theorem} is proved in the appendices: the bound in \(m\) in Appendices~\ref{app:rate} and~\ref{app:half}, and the bound in \(n\) in Appendix~\ref{app:onelog}, which uses the count-preserving sparsification of Appendix~\ref{app:count}, written as a proof sketch. Appendix~\ref{app:lean} states the \hyperref[intro:thm:strong]{Main Theorem} and the failure of ETH in Lean and says what has been checked by machine and what has not. Appendix~\ref{app:eight} proves the eight-square identity, Appendix~\ref{app:related} discusses related work in more detail, and Appendix~\ref{app:motivation} explains how the search for the decomposition of Lemma~\ref{lem:pieces} leads to this identity and to the pieces of Appendix~\ref{app:half}. \subsection{Related work}\label{intro:related} \runin{Algorithms for \(k\)-SAT.} After the branching algorithms \cite{MS85,Kul99}, the two main randomized methods for \(k\)-SAT are the local search of Sch\"oning \cite{Sch99} and the algorithm of Paturi, Pudl\'ak and Zane \cite{PPZ99}, sharpened in later work of the authors joint with Saks \cite{PPSZ05}. The latter solves \(k\)-SAT in time \(2^{(1-\mu_k/(k-1))n+o(n)}\), with constants \(\mu_k\) that increase to \(\pi^2/6\) \cite{PPSZ05}; for \(k=3,4\) this needs Hertli's analysis \cite{Her14}, and later work has lowered the exponents only minutely \cite{SS17,HKZZ19,Sch21}. Sch\"oning's algorithm was derandomized in steps \cite{DGH02,MS11}, and the resulting bound has since been improved \cite{Liu18}. For counting, the known bounds were \(O(1.6423^n)\) for \#3-SAT \cite{Kut07}, improving an earlier bound \cite{DJW05}, and \(2^{(1-\Theta(1/k))n}\) for \#\(k\)-SAT \cite{IMP12,CW16}. In terms of the number of clauses \(m\), satisfiability of CNF formulas with clauses of any length was known in time \(1.2226^m\) times a polynomial in the length of the formula \cite{Hir00,Yam05,CXZ21}. In terms of the total number of literals \(L\), the bound was \(O(1.0638^L)\) \cite{PX23}. \runin{The hypotheses and what was built on them.} Before ETH, Stearns and Hunt had proposed a hypothesis of this kind \cite{SH90}. The bounds in the Sparsification Lemma \cite{IPZ01} were improved by Calabro, Impagliazzo and Paturi \cite{CIP06} and in Calabro's dissertation \cite{Cal09}, and Dell et al.\ \cite{DHMTW14} gave a form of it that preserves the number of satisfying assignments. Unless ETH fails, \(k\)-Clique has no algorithm running in time \(f(k)\,n^{o(k)}\) \cite{CHKX06,LMS11}, treewidth-based algorithms for constraint satisfaction are optimal up to a logarithmic factor in the exponent \cite{Mar10}, and many parameterized algorithms are optimal \cite{LMS18b,CFKLMPPS15}. Under SETH there are matching bounds for dynamic programming on graphs of bounded treewidth \cite{LMS18a}, for problems tied to CNF-SAT by reductions \cite{PW10,CDLMNOPSW16}, and for polynomial-time problems such as Edit Distance \cite{BI18,Vas18}. \runin{Earlier doubts.} Williams refuted a Merlin--Arthur version of SETH \cite{Wil16}, and Super-Strong ETH, a strengthening of SETH, fails for random \(k\)-SAT \cite{VW21}. The set cover conjecture, a relative of SETH \cite{CDLMNOPSW16,CFKLMPPS15}, is incompatible with the asymptotic rank conjecture \cite{BK24,Pra24}. In 2019 Williams estimated the likelihood that ETH is true at 70\% and that SETH is true at 25\% \cite{Wil19}. \runin{From algorithms to circuit lower bounds.} By a theorem of Williams \cite[Theorem~6.1]{Wil13}, Theorem~\ref{intro:thm:strong} implies that \(\mathrm E^{\mathrm{NP}}\) does not have Boolean circuits of linear size; this is part of his program of deriving circuit lower bounds from satisfiability algorithms slightly faster than exhaustive search \cite{Wil13,Wil14,MW20}. The best lower bound known before for a language in \(\mathrm E^{\mathrm{NP}}\), over the full binary basis, was \(3.1n-o(n)\) \cite{LY22}; the class \(\mathrm S_2\mathrm E\), which contains \(\mathrm E^{\mathrm{NP}}\), requires circuits of near-maximum size \cite{CHR24,Li24}. \runin{Sums of products and tensor networks.} The sums of products that we evaluate (\secref{ov:graph}) are weighted counting constraint satisfaction problems (\#CSPs) with constraints on two variables \cite{DGJ09,CC17}, pairwise sum-product expressions \cite{Koi06}, (for nonnegative weights) partition functions of pairwise Markov random fields \cite{WJ08}, and contractions of closed tensor networks \cite{MS08,Oru14,RS19}. Passing from a formula to such a sum on a small dense graph follows Williams's algorithm for 2-CSP \cite{Wil05}, which goes back to Ne\v{s}et\v{r}il and Poljak \cite{NP85}; there the saving comes from fast matrix multiplication, which we do not use. The closest work we know is that of Austrin, Kaski and Kubjas \cite{AKK22}, who study the cost of evaluating such sums by executing one tensor network along one contraction tree and prove, in that model, an unconditional lower bound in terms of branchwidth. By our calculation (Appendix~\ref{app:related}), in that model no algorithm for the problem on which we recurse (\secref{ov:dc}) has an exponent below about \(\frac49\) of that of brute force. Our algorithm lies outside the model, because it expands the sum into a signed sum of tensor networks and contracts different terms in different orders. \runin{Rank and expansions of a crossing} (see also Appendix~\ref{app:related}). Rank-based dynamic programming \cite{BCKN12,CKN12} also exploits low rank, and upper bounds are known on the asymptotic tensor rank of the tensor that underlies the problem on which we recurse \cite{CVZ19,BCKLOSW26}. Expanding a gadget that is not available into a linear combination of gadgets that are was used by Curticapean and Xia \cite{CX15}, after Galluccio and Loebl \cite{GL99}, to count perfect matchings in non-planar graphs. Decompositions of a crossing, the function \([x=v]\,[y=u]\) of \secref{ov:grid}, into functions that have rank 1 by rows or by columns have been studied for other purposes: lower bounds for arithmetic circuits and formulas, Hurwitz's sum-of-squares problem, and the partition rank \cite{HWY11,Nas20,Hru24,RZ25}. The recursion needs a different quantity, the sum of the costs by rows and by columns of each single term; Lemma~\ref{lem:pieces} starts from the classical eight-square case of Hurwitz's problem. The identity goes back to Degen (1818) and Graves (1843) \cite[Section 1]{Bae02}; Appendix~\ref{app:motivation} gives its history and shows how the search for the decomposition that our algorithm needs leads to it. \section{Overview of the proof}\label{sec:overview} \runin{Notation.} Throughout, \(\log=\log_2\), and time is measured in the word RAM model. A conjunctive normal form (CNF) formula is a \emph{set} of clauses (i.e.\ no clause is repeated, and thus a \(k\)-CNF on \(n\) variables has fewer than \((2n+1)^k\) clauses); our input is a \(k\)-CNF. The variables of a formula on \(n\) variables are \(x_1,\dots,x_n\); a formula in which \(n\) variables occur, as in the \hyperref[intro:thm:strong]{Main Theorem}, is one on \(n\) variables each of which occurs in some clause. By \#\(k\)-SAT, we mean the problem of counting the number of satisfying assignments to a given \(k\)-CNF. The main body of our paper proves the following simplified statement. The improved exponent of Theorem~\ref{intro:thm:strong} is proved in the appendix (Appendices~\ref{app:rate} and~\ref{app:half} for the bound in \(m\), and Appendix~\ref{app:onelog} for the bound in \(n\)). \begin{maintheorem}[Simplified version of Theorem~\ref{intro:thm:strong}]\label{thm:main} For every \(\delta>0\) there is a deterministic algorithm that computes the number of satisfying assignments of a 3-CNF on \(n\) variables, with any number of clauses, in time \(O(2^{\delta n})\). \end{maintheorem} \noindent Theorem~\ref{thm:main} refutes the Exponential Time Hypothesis (ETH) of Impagliazzo and Paturi \cite{IP01}. The algorithm depends on \(\delta\). Adjusting the parameters appropriately and using stronger ingredients gives the \hyperref[intro:thm:strong]{Main Theorem}. We describe the proof of Theorem~\ref{thm:main} in six steps (\secref{ov:graph} to \secref{ov:balance}); \secref{ov:stronger} explains how to strengthen the proof to yield the \hyperref[intro:thm:strong]{Main Theorem}. In this overview, we drop lower-order terms, rounding and polynomial factors; the exact statements are in Sections~\ref{sec:networks}--\ref{sec:pseudocode}. A bracket such as \([x=u]\) is 1 if the statement inside it is true and 0 otherwise. \subsection{From \#3-SAT to a sum of products on a graph}\label{ov:graph} By the count-preserving form of the Sparsification Lemma \cite{IPZ01,DHMTW14} (Lemma~\ref{lem:sparsification}), without loss of generality it suffices to reach time \(O(2^{\delta m})\) for every \(\delta>0\) under the sparsity assumption \(m\le O(n)\). We can view a CNF formula as a graph. Each clause corresponds to one node, and edges represent consistency constraints for shared variables. If two nodes have some number \(t\) of shared variables, we say the edge between them carries \(t\) bits, corresponding to how those shared variables are set. The first observation is that if this graph is disconnected, then the problem can be factored into smaller problems with no shared variables. More generally, if we can partition the graph with few edge bits crossing the cut, then for each fixing of the shared variables we can solve the counting problem on the two halves recursively then solve the overall counting problem via enumeration. In our actual algorithm, each level of the recursion rewrites the sum as a sum of polynomially many sums, where the degree of the polynomial depends on \(\delta\). Each of these inner sums is again a sum of products over a graph as before. We partition this graph not into two but into some larger number of pieces, where that number also depends on \(\delta\), merge each piece into a single node, and recurse on the resulting smaller graph, which has fewer edge bits in total. The key quantity is still the number of edge bits that cross between different partitions. The crux of our algorithm is to iteratively reduce this quantity while also keeping the parts small. The other key ingredient in our algorithm is a way to rewrite edges. At a very high level, we take a pair of edges between two parts of the graph and replace them with a single hyperedge. This reduces the number of edge bits between parts. To explain how this works we need to introduce an algebraic view of this graph problem that allows us to exploit cancellations. Each node \(a\) has ``local'' variables \(z_a\) and has a value \(W_a(z_a)\) -- this is 1 if these bits satisfy the clause and 0 otherwise. (In general, we will let \(W\) take arbitrary values.) Two nodes \(a,b\) are joined by an edge if their clauses share variables. The edge carries one bit for each shared variable, and \(\Psi_{a,b}(z_a,z_b)\) is 1 if the local variables \(z_a\) and \(z_b\) give a consistent view of a global set of variables and 0 otherwise. The number of satisfying assignments of the variables that occur in the formula is \begin{equation}\label{ov:Z} Z=\sum_{z}\ \prod_{a}W_a(z_a)\prod_{\{a,b\}}\Psi_{a,b}(z_a,z_b), \end{equation} where the sum over \(z\) ranges over all choices of all variables across all of the nodes, the first product is over all nodes, and the second is over all edges. Edges can be redundant: a variable that occurs in \(d\) clauses can be compared on \(d(d-1)/2\) edges. Since equality is transitive, comparing consecutive occurrences in a chain gives the same \(Z\) (Figure~\ref{fig:ov-graph}). This leaves \(d-1\) edge bits for the variable, and fewer than \(3m\) bits on all edges together. \begin{figure}[t]\centering \begin{tikzpicture}[x=0.97cm,y=1cm,font=\footnotesize, cl/.style={circle,draw,minimum size=5.8mm,inner sep=0pt,fill=white}, grp/.style={draw=black!70,dashed,fill=ourbg,rounded corners=4.3mm}, big/.style={circle,draw,minimum size=7.6mm,inner sep=0pt,fill=ourbg}, tst/.style={ourbar,line width=1.2pt}, ins/.style={black,line width=0.5pt}, rdd/.style={Maroon,dashed,line width=0.7pt}, lab/.style={font=\scriptsize,inner sep=2pt,text=black}, bit/.style={font=\scriptsize,fill=white,inner sep=1.2pt,text=ourbar}] \node[anchor=east,align=left,font=\scriptsize] at (-1.12,1.3) {% \(E_1=({\color{Maroon}x_1}\vee x_2\vee\neg x_3)\)\\[1pt] \(E_2=({\color{Maroon}\neg x_1}\vee x_3\vee x_4)\)\\[1pt] \(E_3=({\color{Maroon}x_1}\vee x_5\vee\neg x_6)\)\\[1pt] \(E_4=(\neg x_2\vee\neg x_5\vee x_7)\)\\[1pt] \(E_5=(\neg x_4\vee x_6\vee\neg x_7)\)\\[4pt] 8 edge bits in all}; \draw[grp] (-1.05,-0.43) rectangle (0.43,3.03); \draw[grp] (4.97,-0.43) rectangle (6.35,3.03); \draw[grp] (2.27,0.87) rectangle (3.13,1.73); \node[cl] (e1) at (0,2.6) {\(E_1\)}; \node[cl] (e2) at (0,0) {\(E_2\)}; \node[cl] (e3) at (2.7,1.3) {\(E_3\)}; \node[cl] (e4) at (5.4,2.6) {\(E_4\)}; \node[cl] (e5) at (5.4,0) {\(E_5\)}; \draw[ins] (e1)--(e2); \node[lab,anchor=east,align=right] at (-0.03,1.3) {\({\color{Maroon}x_1},x_3\)\\2 bits}; \draw[ins] (e4)--(e5); \node[lab,anchor=west,align=left] at (5.43,1.3) {\(x_7\)\\1 bit}; \draw[tst] (e2)--(e3) node[lab,midway,sloped,below] {\({\color{Maroon}x_1}\): 1 bit}; \draw[rdd] (e1)--(e3) node[lab,midway,sloped,above] {\({\color{Maroon}x_1}\): 0 bits}; \draw[tst] (e1)--(e4) node[lab,midway,above] {\(x_2\): 1 bit}; \draw[tst] (e2)--(e5) node[lab,midway,below] {\(x_4\): 1 bit}; \draw[tst] (e3)--(e4) node[lab,midway,sloped,above] {\(x_5\): 1 bit}; \draw[tst] (e3)--(e5) node[lab,midway,sloped,below] {\(x_6\): 1 bit}; \node[lab,above] at (-0.31,3.03) {\(G_1\)}; \node[lab,above] at (5.66,3.03) {\(G_3\)}; \node[lab,above] at (2.7,1.73) {\(G_2\)}; \draw[->,line width=0.7pt] (6.6,1.3)--(7.35,1.3) node[midway,above,font=\scriptsize] {merge}; \begin{scope}[xshift=7.75cm,yshift=0.3cm] \node[big] (g1) at (0,1.9) {\(G_1\)}; \node[big] (g3) at (2.4,1.9) {\(G_3\)}; \node[big] (g2) at (1.2,0.1) {\(G_2\)}; \draw[tst] (g1)--(g3) node[bit,midway,above,fill=none] {\(1+1=2\)}; \draw[tst] (g1)--(g2) node[bit,midway,left,fill=none] {1}; \draw[tst] (g2)--(g3) node[bit,midway,right,fill=none] {\(1+1=2\)}; \end{scope} \end{tikzpicture} \par\smallskip \footnotesize\caption{Left: a 3-CNF formula and its graph; the dashed comparison of \(x_1\) is redundant. Right: merging the shaded groups removes inner edges and adds up the bits between groups.}\label{fig:ov-graph}\label{fig:ov-merge} \end{figure} \subsection{Merging, cutting, and the parameters we track}\label{ov:merge}\label{ov:dc} We can view the graph cuts in \secref{ov:graph} as merge operations on the graph. I.e.\ we combine nodes in a part of the cut into a single node. Edges are also merged (the bits add up) or removed if both endpoints are merged together. \emph{Merging groups the factors of \(Z\) \eqref{ov:Z}.} A group \(G\) of nodes becomes one node (Figure~\ref{fig:ov-merge}) with local variables \(z_G=(z_a)_{a\in G}\). All \(W_a\) and \(\Psi_{a,b}\) inside \(G\) are multiplied into \(W_G\), and all \(\Psi_{a,b}\) between two groups \(G,H\) are multiplied into \(\Psi_{G,H}\). For example, merging \(a\) and \(b\) gives \(W_{\{a,b\}}=W_aW_b\Psi_{a,b}\). Every factor of \eqref{ov:Z} is used exactly once, so \(Z\) does not change. The cutting argument uses only the following property of $\Psi_{a,b}$. We say that a function $F(z_a, z_b)$ \emph{costs $c$ bits} if \begin{equation}\label{ov:share} F(z_a, z_b) \;=\; \sum_{\theta \in \{0,1\}^c} f(z_a, \theta)\, f'(z_b, \theta) \end{equation} for two integer-valued functions $f$ and $f'$. For each fixed $\theta$ the summand is a product of a function of $z_a$ and a function of $z_b$. A test that $c$ bits of $z_a$ equal $c$ bits of $z_b$ costs $c$ bits: $\theta$ is their common value. Conversely, a function that costs $c$ bits can be turned into an equality test: each endpoint gets its own copy of $\theta$, the functions $f$ and $f'$ are multiplied into $W_a$ and $W_b$, and the edge tests that the two copies agree. We define the number of bits on an edge to mean the least number of bits that its corresponding $\Psi_{a,b}$ costs in this sense. A product of functions that cost \(c_1\) and \(c_2\) bits costs \(c_1+c_2\) bits (take \(\theta=(\theta_1,\theta_2)\) and multiply the \(f\)'s), so the bits at most add up when edges are merged. \emph{Cutting exchanges the order of summation.} Take two nodes \(a,b\), say the two merged parts of a cut, and one edge, which costs \(c\) bits. Substitute \eqref{ov:share} in \eqref{ov:Z} and move the sum over \(\theta\) to the front: \begin{equation}\label{ov:cut} Z=\sum_{z_a,z_b}W_a(z_a)\,W_b(z_b)\,\Psi_{a,b}(z_a,z_b)=\sum_{\theta\in\{0,1\}^c}\Bigl(\sum_{z_a}W_a(z_a)\,f(z_a,\theta)\Bigr)\Bigl(\sum_{z_b}W_b(z_b)\,f'(z_b,\theta)\Bigr). \end{equation} The outer sum enumerates the bits that cross the cut; the inner sums solve the two halves. Depending on the parameters, the right-hand side represents a more efficient way to compute $Z$. The halves can be cut further in the same way. This divide and conquer approach does not suffice to achieve subexponential time: In formulas corresponding to sparse expander graphs (such as from random CNF formulae), every cut into two parts of comparable size is crossed by $\Omega(n)$ bits. So any algorithm that fixes one tree of cuts in advance and enumerates the crossing bits of each cut takes time $2^{\Omega(n)}$. Thus earlier divide and conquer ideas only improved the constant in the exponent. \emph{Edge rewriting (via the eight-square identity; see \secref{ov:identity}).} Our new algorithm rewrites $Z$ so that pairs of equality tests are replaced by other integer-valued functions, which can take negative values. These new functions are a parity on sets of four nodes -- in a sense these are ``hyperedges'' added to the graph. However, we then merge nodes so that each of these hyperedges becomes a regular edge (or disappears). That is, each of these new functions either lies inside one merged node, and then it is a factor of the $W$ of that node, or it joins two merged nodes, and then it is turned back into an equality test as described after Equation~\eqref{ov:share}, which multiplies $f$ and $f'$ into the $W$ of these two nodes. (After merging, none of these parity functions cross three or more nodes.) After this rewriting, the $W$ can take negative values, and a term is no longer the number of satisfying assignments of any formula. The recursion therefore has to be set up for a more general problem: compute $Z$ as in Equation~\eqref{ov:Z} where every $\Psi_{a,b}$ is an equality test, as before, but the $W_a$ are arbitrary integer-valued functions, negative values included. Every instance on which the recursion is called has the following form. There are $K$ nodes, and every two of them are joined by an edge with $\lambda$ bits. (Edges with fewer than $\lambda$ bits are padded with bits that the $W_a$ force to be $0$, so only the largest number of bits on an edge matters.) Each node $a$ holds a separate string $z_a(b)$ of $\lambda$ bits for every other node $b$, so that $z_a$ is the list of these $K - 1$ strings. The function $W_a$ is arbitrary, and each edge tests that its two strings agree: \begin{equation}\label{ovw:form} \Psi_{a,b}(z_a, z_b) \;=\; [\, z_a(b) = z_b(a) \,], \end{equation} where the square brackets denote an indicator that is $1$ if the statement inside is true and $0$ otherwise. Let $S = \binom{K}{2} \lambda$ be the number of bits on all edges. \emph{Balancing (see \secref{ov:balance}).} We perform a second round of merging nodes to ensure that the number of bits per edge is balanced. The algorithm is deterministic, but we use the probabilistic method to show that a balanced grouping exists via analyzing a random grouping; the algorithm then tries all groupings. \subsection{The recursion}\label{ov:rec} The proof tracks the number \(K\) of nodes, the largest number \(\lambda\) of bits on an edge, the number \(S\) of bits on all edges, the number of steps for one value of a \(W\), and the number \(\beta\) of bits of such a value. In this section every bit on an edge is counted once. Sections~\ref{sec:networks}--\ref{sec:pseudocode} count it at both of its ends, write \(B\) for \(\beta\) and \emph{factors through \(c\) bits} for costs \(c\) bits, and write the running time as \(2^{eK^2\lambda}\); since \(K^2\lambda\) is about \(2S\), their exponents are about half of those here, and trying all values gives \(e=\frac12\) there. \emph{Running time.} The recursion has levels. Level $\ell$ works on instances of the form above with $K_\ell$ nodes, where $K_0 = 64$ and $K_\ell = 9K_{\ell-1}^{16}$. For an integer $\beta \ge 1$, let $T_\ell(S)$ be the largest number of steps that the algorithm takes on such an instance with $S$ bits on its edges in which all values of the $W_a$ are below $2^\beta$ in absolute value, where one evaluation of some $W_a$ of the instance at one argument counts as one step. So $\beta$ bounds the number of bits of a value of a $W_a$, and $T_\ell(S)$ depends on it because the algorithm adds and multiplies these values. We do not write $\beta$ as an argument of $T_\ell$, because it enters the bounds below only through a factor that is polynomial in $\beta$. When the algorithm runs on a formula with $m$ clauses, $\beta = O(m)$ at every level, with a constant that depends only on $\delta$, so this factor is polynomial in $m$. In such an instance $Z$ is the sum, over all values of the strings on the edges, of the product of the values $W_a(z_a)$. Level $0$ tries all values of the bits on the edges, so \begin{equation}\label{ovw:base} T_0(S) \;\le\; 2^{S} \cdot \mathrm{poly}(\lambda) . \end{equation} Here and below $\mathrm{poly}(\lambda)$ is a factor that is polynomial in $\lambda$ and in $\beta$, and it may depend on $\ell$. We say that \emph{level $\ell$ has exponent $e$} if \begin{equation}\label{ovw:exponent} T_\ell(S) \;\le\; 2^{eS} \cdot \mathrm{poly}(\lambda) \qquad \text{for all } S \text{ and } \beta . \end{equation} So level $0$ has exponent $1$, and we want levels with arbitrarily small exponents. Merging and cutting only rearrange the sum \eqref{ov:Z}. The one further ingredient is the eight-square identity (\secref{ov:identity}). \emph{One level.} Write $K$ for $K_{\ell-1}$. Let \(g=3K^8\), so that \(K_\ell=g^2\) and \(S=\binom{g^2}2\lambda\), and let \(t=\lceil\lambda/3\rceil\). The nodes of an instance are placed on a grid (\secref{ov:grid}), and \(\mathcal R\) is the set of \emph{rectangles} of a \(g\times g\) grid, that is, of choices of two rows and two columns. Level $\ell$ does the following with an instance on $K_\ell = g^2$ nodes that has $S$ bits on its edges. \begingroup\renewcommand{\labelenumi}{Step \arabic{enumi}.}\setlength{\leftmargini}{4.3em} \begin{enumerate} \item It rewrites $Z$ by Equation~\eqref{ovw:bundle}, which applies the identity of \secref{ov:identity} to blocks of 3 bits. This gives $(t+1)^{|\mathcal{R}|}$ terms. \item In each term it merges all rows or all columns. This gives $g$ nodes, with at most $(11/12 + 1/g)\,S$ bits on the edges between them, up to an additive constant that depends only on \(\ell\). \item It merges these $g$ nodes further into $K$ groups of at most $2g/K$ rows each, so that every two groups share at most $L$ bits. Here $L$ is a number for which $S' = \binom{K}{2} L$ satisfies the bound in Inequality~\eqref{ovw:rec}. It turns every edge function into an equality test, as described after Equation~\eqref{ov:share}, and pads the strings to the common length $L$. The local variables are then summed out: the new \(W\) of a group \(G\), at given strings on its edges, is the sum over \(z_G\) of the \(W_G(z_G)\) of \secref{ov:merge} times the functions \(f\) or \(f'\) of these edges. The result is an instance of level $\ell - 1$, whose nodes are the groups, with $S'$ bits on its edges. \item It calls level $\ell - 1$ on this instance, adds the results over all terms, and divides by $2^{t|\mathcal{R}|}$. \end{enumerate} \endgroup Steps 1 and 2 are \emph{grid and merge} (\secref{ov:grid}), and Step 3 is \emph{balancing} (\secref{ov:balance}). Table~\ref{ov:table} shows what one level does to each parameter. \begin{table}[t]\centering\small \renewcommand{\arraystretch}{1.15} \begin{tabular}{@{}llll@{}} \hline & before & after grid and merge & after balancing\\ \hline number of nodes & \(K_\ell=g^2=9K_{\ell-1}^{16}\) & \(g=3K_{\ell-1}^8\) & \(K_{\ell-1}\)\\ bits on an edge & \(\lambda\) & from \(\frac23g^2\lambda\) to about \(g^2\lambda\) & \(L=S'/\binom{K}{2}\)\\ bits on all edges & \(S=\binom{K_\ell}{2}\lambda\) & at most \((\frac{11}{12}+\frac1g)S\) & \(S'=\binom K2L\le(\frac{11}{12}+\frac2K)S\)\\ number of instances & 1 & \((t+1)^{|\mathcal R|}=\lambda^{O(g^4)}\) & the same\\ steps for one value of a \(W\) & 1 & about \(g\) & \(2^{5S/K}\) times a polynomial\\ bits of a value of a \(W\) & \(\beta\) & \(g\beta\) & \(\beta'\le K_\ell^2\beta+5S/K+O(1)\)\\ \hline \end{tabular} \caption{One level of the recursion. Here $K=K_{\ell-1}$, $g=3K^8$, $t=\lceil\lambda/3\rceil$ and $|\mathcal R|=\binom g2^2$. Additive constants that depend only on \(\ell\) are left out, and the steps for one value of a \(W\) are counted in evaluations of the \(W_a\) of the given instance. The corresponding bounds, in the terms of Sections~\ref{sec:networks}--\ref{sec:pseudocode}, are in the proofs of Proposition~\ref{prop:level} (middle column) and Lemma~\ref{lem:grouping} (right column); for the last row those proofs have other bounds, \(g\beta+g^2\lambda+1\) and about \(g^3\beta+g^4\lambda\), which are also linear in \(\lambda\) and \(\beta\).}\label{ov:table} \end{table} The resulting recurrence is \begin{equation}\label{ovw:rec} T_\ell(S) \;\le\; (t+1)^{g^4/4} \cdot 2^{\,5S/K_{\ell-1}} \cdot \mathrm{poly}(\lambda) \cdot T_{\ell-1}(S'), \qquad S' \;\le\; \Bigl(\frac{11}{12} + \frac{2}{K_{\ell-1}}\Bigr)\, S , \end{equation} where the bound on $S'$ holds up to an additive constant that depends only on $\ell$, and $T_{\ell-1}(S')$ is taken with $\beta'$, the number of bits of the values of the $W$ of the groups, in the place of $\beta$. The factor $(t+1)^{g^4/4}$ bounds the number $(t+1)^{|\mathcal{R}|}$ of recursive calls, one for each term, since $|\mathcal{R}| = \bigl(g(g-1)/2\bigr)^2 < g^4/4 = K_\ell^2/4$. It is polynomial in $\lambda$, because $t \le \lambda$ and its degree $g^4/4$ depends only on $\ell$. The factor \(2^{5S/K_{\ell-1}}\) bounds, up to a polynomial factor, the time for one evaluation of the \(W\) of a group; \secref{ov:balance} explains it. \emph{The solution, by induction on $\ell$.} The claim is that $T_\ell(S) \le 2^{e_\ell S} \cdot p_\ell(\lambda, \beta)$ for a polynomial $p_\ell$, so that level $\ell$ has exponent $e_\ell$, where \begin{equation}\label{ovw:ei} e_0 = 1, \qquad e_\ell \;=\; \Bigl(\frac{11}{12} + \frac{2}{K_{\ell-1}}\Bigr)\, e_{\ell-1} + \frac{5}{K_{\ell-1}} . \end{equation} For $\ell = 0$ this is Inequality~\eqref{ovw:base}. For $\ell \ge 1$, put the claim for $\ell - 1$ into Inequality~\eqref{ovw:rec} and use the bound on $S'$: \begin{equation}\label{ovw:step} T_\ell(S) \;\le\; (t+1)^{g^4/4} \cdot \mathrm{poly}(\lambda) \cdot p_{\ell-1}(L, \beta') \cdot 2^{\,5S/K_{\ell-1} \,+\, e_{\ell-1}\,(11/12 + 2/K_{\ell-1})\,S} . \end{equation} The exponent is $e_\ell S$. The factors in front are polynomial in $\lambda$ and $\beta$, because $K_\ell$ is a constant and $L$, the number of bits on an edge of the subproblem, is at most a constant times $\lambda$, and $\beta'$ is at most $K_\ell^2 \beta + 5S/K_{\ell-1} + O(1)$, which is linear in $\lambda$ and $\beta$. The core of the proof is Proposition~\ref{prop:level}, the exact statement of one level. In the units of Sections~\ref{sec:networks}--\ref{sec:pseudocode} its recurrence is \(e'=(\rho+2/K)\,e+2/K\) with \(\rho=\frac{11}{12}\); its \(2/K\) becomes about \(4/K\) here, which \eqref{ovw:ei} bounds by \(5/K_{\ell-1}\). \emph{The exponents go to $0$.} The first one is $e_1 = 11/12 + 7/64 \approx 1.03$. This is larger than $e_0 = 1$, because $K_0 = 64$ is small. From level $2$ on the exponents decrease: there $K_{\ell-1} \ge K_1 = 9 \cdot 2^{96}$, and $K_\ell$ grows doubly exponentially while $e_\ell$ shrinks only geometrically. So the terms $2/K_{\ell-1}$ and $5/K_{\ell-1}$ change $e_\ell$ by a negligible amount, and \begin{equation}\label{ovw:eibound} e_\ell \;\le\; 1.12\, \Bigl(\frac{11}{12}\Bigr)^{\ell} . \end{equation} Each level reduces the number of nodes, from $9K^{16}$ to $K$, and the induction needs this. Step~2, which reduces the number of bits, takes $g^2$ nodes to $g$, and Step~3 takes these to $K = K_{\ell-1}$, so that the claim for level $\ell - 1$ applies to the result. \emph{Formulas.} For a formula with \(m\) clauses there is no grid at the top: we merge the clauses into \(3K_\ell^8\) clusters and balance. This gives a level-\(\ell\) instance with at most about \(3m\) bits on its edges and with \(\beta\le3m\), since a value of a \(W\) counts settings of the variables of at most \(m\) clauses, and hence time \(2^{3e_\ell m+O(m/K_\ell)}\) times a polynomial in \(m\) (Lemma~\ref{lem:grouping} and \secref{sec:proof}). Since \(e_\ell\to0\) and \(K_\ell\to\infty\), a constant \(\ell\), depending only on \(\delta\), gives time \(O(2^{\delta m})\). \begin{figure}[t]\centering \begin{tikzpicture}[x=1cm,y=1cm,font=\footnotesize, dot/.style={circle,fill=black,minimum size=4.4pt,inner sep=0pt}, btw/.style={ourbar,line width=1.3pt}, ins/.style={black,line width=0.6pt}, hyp/.style={circle,draw=ourbar,line width=0.9pt,fill=ourbar,minimum size=2.2mm,inner sep=0pt}, grp/.style={draw=black!70,dashed,fill=ourbg,rounded corners=1.8mm}, bit/.style={font=\scriptsize,fill=white,inner sep=1.2pt}, ttl/.style={font=\footnotesize,anchor=south}, corners/.pic={ \node[dot] (-x) at (0,1.2) {}; \node[dot] (-y) at (2.2,1.2) {}; \node[dot] (-u) at (0,0) {}; \node[dot] (-v) at (2.2,0) {}; \node[above left=-1.5pt] at (-x) {\(x\)}; \node[above right=-1.5pt] at (-y) {\(y\)}; \node[below left=-1.5pt] at (-u) {\(u\)}; \node[below right=-1.5pt] at (-v) {\(v\)};}] \node[dot] (A-x) at (0,1.2) {}; \node[dot] (A-y) at (2.2,1.2) {}; \node[dot] (A-u) at (0,0) {}; \node[dot] (A-v) at (2.2,0) {}; \node[above=1pt,xshift=-2mm] at (A-x) {\(x = z_a(b')\)}; \node[above=1pt,xshift=2mm] at (A-y) {\(y = z_{a'}(b)\)}; \node[below=1pt,xshift=-2mm] at (A-u) {\(u = z_b(a')\)}; \node[below=1pt,xshift=2mm] at (A-v) {\(v = z_{b'}(a)\)}; \draw[ourbar,line width=1.3pt] (A-x)--(A-v) node[bit,pos=0.25,text=ourbar] {3}; \draw[Maroon,line width=1.3pt] (A-y)--(A-u) node[bit,pos=0.25,text=Maroon] {3}; \node[ttl] at (1.1,1.85) {\(2\,\times\) two diagonals}; \node at (3.55,0.6) {\(=\)}; \pic (B) at (4.9,0) {corners}; \node[hyp] (Bk) at (6.0,0.6) {}; \foreach \p in {x,y,u,v} \draw[btw] (B-\p)--(Bk); \draw[ins] (B-x)--(B-y) node[midway,above=1pt,font=\scriptsize] {\(\sigma(x,y)\)}; \draw[ins] (B-u)--(B-v) node[midway,below=1pt,font=\scriptsize] {\(\sigma(v,u)\)}; \node[ttl] at (6.0,1.85) {row choice}; \node at (8.75,0.6) {\(+\)}; \pic (C) at (10.4,0) {corners}; \node[hyp] (Ck) at (11.5,0.6) {}; \foreach \p in {x,y,u,v} \draw[btw] (C-\p)--(Ck); \draw[ins] (C-x)--(C-u) node[midway,left=2pt,font=\scriptsize] {\(\sigma(x,u)\)}; \draw[ins] (C-y)--(C-v) node[midway,right=2pt,font=\scriptsize] {\(\sigma(v,y)\)}; \node[ttl] at (11.5,1.85) {column choice}; \foreach \x in {1.1,6.0,11.5} \draw[->,line width=0.7pt] (\x,-0.68)--(\x,-1.18) node[midway,right,font=\scriptsize] {merge rows}; \begin{scope}[yshift=-2.46cm] \draw[grp] (-0.3,0.72) rectangle (2.5,1.18); \draw[grp] (-0.3,-0.23) rectangle (2.5,0.23); \node at (1.1,0.95) {\(x,\ y\)}; \node at (1.1,0) {\(u,\ v\)}; \draw[btw] (1.1,0.72)--(1.1,0.23) node[midway,right,font=\scriptsize,text=ourbar] {\(x, y\): 6 bits}; \draw[grp] (4.6,0.72) rectangle (7.4,1.18); \draw[grp] (4.6,-0.23) rectangle (7.4,0.23); \node at (6.0,0.95) {\(x,\ y\)}; \node at (6.0,0) {\(u,\ v\)}; \draw[btw] (6.0,0.72)--(6.0,0.23) node[midway,right,font=\scriptsize,text=ourbar] {\(x \oplus y\): 3 bits}; \draw[grp] (10.1,0.72) rectangle (12.9,1.18); \draw[grp] (10.1,-0.23) rectangle (12.9,0.23); \node at (11.5,0.95) {\(x,\ y\)}; \node at (11.5,0) {\(u,\ v\)}; \draw[btw] (11.5,0.72)--(11.5,0.23) node[midway,right,font=\scriptsize,text=ourbar] {\(x, y\): 6 bits}; \end{scope} \end{tikzpicture} \caption{Equation~\eqref{ov:eight} for one rectangle, and what it costs after the rows are merged. The corners $a, a', b, b'$ hold $x, y, u, v$, as in Equation~\eqref{ovw:xyuv}. The thick lines that meet in a dot are the hyperedge $[x \oplus y \oplus u \oplus v = 0]$. When the columns are merged instead, the row choice costs $6$ bits and the column choice costs $3$.}\label{fig:ov-identity} \end{figure} \subsection{The eight-square identity}\label{ov:identity} \begin{lemma*}[Eight-square identity \cite{CS03,AM99}] There is a function \(\sigma\colon\{0,1\}^3\times\{0,1\}^3\to\{-1,1\}\) such that for all \(x,y,u,v\in\{0,1\}^3\), with \(\oplus\) the bitwise exclusive or, \begin{equation}\label{ov:eight} 2\,[x = v]\,[y = u] \;=\; [x \oplus y \oplus u \oplus v = 0]\,\bigl(\sigma(x,y)\,\sigma(v,u) + \sigma(x,u)\,\sigma(v,y)\bigr). \end{equation} \end{lemma*} \begin{proof} Let $\sigma(p,q) = (-1)^{\phi(p,q)}$ with $\phi(p,q) = \sum_{k \le k'} p_k q_{k'} + q_1 p_2 p_3 + p_1 q_2 p_3 + p_1 p_2 q_3$. Equation~\eqref{ov:eight} is a statement about $12$ bits, and it can be checked at all $4096$ settings. (\secref{sec:crossing} and Appendix~\ref{app:eight} prove it by hand.) \end{proof} The identity is two centuries old: Degen found it in 1818, and Graves found it again in 1843 by showing that the norm of the octonions is multiplicative \cite[Section 1]{Bae02}. In its classical form it writes \((a_1^2+\dots+a_8^2)(b_1^2+\dots+b_8^2)\) as a sum of eight squares of sums of terms \(\pm a_i b_j\) \cite[Chapter~6, \S6.10]{CS03}; \secref{sec:crossing} and Appendix~\ref{app:eight} derive Equation~\eqref{ov:eight} from it. From now on $\sigma$ is the function from this proof. It is not symmetric in its two arguments, so their order matters. Multiply out the right side of Equation~\eqref{ov:eight}, and let \(R(x,y,u,v)\) be the term with \(\sigma(x,y)\,\sigma(v,u)\) and \(C(x,y,u,v)\) the term with \(\sigma(x,u)\,\sigma(v,y)\). Figure~\ref{fig:ov-identity} shows the two terms; \secref{ov:grid} calls them the row choice and the column choice. \begin{figure}[t]\centering \begin{tikzpicture}[x=1cm,y=1cm,font=\footnotesize, nd/.style={circle,draw,minimum size=3.8mm,inner sep=0pt,fill=white,font=\scriptsize}, big/.style={circle,draw,minimum size=8.5mm,inner sep=0pt,fill=ourbg}, grp/.style={draw=black!70,dashed,fill=ourbg}, ins/.style={black,line width=0.5pt}, bit/.style={font=\scriptsize,fill=white,inner sep=1.2pt,text=ourbar}] \foreach \r in {0,...,5} \fill[ourbg,rounded corners=1.5mm] (-0.2,{0.48*\r-0.17}) rectangle (2.6,{0.48*\r+0.17}); \foreach \r in {0,...,5} \draw[black!25,line width=0.5pt] (0,{0.48*\r})--(2.4,{0.48*\r}); \foreach \c in {0,...,5} \draw[black!25,line width=0.5pt] ({0.48*\c},0)--({0.48*\c},2.4); \draw[ourbar,line width=1.3pt] (0.48,1.92)--(2.4,0.48); \draw[Maroon,line width=1.3pt] (2.4,1.92)--(0.48,0.48); \foreach \r in {0,...,5} \foreach \c in {0,...,5} \fill[black!45] ({0.48*\c},{0.48*\r}) circle (1.4pt); \foreach \p in {(0.48,1.92),(2.4,1.92),(0.48,0.48),(2.4,0.48)} \fill[black] \p circle (2.3pt); \node[above left=-1.5pt,text=ourbar] at (0.48,1.92) {\(x\)}; \node[below right=-1.5pt,text=ourbar] at (2.4,0.48) {\(v\)}; \node[above right=-1.5pt,text=Maroon] at (2.4,1.92) {\(y\)}; \node[below left=-1.5pt,text=Maroon] at (0.48,0.48) {\(u\)}; \draw[->,line width=0.7pt] (3.05,1.2)--(4.0,1.2) node[midway,above,align=center,font=\scriptsize] {merge\\rows}; \begin{scope}[xshift=4.7cm,yshift=0.2cm] \draw[grp] (0,1.6) ellipse [x radius=0.36,y radius=0.78]; \draw[grp] (3.4,1.6) ellipse [x radius=0.36,y radius=0.78]; \draw[grp] (1.7,0) ellipse [x radius=0.82,y radius=0.36]; \node[nd] (n1) at (0,2.0) {1}; \node[nd] (n2) at (0,1.2) {2}; \node[nd] (n3) at (3.4,2.0) {3}; \node[nd] (n4) at (3.4,1.2) {4}; \node[nd] (n5) at (1.28,0) {5}; \node[nd] (n6) at (2.12,0) {6}; \draw[ins] (n1)--(n2); \draw[ins] (n3)--(n4); \draw[ins] (n5)--(n6); \foreach \p/\q/\w in {1/3/2.0,1/4/0.5,2/3/0.5,2/4/1.2, 1/5/0.5,1/6/1.2,2/5/2.0,2/6/0.5, 3/5/1.2,3/6/0.5,4/5/0.5,4/6/2.0} \draw[ourbar,line width=\w pt] (n\p)--(n\q); \end{scope} \draw[->,line width=0.7pt] (8.8,1.2)--(9.8,1.2) node[midway,above,align=center,font=\scriptsize] {merge\\groups}; \begin{scope}[xshift=10.6cm,yshift=0.2cm] \node[big] (g1) at (0,1.75) {\(G_1\)}; \node[big] (g2) at (2.8,1.75) {\(G_2\)}; \node[big] (g3) at (1.4,0.1) {\(G_3\)}; \foreach \p/\q in {1/2,1/3,2/3} \draw[ourbar,line width=2.0pt] (g\p)--(g\q) node[bit,midway] {\(L\)}; \end{scope} \end{tikzpicture} \par\smallskip \footnotesize\caption{Left: the \(g\times g\) grid for \(g=6\); the corners of a rectangle hold the copies \(x,v\) and \(y,u\) of the strings on its two diagonals. Middle: the \(g\) merged rows; the widths show their unequal edge bits. Right: \(K=3\) merged groups, padded to exactly \(L\) bits on every edge.}\label{fig:ov-grid}\label{fig:ov-balance} \end{figure} \subsection{Grid and merge}\label{ov:grid} \emph{The grid.} Take an instance of level $\ell \ge 1$. Let $g = 3K_{\ell-1}^8$, so that it has $K_\ell = g^2$ nodes, and place the nodes on a $g \times g$ grid. Partition the edges into \emph{side edges} and \emph{diagonals}. A side edge joins two nodes in the same row or in the same column, and every other edge is a diagonal. The two rows and the two columns of a diagonal meet in four nodes, the corners of a rectangle $r$, with top left $a$, top right $a'$, bottom left $b$ and bottom right $b'$. The diagonals of $r$ are $\{a, b'\}$ and $\{a', b\}$, and every diagonal belongs to exactly one rectangle. Let $\mathcal{R}$ be the set of rectangles, so that $|\mathcal{R}| = \binom{g}{2}^2$. Then \begin{equation}\label{ovw:grid} Z \;=\; \sum_{z}\; \prod_{a} W_a(z_a) \prod_{\substack{\text{side edges}\\ \{a,b\}}} \Psi_{a,b}(z_a, z_b) \;\prod_{r \in \mathcal{R}} \Psi_{a,b'}(z_a, z_{b'})\, \Psi_{a',b}(z_{a'}, z_b). \end{equation} The placement is arbitrary. The grid is chosen by the algorithm and is not given by the instance. Its only use is to define two partitions of the nodes into $g$ parts, the rows and the columns. A diagonal joins two different rows and two different columns. A side edge joins two different rows or two different columns, but not both. Since all edges have $\lambda$ bits, every placement gives the same counts: the side edges are a $2/(g+1)$ fraction of all edges. Figure~\ref{fig:ov-grid} shows a rectangle. \emph{The case \(\lambda=3\).} Suppose first that $\lambda = 3$. For a rectangle $r$, write \begin{equation}\label{ovw:xyuv} x = z_a(b'), \qquad y = z_{a'}(b), \qquad u = z_b(a'), \qquad v = z_{b'}(a) . \end{equation} These are not the whole $z_a, z_{a'}, z_b, z_{b'}$. Each is the one string of $3$ bits that a corner holds for its diagonal partner. By Equation~\eqref{ovw:form}, the two diagonals of $r$ contribute the factor $[x = v]\,[y = u]$ to Equation~\eqref{ovw:grid}. Identity \eqref{ov:eight} rewrites this factor times 2. Put it into every rectangle of Equation~\eqref{ovw:grid}: \begin{equation}\label{ovw:sub} \begin{split} 2^{|\mathcal{R}|} Z \;=\; \sum_{z}\; \prod_{a} W_a(z_a) & \prod_{\substack{\text{side edges}\\ \{a,b\}}} \Psi_{a,b}(z_a, z_b)\\ & \cdot \prod_{r \in \mathcal{R}} [x \oplus y \oplus u \oplus v = 0]\,\bigl(\sigma(x,y)\,\sigma(v,u) + \sigma(x,u)\,\sigma(v,y)\bigr), \end{split} \end{equation} where $x, y, u, v$ are those of $r$. Expand the last product. This writes $2^{|\mathcal{R}|} Z$ as a sum of $2^{|\mathcal{R}|}$ terms, each of the form \begin{equation}\label{ovw:star} \sum_{z}\; \prod_{a} W_a(z_a) \prod_{\substack{\text{side edges}\\ \{a,b\}}} \Psi_{a,b}(z_a, z_b) \;\prod_{r \in \mathcal{R}} [x \oplus y \oplus u \oplus v = 0]\;\sigma_1(r)\,\sigma_2(r), \end{equation} where $\sigma_1(r)\,\sigma_2(r)$ is either $\sigma(x,y)\,\sigma(v,u)$ or $\sigma(x,u)\,\sigma(v,y)$. In the first case the two diagonals of $r$ have been replaced by two row edges, $\{a,a'\}$ and $\{b,b'\}$, and a hyperedge on all four corners. Call this a \emph{row choice} for $r$. The factor of \(r\) is then the \(R(x,y,u,v)\) of \secref{ov:identity}. In the second case they have been replaced by two column edges, $\{a,b\}$ and $\{a',b'\}$, and the same hyperedge. Call this a \emph{column choice}. The factor of \(r\) is then \(C(x,y,u,v)\). Figure~\ref{fig:ov-identity} shows both. The algorithm computes each term on its own, adds the results, and divides by $2^{|\mathcal{R}|}$. \emph{Merging.} Look at any term like Expression~\eqref{ovw:star}. If it has at least as many row choices as column choices, merge all rows: each row of the grid becomes one node. Otherwise merge all columns. Say that the rows are merged, and take a rectangle $r$. Then $x$ and $y$ are part of the $z$ of its upper row, and $u$ and $v$ are part of the $z$ of its lower row. We say that $r$ costs $c$ bits if its factor in the product, as a function of the $z$ of these two rows, costs $c$ bits in the sense of Equation~\eqref{ov:share}. \begin{itemize} \item Before the rewriting, $r$ costs $6$ bits, $3$ for each diagonal. \item With a row choice, $r$ costs $3$ bits. The hyperedge tests that $x \oplus y = u \oplus v$, so the two rows only have to agree on this one string of $3$ bits. Summing over its value $\theta$ gives \begin{equation}\label{ovw:rowff} [x \oplus y \oplus u \oplus v = 0]\,\sigma(x,y)\,\sigma(v,u) \;=\; \sum_{\theta \in \{0,1\}^3} \underbrace{[x \oplus y = \theta]\,\sigma(x,y)}_{f} \;\cdot\; \underbrace{[u \oplus v = \theta]\,\sigma(v,u)}_{f'} . \end{equation} This has the form of Equation~\eqref{ov:share} with $c = 3$: $f$ depends only on $\theta$ and the $z$ of the upper row, and $f'$ only on $\theta$ and the $z$ of the lower row. \item With a column choice, $r$ costs $6$ bits. Its factor depends on only $6$ bits of the $z$ of the upper row, namely $x$ and $y$. Summing over their values $\theta = (\theta_1, \theta_2)$ gives \begin{equation}\label{ovw:colff} \begin{split} [x \oplus y \oplus u \oplus v = 0]\,&\sigma(x,u)\,\sigma(v,y)\\ &=\; \sum_{\theta \in \{0,1\}^6} \underbrace{[x = \theta_1]\,[y = \theta_2]}_{f} \;\cdot\; \underbrace{[\theta_1 \oplus \theta_2 \oplus u \oplus v = 0]\,\sigma(\theta_1,u)\,\sigma(v,\theta_2)}_{f'} , \end{split} \end{equation} which has the form of Equation~\eqref{ov:share} with $c = 6$. \end{itemize} So no rectangle costs more than $6$ bits after the merge, and at least half of them cost only $3$. This reduces $6\,|\mathcal{R}|$ bits to at most $4.5\,|\mathcal{R}|$ bits. The factor of a rectangle is no longer an equality test, but it is turned back into one as described after Equation~\eqref{ov:share}: each of the two rows gets its own copy of $\theta$, the function $f$ of Equation~\eqref{ovw:rowff} or~\eqref{ovw:colff} is multiplied into the $W$ of the upper row and $f'$ into the $W$ of the lower row, and the edge between the rows tests that the two copies agree. The $\Psi_{a,b}$ of the side edges inside a row become factors of the $W$ of that row. The side edges inside columns still run between rows with all their bits, but they are only a $1/g$ fraction of the bits between rows. So for large $g$ the merged rows share about $3/4$ of the bits that they shared before. Since $g$ is a constant, an instance with $\lambda = 3$ has constant size, so this case only illustrates the drop from $6\,|\mathcal{R}|$ to at most $4.5\,|\mathcal{R}|$ bits. The next part handles general $\lambda > 3$. \emph{General \(\lambda>3\).} In the algorithm $\lambda$ is not a constant. The number $K$ of nodes depends only on $\delta$, while a formula with $m$ clauses can have close to $3m$ bits on its edges. These bits are spread over $\binom{K}{2}$ edges, so $\lambda$ can be as large as about $3m / \binom{K}{2}$, which grows in proportion to $m$. Let $t = \lceil \lambda/3 \rceil$, append zeros to the strings so that they have $3t$ bits, and divide each string into $t$ blocks of $3$ bits, $x = (x_1, \dots, x_t)$. Two strings are equal exactly if all their blocks are equal, so Equation~\eqref{ov:eight} can be used on each block: \begin{equation}\label{ovw:blocks} 2^{t}\,[x = v]\,[y = u] \;=\; \prod_{j \le t}\, [x_j \oplus y_j \oplus u_j \oplus v_j = 0]\,\bigl(\sigma(x_j,y_j)\,\sigma(v_j,u_j) + \sigma(x_j,u_j)\,\sigma(v_j,y_j)\bigr). \end{equation} Expanding this product gives $2^t$ terms for each rectangle, one for each way of making a row choice or a column choice in every block, and $2^{t|\mathcal{R}|}$ terms for the whole grid. A block costs $3$ bits one way and $6$ bits the other, as before. So for each term, merging rows or columns, whichever has more blocks with its choice, and turning the edge functions back into equality tests gives an instance with about $3/4$ of the bits on its edges. \emph{The number of terms.} The final algorithm does not use this expansion, because its number of terms is exponential in $\lambda$. The diagonals carry about $6t\,|\mathcal{R}|$ bits, which is almost all of $S$, so $2^{t|\mathcal{R}|}$ is about $2^{S/6}$. An algorithm that computes each term separately, as in the case $\lambda = 3$, therefore takes time at least about $2^{S/6}$, whatever it does for a single term. This is too slow: we want time $2^{eS}$ for arbitrarily small $e$. The final algorithm uses the following expansion instead, whose number of terms is polynomial in $\lambda$. \emph{Grouping the terms.} For each rectangle and each $i \in \{0, \dots, t\}$, add up all the terms of Equation~\eqref{ovw:blocks} with exactly $i$ column choices, and call the sum $A_i$. Then \begin{equation}\label{ovw:bundle} 2^{t}\,[x = v]\,[y = u] \;=\; A_0 + A_1 + \dots + A_t . \end{equation} Putting this into every rectangle and expanding gives $(t+1)^{|\mathcal{R}|}$ terms, one for each way of picking one $A_i$ for every rectangle. This is polynomial in $\lambda$, because $g$ is a constant. \emph{How many bits $A_i$ costs.} The terms inside one $A_i$ differ in which blocks have the column choice, and they have different strings $\theta$ in Equation~\eqref{ov:share}. For $t = 2$ and merged rows, the term with a row choice in block $1$ and a column choice in block $2$ has $\theta = (x_1 \oplus y_1,\, x_2,\, y_2)$, and the term with the choices exchanged has $\theta = (x_1,\, y_1,\, x_2 \oplus y_2)$. Each has $9$ bits. So the first term is $\sum_\theta f_1 f'_1$ and the second is $\sum_\theta f_2 f'_2$, where $f_1$ and $f_2$ depend on $\theta$ and the $z$ of the upper row, and $f'_1$ and $f'_2$ on $\theta$ and the $z$ of the lower row. Their sum $A_1 = \sum_\theta (f_1 f'_1 + f_2 f'_2)$ does not have the form of Equation~\eqref{ov:share}, which requires a single product of a function of the upper row and a function of the lower row. But $A_1 = \sum_{\omega \in \{1,2\}} \sum_{\theta} f_\omega f'_\omega$ does have this form, with the string $(\omega, \theta)$ of $1 + 9$ bits in the place of $\theta$. In general the extra part of the string ranges over the $\binom{t}{i}$ sets of $i$ blocks that have the column choice, one set for each term of $A_i$. This takes $\lceil \log_2 \binom{t}{i} \rceil$ bits, which is at most $t$ for every $i$. In the example it is $1$ bit because $\binom{2}{1} = 2$. We use $t$ bits for every $i$: one bit for each block, which says whether the block has the column choice. The number $i$ is not part of the string: the algorithm computes each of the $(t+1)^{|\mathcal{R}|}$ terms separately, and $i$ is fixed within a term. Since $i$ is fixed, $\theta$ has the same number of bits in every term of $A_i$, namely $3(t-i) + 6i$ with rows merged and $6(t-i) + 3i$ with columns merged. So $A_i$ costs at most \begin{equation}\label{ovw:cost} t + 3(t-i) + 6i \ \text{ bits with rows merged,} \qquad t + 6(t-i) + 3i \ \text{ bits with columns merged.} \end{equation} It never costs more than $6t$ bits, since $\theta = (x,y)$ always works for rows, and $\theta = (x,u)$ for columns. The two numbers in Expression~\eqref{ovw:cost} add up to $11t$, whatever $i$ is, against $6t + 6t = 12t$ for the two diagonals. For each block, rows plus columns, the count was $3 + 6 = 9$ against $12$, and now it is $3 + 6 + 1 + 1 = 11$ against $12$. For each term, the algorithm merges all rows or all columns, whichever gives the smaller number of bits on the edges of the merged instance. The two totals add up to at most $11t\,|\mathcal{R}|$ for the rectangles, so the smaller one is at most $5.5\,t\,|\mathcal{R}|$, against $6t\,|\mathcal{R}|$ before. This is the factor $11/12$. The exact statement is Lemma~\ref{lem:pieces}. \emph{The two expansions side by side.} Suppose that a merged instance with $S'$ bits on its edges is solved in time $2^{eS'}$, and let $s_0$ be the number of bits on the side edges between the merged parts. The running times with the expansion of Equation~\eqref{ovw:blocks} and with that of Equation~\eqref{ovw:bundle} are then at most about \begin{equation}\label{ovw:sidebyside} 2^{\,t|\mathcal{R}|} \cdot 2^{\,e\,(4.5\,t|\mathcal{R}| + s_0)} \qquad \text{and} \qquad (t+1)^{|\mathcal{R}|} \cdot 2^{\,e\,(5.5\,t|\mathcal{R}| + s_0)} . \end{equation} In each product the first factor is the number of terms, and the second is the time for one term. For $e = 1$ the two products agree, up to the factor $(t+1)^{|\mathcal{R}|}$. For $e < 1$ the second product is the smaller one as soon as $(1 - e)\,t > \log_2 (t+1)$. \emph{The middle column of Table~\ref{ov:table}.} Two rows are joined by \(g\) side edges and by \(g(g-1)/2\) rectangles, so they share \(g\lambda\) bits plus what is counted for these rectangles, which by Expression~\eqref{ovw:cost} and the sentence after it is between \(4t\) and \(6t\) bits each. In all, two rows share between \(\frac23g^2\lambda\) and about \(g^2\lambda\) bits. The side edges between the merged parts carry \(g\binom g2\lambda