OpenAI’s 3-SAT Result Depends on a Proof Still Awaiting Verification

OpenAI’s paper claims an algorithm that refutes the Exponential Time Hypothesis (ETH), an assumption that some problems cannot be solved substantially faster than by searching exponentially many possibilities. The paper does more than argue that a faster method might exist: it gives a deterministic algorithm for counting satisfying assignments of a Boolean formula.

As Károly Zsolnai-Fehér explains, 3-SAT asks whether there is an assignment of true and false values that satisfies every clause in a formula, where each clause contains three variables or their negations. In his example, one clause can be satisfied by making the cat sleep. Add a second clause that requires the cat to be awake, and that choice no longer works for both. A different variable—the dog or the robot—may satisfy both clauses. With many variables and clauses, the task is to find an assignment that works across the entire formula.

A brute-force approach checks every assignment. For n variables, that means considering exponentially many combinations. Zsolnai-Fehér illustrates the scale by saying that a processor checking a billion combinations per second could take a quadrillion years to finish. Researchers have devised smarter algorithms, and these can outperform brute force; in his account, however, none had broken the exponential barrier in the general case. The chart in the presentation marks improvements from 1985, 1999, and 2019, while showing them still on the exponential side of that barrier.

ETH is not presented as a proved theorem. Zsolnai-Fehér says many researchers have accepted the assumption and built further results on it. OpenAI’s claim, if its proof holds up, would overturn that assumption.

The paper’s abstract states a result for every fixed k ≥ 2: a deterministic algorithm exactly counts the satisfying assignments of an arbitrary k-CNF formula with n variables and m clauses. It uses space polynomial in n and m, for fixed k, and runs in time (n + m)^{O_k(1)} 2^{n / (log n)^{1/2 + o(1)}}.

The abstract says this refutes ETH, which postulates that deciding 3-SAT on n variables requires 2^{Ω(n)} time in the worst case. An exact count also answers the decision question: if the count is greater than zero, a satisfying assignment exists; if it is zero, none exists. Thus, the counting result gives a way to decide whether a 3-CNF formula has a solution. The source’s shorthand is a sub-exponential bound for 3-SAT: the stated exponential factor grows more slowly than 2^n.

Two features matter in Zsolnai-Fehér’s explanation. The paper supplies the algorithm itself, rather than only proving that some faster algorithm must exist. And the algorithm counts satisfying assignments exactly; it does not merely report whether a solution exists. The abstract states the counting result for arbitrary k-CNF formulas with fixed k, while the source highlights the implication for 3-SAT.

Zsolnai-Fehér connects the result to other problems through Karp reductions: transformations that encode one problem as another. He gives examples that include finding an efficient route to deliver medicine to hospitals, assigning radio frequencies to transmitters to limit interference, choosing sensors to monitor a system, and selecting valuable equipment to fit on a spacecraft.

These tasks look different, but, he says, they can be molded into the form of a satisfiability problem. In his illustration, roads are transformed into questions about cats and dogs. If an algorithm solves that target problem faster, the improvement can sometimes carry back to the original one. The transfer is not automatic in every case, Zsolnai-Fehér cautions, though it often applies. The point of the examples is that a result about satisfiability can matter beyond the logic problem itself.

Zsolnai-Fehér says the proof looked increasingly convincing to him, but proper verification was still needed and expert review was not complete. If it holds up, he says, an important assumption in theoretical computer science will have fallen.

He also distinguishes ETH from the P versus NP question: that question has not been solved. The claim is about refuting ETH with a sub-exponential algorithm for 3-SAT, not about proving that P equals NP.