Dinur's gap theorem for 3-SAT

The mathematical conclusion of the development. Every 3CNF formula is turned into a constraint graph over a fixed constant-size alphabet, of size polynomial in the formula, which is satisfiable when the formula is and whose unsatisfiability value is at least a universal constant when it is not.

Three ingredients meet: the reduction of ThreeSATCSP carried across alphabets by GapReduction, the expander family of ExpanderExists, and the amplifier of Dinur, whose dichotomy supplies the gap after logarithmically many rounds.

What this does not supply is computability. gapGraph is defined through Classical.choose — the expander family is obtained by counting, not constructed — so it is a reduction in the mathematical sense only. Turning it into a PCPVerifier, which additionally demands an FP query function and a P verdict, needs an explicit expander family and a polynomial-time implementation of every round.

Main definitions

• Complexity.dinurAmp — Dinur's amplifier, with the expander supplied
• Complexity.gapGraph — the gap graph of a formula

Main results

• Complexity.satisfiable_gapGraph — completeness
• Complexity.gap_le_unsatVal_gapGraph — soundness, with a universal gap
• Complexity.numEdges_gapGraph_le — the size bound

noncomputable def Complexity.dinurAmp : Amplifier DinurAlpha

Dinur's amplifier, with the expander family supplied.

Equations

• Complexity.dinurAmp = Complexity.Dinur.amplifier Complexity.algFamily

def Complexity.gapRounds (φ : SAT.CNF) : ℕ

How many rounds of amplification a formula needs: enough that the doubling of the unsatisfiability value reaches the threshold, which is the bit length of the edge count.

Equations

• Complexity.gapRounds φ = Nat.log 2 (3 * List.length φ) + 1

theorem Complexity.numEdges_baseCSP_le_pow_rounds (φ : SAT.CNF) : (baseCSP φ).numEdges ≤ 2 ^ gapRounds φ

noncomputable def Complexity.gapGraph (φ : SAT.CNF) : ConstraintGraph DinurAlpha

The gap graph of a formula: logarithmically many rounds of amplification applied to its constraint graph.

Equations

• Complexity.gapGraph φ = Complexity.dinurAmp.iter (Complexity.gapRounds φ) (Complexity.baseCSP φ)

theorem Complexity.satisfiable_gapGraph {φ : SAT.CNF} (h3 : φ.Is3CNF) (h : φ.Satisfiable) : (gapGraph φ).Satisfiable

Completeness.

theorem Complexity.gap_le_unsatVal_gapGraph {φ : SAT.CNF} (h3 : φ.Is3CNF) (h : ¬φ.Satisfiable) : dinurAmp.gap ≤ (gapGraph φ).unsatVal

Soundness, with a gap that does not depend on the formula.

theorem Complexity.dinurAmp_gap_pos : 0 < dinurAmp.gap

The gap is a positive constant.

theorem Complexity.dinurAmp_gap_le_one : dinurAmp.gap ≤ 1

The gap is at most one, as any unsatisfiability value is.

theorem Complexity.two_pow_log_succ_le (n : ℕ) : 2 ^ (Nat.log 2 n + 1) ≤ 2 * n + 2

A bit length costs at most a doubling.

theorem Complexity.numEdges_gapGraph_le (φ : SAT.CNF) : (gapGraph φ).numEdges ≤ (2 * (3 * List.length φ) + 2) ^ (Nat.log 2 dinurAmp.edgeFactor + 1) * (3 * List.length φ)

The size bound: a constant factor per round, and logarithmically many rounds, so polynomially many edges.