The Exponential Time Hypothesis for 3-SAT

The Exponential Time Hypothesis for 3-SAT

Definitions and mathematical statement

A $3$-CNF formula is a conjunction of clauses, each a disjunction of at most three literals in Boolean variables. Let $n$ be the number of variables and $|F|$ the input length. ETH asserts a strictly positive exponential-time rate for deciding satisfiability, conventionally expressed as \[ \exists c>0:\quad 3\text{-SAT has no deterministic }O(2^{cn}\operatorname{poly}(|F|))\text{-time algorithm}. \] Polynomial input-reading factors and the precise time-bound convention are implicit in the catalogue's abbreviated $2^{cn}$ wording. The parameter is the number of variables, not the numerical size of an encoding or the clause count alone.

Formulation and concept references: [S1].

Short English statement

Does some positive exponential dependence on the number of variables remain unavoidable for deterministic $3$-SAT algorithms?

Research attempt

Current frontier.

The positive lower bound on the exponential rate in [S1] is stronger than $\mathsf P\ne\mathsf{NP}$, as also emphasized by the 2026 notes [S2]. The sparsification lemma of Impagliazzo--Paturi--Zane reduces general fixed-width SAT to a controlled number of bounded-occurrence instances [E1]. A published benchmark deterministic algorithm for $3$-SAT has running time $O^*(1.32793^n)$ [E2]; quoting such an upper bound does not prove that every algorithm needs any particular positive exponent. Recent strong sparsification by merging variables concerns $1$-in-$3$-SAT, with its different acceptance predicate, and cannot simply be substituted for ordinary $3$-SAT [E4]. The attempt below therefore looks for a subexponential algorithm, then tests the structural lemmas that would make it work.

Attack route.

The first candidate is a sparse-instance separator algorithm: enumerate assignments on a small separator and solve independent residual pieces. The precise missing property is an efficiently discoverable, recursively sublinear boundary after sound preprocessing. A second candidate replaces large boundary tables by compressed functions. That requires an exact representation closed under conjunction and existential quantification, with subexponential representation size and update time. A third route, proving ETH from large tables or large matrix ranks, would need a lower bound applying to every deterministic computation, not merely to a particular decomposition. We investigate the separator route and explicitly invalidate the simplest rank-based converse.

Attempt: a separator-to-algorithm lemma.

The primal graph of a CNF formula has one vertex per variable and an edge between variables occurring in a common clause. Consider a hereditary class of such graphs for which a deterministic polynomial-time procedure finds, on every $v$-vertex induced subgraph, a set $S$ of size at most $s(v)$ such that all components after deletion have at most $2v/3$ vertices. Suppose $s(v)=o(v)$, uniformly over that class.

Recursively delete separators until only bounded-size pieces remain. For each node make a bag containing its separator and all ancestor separators; leaves also contain their remaining variables. This is a tree decomposition: every vertex has connected bag occurrences, and an edge cannot connect two different components below the separator that first separates them. Every clause is contained in some bag, since its variables form a clique. The largest bag size $w+1$ is bounded by the sum of separator sizes along one root-to-leaf path, plus the leaf size.

Here the little-oh estimate really is uniform. Given $\epsilon>0$, choose $V_\epsilon$ so that $s(v)\le\epsilon v$ for $v\ge V_\epsilon$. Along a path the subproblem sizes decrease by a factor at most $2/3$. The contribution before reaching $V_\epsilon$ is at most \[ \epsilon n\sum_{j\ge0}(2/3)^j=3\epsilon n. \] The remaining path has bounded length and bounded bag contribution, depending on $V_\epsilon$ but not on $n$. Hence $w=o(n)$.

