Dinur's gap theorem

The combinatorial heart of Dinur's proof of the PCP theorem Dinur, Corollary 4.2: every formula φ in 3-CNF with m clauses yields a constraint graph gapGraph φ over the fixed alphabet Σ₀ = Bool × (Fin 6 → Bool) with polynomially many vertices and edges in m (exists_card_gapGraph_le), which is satisfiable exactly when φ is (satisfiable_gapGraph_iff), and whose value is at least the universal constant Cslib.PCP.Dinur.gap when φ is unsatisfiable (gap_le_unsatVal_gapGraph). As the construction can be carried out in polynomial time Dinur, Theorem 4.1, telling the two cases apart is as hard as 3-SAT: this is the PCP theorem in its gap form. This module proves its combinatorial half; the polynomial-time half is Cslib.PCP.Encoded.isPolyTime_gapGraph.

The construction:

1. the constraint graph ofCNF φ of the formula, with 3 m edges, over the alphabet Fin 3 → Bool, satisfiable exactly when φ is;
2. preprocessed and composed (cnfGraph φ): its vertices become the half-edges, so the variables of φ disappear, and its alphabet becomes Σ₀; it has a number of edges linear in m;
3. then ⌈log₂ |E|⌉ rounds of Dinur's amplifier (Cslib.PCP.Dinur.amplifier), which double the value up to the threshold: since an unsatisfiable graph with |E| edges has value at least 1 / |E|, the value reaches the threshold, while the size grows by a factor polynomial in |E|.

Everything here is a noncomputable definition: the expanders of preprocessing are chosen non-constructively (Cslib.RotationMap.expanderFamily). The polynomial-time realization, which needs explicit expanders Dinur, Lemma 2.2, is the separate pipeline Cslib.PCP.Encoded.gapGraph in Complexity.Computability.PCP.Encoded.GapTheorem, built on the explicit arithmetic expander family; it is the construction the PCP theorem uses. As the function gapGraph is fixed, the theorems below are not mere existence statements, which would be trivial: a function deciding satisfiability could output one fixed graph of each kind.

Main definitions

• Cslib.PCP.Dinur.round: Dinur's round on bundled constraint graphs.
• Cslib.PCP.Dinur.amplifier: Dinur's round as a gap amplifier.
• Cslib.PCP.Dinur.cnfGraph: the constraint graph of a formula over Σ₀.
• Cslib.PCP.Dinur.gapGraph: the gap graph of a formula.

Main results

• Cslib.PCP.Dinur.satisfiable_gapGraph_iff: completeness and soundness, qualitatively.
• Cslib.PCP.Dinur.gap_le_unsatVal_gapGraph: the gap.
• Cslib.PCP.Dinur.unsatVal_gapGraph_eq_zero_or_gap_le: the dichotomy.
• Cslib.PCP.Dinur.exists_card_gapGraph_le: the size is polynomial in the number of clauses.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1

noncomputable def Cslib.PCP.Dinur.round (G : FinConstraintGraph Alphabet) : FinConstraintGraph Alphabet

Dinur's round on a finite constraint graph over the fixed alphabet Σ₀: amplify walkLength killRate, with the vertices and edges it builds from the edges of its input.

theorem Cslib.PCP.Dinur.satisfiable_round_iff (G : FinConstraintGraph Alphabet) : (round G).graph.Satisfiable ↔ G.graph.Satisfiable

Dinur's round preserves satisfiability.

theorem Cslib.PCP.Dinur.min_le_unsatVal_round (G : FinConstraintGraph Alphabet) : min (2 * G.graph.unsatVal) gap ≤ (round G).graph.unsatVal

Dinur's main theorem Dinur, Theorem 4.1: Dinur's round doubles the value up to the threshold gap.

theorem Cslib.PCP.Dinur.card_vertices_round (G : FinConstraintGraph Alphabet) : Fintype.card (round G).V = vertexFactor * Fintype.card G.E

Dinur's round has vertexFactor vertices per edge of its input.

theorem Cslib.PCP.Dinur.card_edges_round (G : FinConstraintGraph Alphabet) : Fintype.card (round G).E = edgeFactor * Fintype.card G.E

Dinur's round has edgeFactor edges per edge of its input.

