A 2^O(n) Time Algorithm for 3-SAT

The work gives a deterministic algorithm for counting satisfying assignments of 3-CNF formulas, a task at least as hard as deciding whether such a formula is satisfiable. Its stated running time is \(2^{O(n\log\log n/\sqrt{\log n})}\), where \(n\) is the number of variables. Because this is subexponential in \(n\), it contradicts the Exponential Time Hypothesis (ETH), which asserts that 3-SAT cannot be solved in subexponential time. The result is asymptotic: it does not claim that the method is useful on practical instances.

The central idea is to accelerate tensor-network contraction on complete graphs. A recurrence bounds the contraction exponent for a larger graph in terms of a smaller one. To obtain it, the proof places nodes on a grid and represents each rectangle’s crossing diagonals as a swap; expanding swaps into identity and singlet terms and grouping by singlet count yields low-rank operators. For each combination of operators, rows or columns are merged according to which is cheaper, then regrouped into balanced classes. This recursive improvement ultimately gives the algorithm. The repository also provides a Lean 4 formalization of the main theorem and the ETH refutation, checked against Mathlib and a second kernel. Its condensed proof sketch establishes the qualitative conclusion that 3-SAT admits a \(2^{\delta n}\)-time algorithm for every \(\delta>0\), but not the sharper counting bound.