A simplified proof of ETH is False [pdf]

Our simplified exposition of OpenAI’s proof [1] combines sparsification, bounded occurrences, spectral replacement, and rational interpolation.

1 The goal and the proof strategy A Boolean variable takes a value in {0, 1}, where zero means false and one means true.

A literal is a variable or its negation.

A clause is satisfied when at least one of its literals is true. A 3-CNF is a conjunction of clauses of at most three literals.

Given such a formula on n declared variables with m clauses, 3-SAT asks whether some assignment satisfies every clause.

An assignment specifies all declared variables, including any that occur in no clause. We allow n = 0 and m = 0, with the conventions below.

Our goal is an algorithm with an arbitrarily small exponential rate.

Theorem 1.1 contradicts this assertion by taking, for example, ε = δ/2.

The theorem asserts a family of algorithms, one for each fixed rate parameter ε.

This parameter is fixed before the input is given; the algorithm and its polynomial time factor may depend on it.

The main idea.

If the variables could be divided into small groups so that every clause used only one group, we could count satisfying assignments separately in each group and multiply the answers. The difficulty is that clauses link different groups. We remove these links algebraically. First express each clause by a polynomial equal to its truth value on Boolean inputs. In these polynomials, replace each variable occurrence by a linear expression whose coefficients depend polynomially on a parameter T .

At T = 0 the expression is the original variable.

At selected positive integers T = t, each deformed clause factor depends on variables in just one group and on a small collection of integer linear measurements (linear sums with integer coefficients). Each measurement uses variables from a single group. Once their values are fixed, both the factors and the constraints realizing those values separate by group, so the group ∗Email: [email protected] Homepage: shivakintali.github.io 1 sums can be multiplied. Summing the product of the deformed clause polynomials over all original Boolean assignments defines a polynomial H(T ).

At zero it equals the desired count.

At the other integer nodes its values need not be positive or integral; we use them as interpolation data to recover H(0). Specifically, we compute Taylor coefficients up to an order that is a small fraction of the variable count, at each selected integer, and interpolate.

There are two main tasks.

Section 2 shows how such a replacement gives a counting algorithm; its key observation is that a monomial in a low-order Taylor coefficient uses only a few formal variables. Section 3 constructs the replacement using commuting swap matrices and a polynomial that corrects their action on most basis directions.

Section 4 chooses the parameters and accounts for exact arithmetic.

After the two reductions below, we first deduce the main theorem from the counting proposition. The remaining sections then prove that proposition. We use elementary linear algebra, polynomial interpolation, and basic probability; the Boolean coefficient-extraction identity is derived when it is used. The only result about SAT complexity that we invoke without proof is the sparsification lemma stated below.

Conventions.

All logarithms have base two except ln, which is natural. For an integer k ≥ 0, write [k] = {1, .

. .

, k}.