noncomputable def Cslib.PCP.Dinur.amplifier : Amplifier Alphabet

Dinur's amplifier Dinur, Theorem 4.1: Dinur's round on finite constraint graphs over the fixed alphabet Σ₀, which doubles the value up to the threshold gap and multiplies the numbers of vertices and edges by at most vertexFactor + edgeFactor.

@[simp]

theorem Cslib.PCP.Dinur.gap_amplifier : amplifier.gap = gap

The threshold of Dinur's amplifier is gap.

@[simp]

theorem Cslib.PCP.Dinur.factor_amplifier : amplifier.factor = vertexFactor + edgeFactor

The size factor of Dinur's amplifier is vertexFactor + edgeFactor.

The gap graph of a formula

noncomputable def Cslib.PCP.Dinur.cnfGraph {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) : FinConstraintGraph Alphabet

The constraint graph of a formula φ over the fixed alphabet Σ₀: its constraint graph ofCNF φ, preprocessed, then composed. Preprocessing replaces the vertices by the half-edges, so that the variables of φ disappear, and composition brings the alphabet to Σ₀.

theorem Cslib.PCP.Dinur.satisfiable_cnfGraph_iff {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) (h3 : ∀ κ ∈ φ, List.length κ ≤ 3) : (cnfGraph φ).graph.Satisfiable ↔ φ.Satisfiable

If the clauses of φ have at most three literals, its constraint graph over Σ₀ is satisfiable exactly when φ is.

theorem Cslib.PCP.Dinur.card_edges_cnfGraph {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) : Fintype.card (cnfGraph φ).E = 43560 * 2 ^ 1403 * List.length φ

The constraint graph over Σ₀ of a formula with m clauses has 43560 · 2 ^ 1403 · m edges.

theorem Cslib.PCP.Dinur.card_vertices_cnfGraph {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) : Fintype.card (cnfGraph φ).V = (1536 + 1452 * (2 ^ 16 + 2 ^ 256 + 5 * 2 ^ 1403)) * List.length φ

The constraint graph over Σ₀ of a formula with m clauses has (1536 + 1452 (2 ^ 16 + 2 ^ 256 + 5 * 2 ^ 1403)) m vertices.

noncomputable def Cslib.PCP.Dinur.gapGraph {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) : FinConstraintGraph Alphabet

The gap graph of a formula φ Dinur, Corollary 4.2: ⌈log₂ |E|⌉ rounds of Dinur's amplifier on the constraint graph of φ over Σ₀, which has |E| edges.

theorem Cslib.PCP.Dinur.satisfiable_gapGraph_iff {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) (h3 : ∀ κ ∈ φ, List.length κ ≤ 3) : (gapGraph φ).graph.Satisfiable ↔ φ.Satisfiable

Completeness and soundness of the gap graph: if the clauses of φ have at most three literals, its gap graph is satisfiable exactly when φ is.

theorem Cslib.PCP.Dinur.gap_le_unsatVal_gapGraph {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) (h3 : ∀ κ ∈ φ, List.length κ ≤ 3) (h : ¬φ.Satisfiable) : gap ≤ (gapGraph φ).graph.unsatVal

Dinur's gap theorem Dinur, Corollary 4.2: if the clauses of φ have at most three literals and φ is unsatisfiable, the value of its gap graph is at least the universal constant gap.

theorem Cslib.PCP.Dinur.unsatVal_gapGraph_eq_zero_or_gap_le {V : Type u} [DecidableEq V] (φ : Logic.PL.CNF V) : (gapGraph φ).graph.unsatVal = 0 ∨ gap ≤ (gapGraph φ).graph.unsatVal

The dichotomy Dinur, Corollary 4.2: the value of the gap graph of a formula is either zero or at least the universal constant gap.

theorem Cslib.PCP.Dinur.exists_card_gapGraph_le : ∃ (C : ℕ) (c : ℕ), ∀ {V : Type u} [inst : DecidableEq V] (φ : Logic.PL.CNF V), Fintype.card (gapGraph φ).V ≤ C * List.length φ ^ c ∧ Fintype.card (gapGraph φ).E ≤ C * List.length φ ^ c

The gap graph is polynomial Dinur, Corollary 4.2: its numbers of vertices and edges are at most C m ^ c for a formula with m clauses, for universal constants C and c.