Strong Exponential Time Hypothesis (SETH)

Strong Exponential Time Hypothesis (SETH)

Definitions and mathematical statement

For each fixed $k$, let \[ s_k=\inf\{s\ge0:k\text{-SAT on }n\text{ variables is decidable in } O(2^{sn}\operatorname{poly}(|F|))\text{ deterministic time}\}. \] The strong exponential time hypothesis is $\lim_{k\to\infty}s_k=1$. Equivalently, for every $\varepsilon>0$ some fixed clause width $k$ rules out a deterministic $O(2^{(1-\varepsilon)n}\operatorname{poly}(|F|))$ algorithm. The algorithm may depend on $k$; the claim is not that every fixed-width SAT problem has exponent one.

Formulation and concept references: [S1].

Short English statement

As clause width grows, must the best deterministic SAT exponent approach exhaustive-search exponent one?

Research attempt

Current frontier.

The target takes the limit of optimal deterministic exponents after fixing the clause width [S1]. An exponent below one for each $k$ does not refute SETH if the saving tends to zero. Efremenko--Itsykson prove a strong lower bound for bounded-depth resolution over parities, not for every deterministic SAT algorithm [E1]. The recent conditional applications in the catalogue likewise do not prove their SETH premise. We attempt a width-independent algorithmic saving and test its proposed representation of eliminated variables.

Attack route.

A lower bound for every algorithm must go beyond a chosen branching or refutation model. An algorithmic route could eliminate a linear-size variable block while summarizing its influence on the remaining variables. The missing condition is not merely the ability to project constraints, but a sufficiently small total cost of building and using the projection. We derive that cost exactly and test a compact-CNF repair.

Attempt: the easy fixed-width gain has the wrong limit.

For a $k$-CNF on $n\ge k$ variables, choose a nonempty clause and extend its variable set to $k$ variables. At least one of the $2^k$ assignments falsifies the clause. Branch on the other assignments, simplify, and stop at empty clauses or an empty conjunction. With polynomial work at each node, the recurrence has the form \[ T_k(n)\le(2^k-1)T_k(n-k)+\operatorname{poly}(|F|). \] Charging work to the search-tree nodes, rather than multiplying a new polynomial at every recursive level, gives \begin{equation}\label{wsref-0-72-36-35-3a-62-72-61-6e-63-68} T_k(n)=O\!\left((2^k-1)^{n/k}\operatorname{poly}(|F|)\right),\qquad \alpha_k=\frac{\log_2(2^k-1)}{k}<1. \end{equation} Here $\alpha_k=1+k^{-1}\log_2(1-2^{-k})\to1$. The $k=1$ case is directly polynomial. Thus this complete deterministic algorithm is consistent with SETH.

A block-elimination bound with all boundary costs counted.

Choose a block $B$ of $t$ variables. Let $C$ consist of outside variables in clauses meeting $B$, and let $b=|C|$. Write $F_B$ for those clauses and $F_0$ for the others. Define \[ R_B(c)=1\quad\Longleftrightarrow\quad \exists u\in\{0,1\}^{B}:F_B(u,c)=1. \] Then \begin{equation}\label{wsref-0-72-36-35-3a-70-72-6f-6a-65-63-74-69-6f-6e} F\text{ satisfiable}\ \Longleftrightarrow\ \exists x\in\{0,1\}^{V\setminus B}:F_0(x)=1\text{ and }R_B(x|_C)=1. \end{equation} A standard multitape implementation can stream through all $c$. For each, compute $R_B(c)$ by enumerating the $2^t$ internal assignments; when it is true, enumerate assignments of the remaining $n-t-b$ variables and test $F_0$. Thus no free random-access table lookup is assumed. The total time is \begin{equation}\label{wsref-0-72-36-35-3a-63-6f-73-74} \operatorname{poly}(|F|)\left(2^{t+b}+2^{n-t}\right), \end{equation} and the enumerations themselves need only polynomial work space.

