3-SAT

Given a formula in conjunctive normal form with $n$ variables and $m$ clauses, where each clause is an OR of at most three variables or negated variables, decide whether some assignment makes every clause true. Time counts bit operations on the standard encoding of the formula, on every input and on every run. The algorithm can use random bits: on every input, it must give the correct answer with probability at least $2/3$. A deterministic algorithm also qualifies. $O^*$ hides factors $(n+m)^{O(1)}$.

Classic bound: $O^*(1.307031578^n)$ (Jiang and Cai 2026, preprint).

The bound has the form $O^*(2^{n/(\log n)^{\alpha-o(1)}})$. $\alpha$ is the exponent of $\log n$ in the denominator; higher is better. The term $o(1)$ means that for every fixed $\varepsilon>0$, the time is at most $(n+m)^{O(1)}2^{n/(\log n)^{\alpha-\varepsilon}}$ for all large $n$. Every bound $c^n$ with a constant $c>1$, such as the classic bound or trying all assignments, has $\alpha=0$: $c^n=2^{n\log_2 c}$ is at most $2^{n(\log n)^{\varepsilon}}$ for every $\varepsilon>0$ and large $n$, but more than $2^{n/(\log n)^{\varepsilon}}$. The Exponential Time Hypothesis states that 3-SAT needs time $2^{cn}$ for some constant $c>0$, also with random bits; any $\alpha>0$ refutes it.

• What counts as Claimed: Published results for this problem without a qualifying repository review or Lean proof check.
• What counts as Human Verified: This problem has no community repo with a qualifying review rule.
• What counts as Lean Verified: A result shows here when we rebuild its Lean proof from source and check, with the Lean kernel, that it proves our exact problem statement.