For completeness, SAT can be decided from this decomposition without a probabilistic step. At each bag store which Boolean assignments to the bag extend to satisfying assignments of all clauses allocated to its subtree. Check the clauses allocated to the bag and combine child tables by agreement on overlaps and existentially forgetting child-only variables. The separator property ensures there are no missing cross-child clauses. There are $2^{w+1}$ assignments per bag; even a naive pairwise implementation costs only $2^{O(w)}$ times a polynomial in the input and decomposition size. Thus the stated separator hypothesis gives a deterministic $2^{o(n)}\operatorname{poly}(|F|)$ algorithm on the class. This is an auxiliary algorithmic lemma, not a proof that all sparse formulas satisfy its hypothesis.

Attempt: the exact rate calculation with sparsification.

The sparsification theorem [E1], Section 2 and Corollary 1, says that for each fixed $\alpha>0$ a $3$-CNF on $n$ variables can be expressed as the disjunction of at most $2^{\alpha n}$ formulas on those variables, each with occurrence bound depending only on $\alpha$. The list is generated in time $2^{\alpha n}\operatorname{poly}(|F|)$. In particular every output formula has at most $D_\alpha n$ clauses, for a constant $D_\alpha$.

Suppose one could solve every fixed-density class $m\le Dn$ in time $2^{o_D(n)}\operatorname{poly}(|F|)$, for example by a valid extension of the preceding separator method. Solving all sparsified formulas would cost \[ 2^{\alpha n+o_{D_\alpha}(n)}\operatorname{poly}(|F|). \tag{45.1} \] For any proposed ETH constant $c>0$, fix $\alpha=c/3$. For sufficiently large $n$, the little-oh term is at most $cn/3$, so $45.1$ is bounded by $2^{2cn/3}\operatorname{poly}(|F|)$, with the finitely many smaller inputs absorbed into a constant. This supplies an algorithm within the rate excluded by that $c$. Consequently such a collection of sparse algorithms would refute the exact existential-rate formulation of ETH in the original entry.

The quantifiers here are important: the selected algorithm can depend on the fixed $c$, not on the growing input. We have not silently asserted that a non-effectively chosen family of algorithms automatically becomes one algorithm with a uniformly specified $2^{o(n)}$ running time. The rate calculation already contradicts the displayed target without that extra uniformization claim.

Stress test: sparse graphs need not have small separators.

Bounded-degree vertex-expander families exist; see [E3], Sections 2 and 4. Let $G$ be such a graph with maximum degree $d$ and expansion constant $h>0$, meaning every $U$ with $|U|\le n/2$ has at least $h|U|$ neighbors outside $U$. A separator $S$ whose remaining components have size at most $2n/3$ must have linear size. If $|S|\ge n/6$ this is immediate. Otherwise a union of components can be chosen with size between $n/6$ and $n/2$: choose one in that range, greedily combine smaller ones, or take the complement of a component larger than $n/2$ inside $G-S$. All external neighbors of this union lie in $S$. Therefore \[ |S|\ge hn/6\quad\hbox{or}\quad |S|\ge n/6. \tag{45.2} \] This disproves the universal graph-theoretic separator hypothesis even when the clause count is linear. Indeed \[ F_G=\bigwedge_{\{u,v\}\in E(G)}(x_u\lor x_v) \tag{45.3} \] is a $3$-CNF in the entry's "at most three literals" convention, has at most $dn/2$ clauses, and has primal graph $G$. Yet $45.3$ is satisfied by the all-one assignment and can be recognized as such immediately. Thus large separators do not prove computational hardness either. A successful extension would have to exploit the actual predicates or a sound semantic simplification, not just the primal graph.

A simple preprocessing calculation illustrates the remaining tradeoff. For a formula with $m\le Dn$, let $T$ contain variables with more than $\Delta$ occurrences. Since total occurrences are at most $3Dn$, $|T|\le3Dn/\Delta$. Enumerating $T$ costs at most $2^{3Dn/\Delta}$ branches, after which every remaining variable has at most $\Delta$ occurrences. This reduces high occurrence but leaves the bounded-degree obstruction $45.2$; it does not produce sublinear separators. It cannot be promoted to a subexponential algorithm by ignoring the cost of solving the residual instances.