Repeated input clauses count separately. An empty conjunction is true; an empty disjunction, including an empty clause, is false. A clause is tautological if it contains both a variable and its negation. After deleting tautological clauses and repeated literals within a clause, the number of occurrences of a variable is the number of clauses containing it. Variables are indexed by [n], and input clauses are listed explicitly using binary variable indices and clause delimiters. Running-time bounds count bit operations and include reading this encoding; intermediate arithmetic-operation counts are explicitly identified. We write polyθ(u) for a polynomial upper bound in u whose constants and degree may depend on the fixed parameter θ; we use this notation with θ = s or θ = ε. Empty products equal one and empty sums equal zero. The coefficient `1 norm is the sum of the absolute values of the coefficients. This norm will bound the range of our integer measurements and the size of the numbers used in exact arithmetic. 1.1 Reducing to bounded occurrences The first reduction makes the number of clauses linear in the number of variables. It produces several formulas, and the original formula is satisfiable exactly when at least one of them is satisfiable.

Lemma 1.2 (Decision sparsification [3, Corollary 1, p.

523]). For every fixed η > 0, a deterministic algorithm expresses a 3-CNF F on n declared variables as F ≡ L∨ i=1 Fi, 0 ≤ L ≤ 2ηn, where each Fi is a 3-CNF on the same declared variables with at most Cηn clauses.

The total construction time is 2ηn(n + m + 1)Oη (1). Here Cη depends only on η.

To apply the cited result, first remove tautological clauses, repeated literals within a clause, and duplicate clauses. These operations preserve the satisfying assignments and take polynomial bit time in n + m + 1. All declared variables are retained even if they no longer appear. If an empty clause is present, use L = 0; if no clauses remain, use L = 1 with F1 the empty conjunction. These conventions also cover n = 0. For every other input, the cited construction applies to clauses of width at most three; its polynomial work, including binary encoding costs, is absorbed by the 2 displayed time bound. The equivalence is an equality of Boolean functions. Disjointness of the solution sets is unnecessary: we only ask whether at least one Fi is satisfiable. The second reduction limits how many clauses can use the same variable. It preserves satisfiability; two formulas with this relationship are called equisatisfiable. We give each occurrence its own copy and enforce agreement with a cycle of implications. Bounded occurrences will later let us balance the formula’s incidences among an auxiliary array’s positions.

Lemma 1.3 (Bound the occurrences).

A 3-CNF with n declared variables and m clauses can be transformed using polynomially many bit operations in n + m + 1 into an equisatisfiable 3-CNF with N ≤ n + 3m declared variables in which each variable occurs in at most three clauses. The output has at most 4m clauses.

Proof.

First remove tautological clauses and repeated literals within a clause. If an empty clause occurs, return the single empty-clause formula on the same declared variables; all claimed bounds hold because then m ≥ 1. Otherwise, let m′ be the number of remaining clauses, and let dx count the occurrences of variable x in them. For d = dx ≥ 2, replace its occurrences by x1 = x, x2, .

. .

, xd, preserving their signs. All newly introduced copies are fresh variables, distinct across all original variables. Add the cycle d∧ i=1 (¬xi ∨ xi+1), xd+1 := x1. The cycle is satisfied exactly when all copies agree. If any copy is one, the implications force every copy around the cycle to be one; the all-zero assignment also satisfies the cycle. This includes d = 2, where the two clauses give the two directions of an equivalence. Every satisfying assignment of the original formula extends to a satisfying assignment of the output by giving each copy its original variable’s value. Conversely, any satisfying assignment of the output has equal copies, and reading x1 for each copied variable satisfies every original clause. Thus the formulas are equisatisfiable.

The extension is in fact unique. Variables with zero or one occurrence are retained.

Each copy appears in one rewritten original clause and two cycle clauses, so it occurs at most three times. Since ∑ x dx ≤ 3m′ ≤ 3m, the exact variable and clause counts obey N = n + ∑ x:dx≥2 (dx − 1) ≤ n + 3m, mout = m′ + ∑ x:dx≥2 dx ≤ 4m. The new clauses have width two, so the width bound remains three. Scanning the clauses, assigning fresh indices, and writing the output all take polynomially many bit operations in n + m + 1. It remains to solve these bounded-occurrence formulas at arbitrarily small exponential rates.

The following statement will be proved without assuming any of the new lemmas of [1].

The parameter s is a fixed integer controlling the exponential rate; it is never the input length.

All constants depending on s may be large. 3 1.2 How the counting proposition implies the main theorem We allocate half of the allowed exponential rate to sparsification and half to solving its output formulas. The bounded-occurrence reduction enlarges the variable count by a constant factor. We therefore choose the counting parameter s only after that factor is known.

Deduction of Theorem 1.1 from Proposition 1.4.

It suffices to consider rational ε > 0: a smaller positive rational target implies the bound for any prescribed real ε > 0.

Fix such an ε, and put η = ε/2.