The ACE Complexity Lab

A · EXPONENTIAL GROWTH

Why 2ⁿ wins every argument.

A formula with n true-or-false variables has 2ⁿ possible assignments. Checking them all is the brute-force baseline every SAT result is measured against. Move the slider and watch how quickly the number stops being something you can wait for.

B · SAT PLAYGROUND

Solve a real formula.

A 3-SAT formula is a list of clauses. Each clause is three literals joined by OR, and the whole formula is satisfied when every clause has at least one true literal. Write one clause per line as numbers ending in 0, the DIMACS style: 1 -2 3 0 means x1 or not x2 or x3.

Random 3-SAT has a sharp transition at about 4.26 clauses per variable. Below it most formulas are satisfiable, above it most are not, and the hardest instances cluster right at the edge. Try the ratio slider either side of 4.26.

C · SEARCH TREE

Watch DPLL prune the search.

DPLL guesses a variable, then follows the consequences. When a clause has only one literal left, that literal is forced (unit propagation). When a variable only ever appears one way round, it can be set that way for free (pure literal). A clause with nothing left is a conflict and the solver backs up. Every forced literal is a branch that never needs exploring.

D · THE NEW MATHEMATICS

Counting by polynomials, in plain words.

The paper does not search for one solution. It counts all of them exactly, which is harder, and it does it with algebra rather than branching. Here is the construction from Sections 2.2 to 2.5, as I understand it.

1. Clauses become polynomials. A clause like x1 or not x2 or x3 becomes Φ = 1 − (1 − x1)·x2·(1 − x3). On true-or-false inputs it is 1 when the clause is satisfied and 0 when it is not.
2. The count is a sum of products. Multiply every clause polynomial together and add the result over all 2ⁿ assignments: the total is exactly the number of satisfying assignments, #F. Done naively, that is brute force again.
3. Bend the inputs with a parameter T. Each place a variable is used inside a clause is replaced by a linear form that equals the variable exactly when T = 0 but can be something easier at T = 1, 2, …, Q. That defines a polynomial H(T) with H(0) = #F.
4. Split variables into groups that only talk through measurements. At each easy point, the variables fall into groups. A clause may reach outside its own group only through a few integer “measurements” of another group, such as how many of its variables are true.
5. Fix the measurements and the sum factorises. Enumerate every possible tuple of measurement values. For a fixed tuple, each group can be summed on its own, and the group sums simply multiply. Adding over all tuples gives H(t) exactly.
6. Recover T = 0 from the easy points. A few values of H are not enough to pin it down, so the method computes Taylor coefficients at each point, using inclusion-exclusion to keep the groups separate, then solves a Hermite interpolation system over exact rationals. The constant term is the count.
7. General formulas first become sparse ones. Any k-CNF is reduced to bounded-occurrence pieces with counting-preserving sparsification and variable copying, so the method above applies.
8. The sharpest bound is tensor contraction. Appendix D recasts the whole thing as contracting a Boolean tensor network recursively, working modulo powers of two (2-adically), and that is where the 2^{O(n/√log n)} rate for sparse formulas comes from.

What is genuinely new is how the paper builds the bent linear forms so that very few measurements are needed while the degree stays low (Section 4), and the 2-adic recursion in Appendix D. Arithmetisation, split-and-sum and interpolation are older tools, credited in the paper.

The catch for practice: the number of groups grows like √log n divided by (log log n)². By my reading of the parameter choices, that only reaches 2 when n is around e¹⁰⁰⁰⁰⁰. For any formula a computer could store, the method gives no speed-up over brute force at all. It is a theorem about the shape of the curve, not a faster solver.

E · ACE EXPERIMENTS

What we measured in our own code.

The paper itself will not speed up a web server. The habit behind it, asking whether the obvious exhaustive approach is really the limit, does. These are before-and-after measurements from ACE projects. Each one lists its input, the spread of runs and what we gave up for the gain.

SOURCES

Where this comes from.

• The repository: github.com/openai/math
• The paper: preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf, Theorem 1.1, Sections 2.2 to 2.5 and Appendix D
• The Lean formalisation notes: lean/docs/378.md
• My article: AI challenged a fundamental limit of computing

The solver, the tree and the miniature are my own small implementations for teaching. They are checked against exhaustive enumeration, but they are not the paper's algorithm at scale and make no claim about its correctness.