Beat PPSZ's Θ(1/k) savings for k-SAT — solve k-SAT in 2^{n(1 - ω(1/k))} time

Record

2^{n(1 - c_k/k)} time with c_k → π²/6 ≈ 1.645 (PPSZ savings)

Record held by

Paturi, Pudlák, Saks & Zane, JACM 2005; general (non-unique) case by Hertli, SICOMP 2014

Hardness

no 2^{o(n)} algorithm for any fixed k ≥ 3 unless ETH fails; SETH asserts the exponent tends to n as k grows

Hardness from

Impagliazzo & Paturi, JCSS 2001

Endgame

no direct implication published (Vyas & Williams, SAT 2019, prove none), but one published route is two-for-one: optimal bounds for the local-enumeration problem Enum(k,t) would simultaneously beat PPSZ savings (k-SAT in 2^{n(1-Ω(log k/k))}) and give 2^{ω(sqrt n)} depth-3 circuit lower bounds (Gurumukhani, Paturi, Pudlák, Saks & Talebanfard, CCC 2024, arXiv:2403.09134)

Hypotheses

SETH, Super Strong ETH

Problems

k-SAT

Statement

For k-SAT (satisfiability of CNF formulas with clauses of width at most k), every known algorithm runs in time 2^{n(1 - Θ(1/k))}: the "savings" over brute force is a constant divided by k. Find an algorithm whose savings grow asymptotically faster — running time 2^{n(1 - s(k)/k)} with s(k) → ∞, for example savings of order (log k)/k — or give evidence this is impossible by deriving a Θ(1/k) barrier from a standard hypothesis.

Current record

PPSZ (Paturi–Pudlák–Saks–Zane, JACM 2005) solves k-SAT in time 2^{n(1 - μ_k/k)} where the constant μ_k increases to π²/6 ≈ 1.645 as k grows; Hertli (SICOMP 2014) removed the unique-solution assumption. Subsequent improvements (biased PPSZ and successors) improve the constant for small k but not the Θ(1/k) shape. The statement that Θ(1/k) savings is optimal has been studied under the name "Super Strong ETH" (see Vyas & Williams, "On Super Strong ETH", SAT 2019, and Scheder & Talebanfard, CCC 2020, who constructed instances on which even the strong PPSZ variant with bounded-width resolution has savings at most (1 + o(1))·2/k — so PPSZ-type algorithms themselves cannot achieve ω(1/k) savings). As of 2026-08 the Θ(1/k) shape still stands: the newest published improvements (e.g., Scheder, "PPSZ for General k-SAT and CSP — Making Hertli's Analysis Simpler and 3-SAT Faster", computational complexity 2024) again move only the constant. No consequence links Super Strong ETH to SETH or ETH in either direction: it could fail while SETH holds, or vice versa.

Why it matters

SETH (the Strong Exponential Time Hypothesis) says the base for k-SAT tends to 2 as k → ∞, and it is the load-bearing assumption behind dozens of fine-grained lower bounds. This problem asks a sharper quantitative question: not just whether the base tends to 2, but how fast. An algorithm with ω(1/k) savings would be the first structural progress on k-SAT beyond the PPSZ framework and would immediately tighten every reduction that pays attention to the savings function (e.g., hardness for Orthogonal Vectors and its descendants is calibrated to savings). Conversely, a reduction showing that ω(1/k) savings implies a breakthrough elsewhere would give SETH a quantitative moat. The savings function is also entangled with unconditional lower bounds: Gurumukhani, Paturi, Pudlák, Saks and Talebanfard (CCC 2024) show that optimal bounds for a single transversal-enumeration problem would simultaneously push k-SAT savings to Θ((log k)/k) and yield 2^{ω(sqrt n)} depth-3 circuit lower bounds, so the natural attack route here doubles as a circuit-lower-bound program.

Attack surface

(1) Restricted instance classes first: for random k-SAT and for formulas with bounded clause density, better-than-PPSZ savings have been claimed in special regimes — mapping exactly which regimes is a good literature task, and extending any of them toward worst case is the prize. (2) Width reduction: the Impagliazzo–Paturi–Zane sparsification lemma is the standard preprocessing step, and its exponential blowup in 1/ε is one identified bottleneck; improved sparsification would propagate directly. (3) The polynomial method of Abboud–Williams-style SAT algorithms gives superior savings for depth-two circuits with few gates; pushing it to unrestricted CNF with m = O(n) clauses is a concrete first target.