Does OpenAI's SAT Solver Break the ETH?

Episode 1 · minilek and Ryan Williams Debate Whether ETH Still Holds (2026-10-28, 7 posts)

From October 28 to 29, Duke professor minilek (Donald Knuth's biographer and founder of ACM CSSI) and theoretical computer scientist Ryan Williams held a multi-round technical exchange on X about the Exponential Time Hypothesis (ETH), prompted by questions arising from Williams's new work refuting the Strong Exponential Time Hypothesis (SETH).

Confirmed

• minilek's core question: beyond the empirical fact that "smart people just haven't found faster algorithms," is there any substantive historical reason to believe ETH should hold?
• Williams acknowledged that a series of papers has pushed the exponential base for SAT down from 2^n to smaller c^n (the posts mention a trivial 1.913^n algorithm), so the premise "no algorithm beats brute force" has long been false—one reason he was skeptical of ETH back in the day.
• When minilek pressed on whether the best known SAT algorithms (e.g., PPSZ-type (2-ε)^n subexponential algorithms) fall under some lower-bound constraint, Williams replied that all known extensions of these algorithms are still consistent with ETH; exponential-time lower bounds (e.g., ruling out 2^{o(n)} algorithms) hold only for restricted algorithm classes such as resolution-based methods—which happen to characterize the main behavior of modern SAT solvers.
• minilek also asked whether the known (2-ε)^n algorithms can be unified under some broad, natural algorithm class; the discussion touched on fine-grained complexity (SETH-related) frameworks.

Why it matters

• ETH/SETH underpin a vast body of conditional lower bounds (i.e., "unless ETH fails, problem X has no fast algorithm"). If their foundation shakes, all hardness results relying on them need reexamination.
• The conversation cleared up a common misconception: lower bounds do not hold against all algorithms, only against restricted models such as resolution; modern SAT solvers happen to fall largely within such models, which keeps these lower bounds explanatorily relevant in practice. The relationship between algorithms like PPSZ and lower-bound conditions is precisely the key boundary for judging whether ETH is threatened by existing techniques.

• Is ETH still credible? A trivial 7^n/3 = 1.913^n SAT algorithm raises doubts — minilek · 2026-10-28
• Ryan Williams: c^n breakthroughs made "brute force is optimal" already false — rrwilliams · 2026-10-28
• Did prior SOTA algorithms like PPSZ meet the resolution-based lower bound conditions? — minilek · 2026-10-29
• Ryan Williams explains why PPSZ and resolution-based SAT methods obey ETH — rrwilliams · 2026-10-29
• Theorists debate whether known SAT algorithms like PPSZ fall under ETH lower bounds — minilek · 2026-10-29
• Does a natural algorithm class capture all known 2^(-εn) subexponential k-SAT algorithms? minilek probes PPSZ's limits — minilek · 2026-10-29
• Williams recalls: resolution-based methods were known to obey ETH before SETH breakthrough — quantum_aram · 2026-10-29

Episode 2 · Theorist Ryan Williams Explains OpenAI's ETH-Breaking Solver as Split and List (2026-10-30, 2 posts)

Ryan Williams analyzes OpenAI's ETH-violating solver as a "split and list" approach, noting that brute-force enumeration within blocks alone breaks ETH and further improvements may be possible.

• Ryan Williams: OpenAI's ETH-violating solver fits the "split and list" algorithm class — rrwilliams · 2026-10-30
• Williams: ETH-breaking strategy still brute-forces within pieces, more gains ahead — rrwilliams · 2026-10-30