Stress test: an exponential boundary rank is not ETH.

Consider $2b$ variables and the formula \[ E_b(x,y)=\bigwedge_{i=1}^b [(\neg x_i\lor y_i)\land(x_i\lor\neg y_i)]. \tag{45.4} \] The truth table across the cut $x\mid y$ is the $2^b$ by $2^b$ identity matrix, since $45.4$ holds precisely when $x=y$. It has rank $2^b$ over every field. Any representation as a sum of separated scalar products $\sum_{j=1}^r a_j(x)b_j(y)$ therefore requires $r\ge2^b$. Nevertheless the formula is trivially satisfiable, describes only pairwise equalities, and has a width-one decomposition if variables are ordered as pairs. Its matrix-free description has linear size.

The exact ranks for $b\le6$ are checked in the supplied script. The calculation refutes a lower-bound argument based on one chosen cut; it is not evidence against a better optimized representation. To prove ETH one would need to rule out all deterministic algorithms, including algorithms that never materialize that table. To disprove ETH using compression, one must give a uniform update procedure and account for all existential projections; naming a short formula for the original input does not show that its projections stay short.

Outcome.

Outcome: Exploratory approach with unresolved gap. The attempt proves a separator-based subexponential algorithm under a precise hereditary hypothesis, and shows exactly how sparse-instance algorithms with vanishing rate would contradict the stated ETH quantifiers. The unqualified separator hypothesis is false, as shown by explicit easy formulas on expanders. A separate exact construction shows why exponential boundary rank does not furnish an unrestricted time lower bound. These are auxiliary deductions, not assertions of historical novelty or a resolution of ETH. The unresolved step is a semantic decomposition or compression theorem handling every sparse formula with a genuinely vanishing exponential rate; no such theorem is supplied. Conversely no universal positive-rate lower bound is established. A proof of ETH would in particular prove $\mathsf P\ne\mathsf{NP}$.

Sources

• S1 R. Impagliazzo, R. Paturi, J. Comput. System Sci. 62$2$:367-375, 2001. https://doi.org/10.1006/jcss.2000.1727. Catalogue formulation source.
• S2 Complexity Theory: Stronger forms of P != NP, Roei Tell. https://www.cs.toronto.edu/~roei/2026%20complexity/6%20stronger%20lbs.pdf. Catalogue research/status reference; not a proof endorsement.
• E1 Russell Impagliazzo, Ramamohan Paturi and Francis Zane, Which Problems Have Strongly Exponential Complexity?, Journal of Computer and System Sciences 63 $2001$, 512--530, Section 2, especially Corollary 1 (sparsification). https://cseweb.ucsd.edu/~russell/ipz.pdf. Primary sparsification theorem and its uniform parameter dependence. Consulted 27 September 2026.
• E2 Sixue Liu, Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT, ICALP 2018, LIPIcs 107, 88:1--88:13, abstract and the deterministic $3$-SAT bound. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.88. A published algorithmic benchmark, not asserted to be a newly verified optimal bound. Consulted 27 September 2026.
• E3 Shlomo Hoory, Nathan Linial and Avi Wigderson, Expander graphs and their applications, Bulletin of the American Mathematical Society 43 $2006$, 439--561, Sections 2 and 4. https://www.cs.huji.ac.il/~nati/PAPERS/expander_survey.pdf. Existence and expansion properties of bounded-degree expanders. Consulted 27 September 2026.
• E4 Benjamin Bedert, Tamio-Vesa Nakajima, Karolina Okrasa and Stanislav Živný, Strong Sparsification for 1-in-3-SAT via Polynomial Freiman-Ruzsa, arXiv:2507.17878, full version of a FOCS 2025 paper, abstract. https://arxiv.org/abs/2507.17878. Adjacent sparsification result with a different constraint predicate. Consulted 27 September 2026.