\begin{notebookproposition} Suppose an absolute $\delta>0$ has the following property. For every fixed $k$, a polynomial-time procedure finds in each $k$-CNF a block with \[
 t\ge\delta n,\qquad t+b\le(1-\delta)n,
\] except on instances already decidable in time $O(2^{(1-\delta)n}\operatorname{poly}(|F|))$. Then SETH is false. \end{notebookproposition}

No such decomposition theorem is proved. Dense primal graphs defeat a purely graph-based argument: when every pair of variables occurs in a clause, every nonempty proper block has $t+b=n$. Even easy positive 2-CNF examples have this graph. Thus the criterion is sufficient but not necessary; a proof cannot simply assume that hard instances have small boundaries.

Attempted repair: exact projection as a short CNF.

Maybe a large boundary could still be summarized by a short CNF. Take boundary bits $x_1,\ldots,x_b$ and auxiliary bits $z_2,\ldots,z_b$. Enforce \[ z_2=x_1\oplus x_2,\qquad z_j=z_{j-1}\oplus x_j\ (3\le j\le b), \qquad z_b=0. \] The constraint $w=u\oplus v$ is exactly the conjunction \[ (u\vee v\vee\neg w),\quad(u\vee\neg v\vee w),\quad (\neg u\vee v\vee w),\quad(\neg u\vee\neg v\vee\neg w). \] This gives $O(b)$ clauses of width at most three. Existentially eliminating all auxiliary variables produces precisely even parity on the $b$ boundary bits.

\begin{notebooklemma} Every CNF on just the boundary variables that computes even parity has at least $2^{b-1}$ non-tautological clauses. \end{notebooklemma}

So exact auxiliary-variable elimination can turn a linear-size 3-CNF into an exponentially large CNF on its boundary. This disproves the hoped-for general compact-CNF projection lemma. It does not prohibit a compact circuit or parity representation of the same relation; parity itself is easy. Nor does it show that every input defeating the block criterion is hard for SAT.

Stress test.

The boundary variables are included in the construction cost, and the multitape implementation streams rather than assuming unit-cost access to an exponentially large array. A saving $\delta_k\to0$ would not contradict SETH. The parity lower bound concerns formulas after removing all auxiliaries; retaining auxiliary variables would invalidate its hypothesis. The verification script checks the four XOR clauses and all boundary/auxiliary assignments for $2\le b\le7$, and compares the projected truth table with even parity. The universal exponential lower bound follows from the proof, not from these finite checks.

A uniform exponent improvement would refute SETH but would not automatically give $\mathsf P=\mathsf{NP}$. Conversely, failure of this elimination strategy or a lower bound in the resolution system of [E1] would not establish SETH. The deterministic and unrestricted quantifiers in the target remain unchanged.

Outcome.

Outcome: Exploratory approach with unresolved gap.

The attempt supplies a width-uniform sufficient block criterion for a SETH refutation and an exact exponential obstruction to one proposed projection representation. The missing step is a different representation with a uniform construction-and-evaluation bound, or another mechanism giving an absolute exponent saving. Neither a universal speedup nor a lower bound for all deterministic algorithms is established.

Sources

• S1 C. Calabro, R. Impagliazzo, R. Paturi, J. Comput. System Sci. 74$3$:367-381, 2008. https://doi.org/10.1016/j.jcss.2007.07.007. Catalogue formulation source.
• S2 Strong ETH Holds for Bounded-Depth Resolution over Parities. https://eccc.weizmann.ac.il/report/2025/188/. Catalogue research/status reference; not a proof endorsement.
• S3 Tight (S)ETH-based Lower Bounds for Pseudopolynomial Algorithms for Bin Packing and Multi-Machine Scheduling. https://arxiv.org/abs/2603.12999. Catalogue research/status reference; not a proof endorsement.

• E1 Klim Efremenko and Dmitry Itsykson, Strong ETH Holds for Bounded-Depth Resolution over Parities, ECCC TR25-188 (20 November 2025). https://eccc.weizmann.ac.il/report/2025/188/. A lower bound for a specified proof system, not all deterministic SAT algorithms. Consulted 27 September 2026.