Degree reduction

The first step of Dinur's preprocessing Dinur, Section 3.1: an arbitrary constraint graph, whose vertices may have wildly different degrees, is replaced by a regular one over the same alphabet, losing at most a constant factor of its value. This is the expander replacement of Papadimitriou and Yannakakis: every vertex is split into one copy per edge end at it, and the copies of a vertex are joined by an expander carrying equality constraints.

The vertices of the new constraint graph G.degreeReduce H are the half-edges (e, b) of G: an edge e with one of its ends, the first one for b = false and the second one for b = true. There are 2 |E| of them, whatever the degrees of G. Each half-edge has

• one edge-link, labelled inl (), to the other half of its edge, carrying the constraint of that edge, and
• |D| cloud-links, labelled inr i, given by a regular multigraph H v on the cloud of half-edges at the same vertex v, carrying equality constraints.

So G.degreeReduce H is (1 + |D|)-regular. A labelling satisfying G labels every half-edge by the label of its vertex and satisfies the new constraint graph (satisfiable_degreeReduce). In the other direction, from a labelling A of the half-edges, label every vertex v by a most frequent label σ v of its cloud. A half-edge disagreeing with the label of its vertex is charged to the cloud-links joining differently labelled half-edges of its cloud, which all violate their equality constraints. When H v is an expander there are many of them: at least (1 - μ) |D| per disagreeing half-edge, since the half-edges with any label a are at most as many as those with the label σ v, so that many edges leave them (Cslib.RotationMap.mul_card_filter_ne_le_card_filter_ne_neighbor). An edge violated by σ either has a disagreeing half-edge, or its edge-links are violated by A. Trading the two charges off shows that the proportion of darts violated by A is at least min 1 ((1 - μ) |D|) / (2 (1 + |D|)) times the value of G, when the spectral expansion of every H v is at most μ (le_unsatVal_degreeReduce). The constant does not depend on the alphabet, as in Dinur's analysis.

Main definitions

• Cslib.PCP.ConstraintGraph.endpoint, Cslib.PCP.ConstraintGraph.Cloud: the vertex of a half-edge, and the half-edges at a vertex.
• Cslib.PCP.ConstraintGraph.cloudGraph: the regular multigraph on the half-edges joining each cloud by a given multigraph.
• Cslib.PCP.ConstraintGraph.degreeReduce: the degree-reduced regular constraint graph.

Main results

• Cslib.PCP.ConstraintGraph.satisfiable_degreeReduce: completeness.
• Cslib.PCP.ConstraintGraph.one_add_card_mul_unsatVal_degreeReduce_le: degree reduction divides the value by at least 1 + |D|.
• Cslib.PCP.ConstraintGraph.le_unsatVal_degreeReduce: soundness.
• Cslib.PCP.ConstraintGraph.satisfiable_degreeReduce_iff: with expanders on the clouds, degree reduction preserves satisfiability.

References

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

Half-edges and clouds

def Cslib.PCP.ConstraintGraph.endpoint {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) : E × Bool → V

The vertex of a half-edge (e, b): the first end of e for b = false, the second one for b = true.

@[simp]

theorem Cslib.PCP.ConstraintGraph.endpoint_false {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) (e : E) : G.endpoint (e, false) = G.src e

The vertex of the first half of an edge is its first end.

@[simp]

theorem Cslib.PCP.ConstraintGraph.endpoint_true {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) (e : E) : G.endpoint (e, true) = G.dst e

The vertex of the second half of an edge is its second end.

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.Cloud {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) (v : V) : Type u_2

The cloud of a vertex: the half-edges at it.

def Cslib.PCP.ConstraintGraph.cloudGraph {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : (v : V) → RotationMap (G.Cloud v) D) : RotationMap (E × Bool) D

The regular multigraph on the half-edges whose edges join, within the cloud of every vertex v, the half-edges as H v does.

@[simp]

theorem Cslib.PCP.ConstraintGraph.endpoint_neighbor_cloudGraph {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} (H : (v : V) → RotationMap (G.Cloud v) D) (p : E × Bool) (i : D) : G.endpoint ((G.cloudGraph H).neighbor p i) = G.endpoint p

The neighbors of a half-edge in the cloud graph are in its cloud.

The degree-reduced constraint graph

def Cslib.PCP.ConstraintGraph.halfEdgeGraph {E : Type u_2} : RotationMap (E × Bool) Unit

The 1-regular multigraph joining the two halves of every edge.

@[simp]

theorem Cslib.PCP.ConstraintGraph.neighbor_halfEdgeGraph {E : Type u_2} (e : E) (b : Bool) (i : Unit) : halfEdgeGraph.neighbor (e, b) i = (e, !b)

The other half of the half-edge (e, b) is (e, !b).

def Cslib.PCP.ConstraintGraph.degreeReduce {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : (v : V) → RotationMap (G.Cloud v) D) : RegularConstraintGraph (E × Bool) (Unit ⊕ D) α

The degree-reduced constraint graph Dinur, Section 3.1: its vertices are the half-edges of G; the edge-link inl () joins the two halves of an edge e and carries the constraint of e, read from its first end to its second one; the cloud-links inr i join the half-edges of every cloud as H does and carry equality constraints.

@[simp]

theorem Cslib.PCP.ConstraintGraph.graph_degreeReduce {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} (H : (v : V) → RotationMap (G.Cloud v) D) : (G.degreeReduce H).graph = halfEdgeGraph.union (G.cloudGraph H)

The underlying multigraph of the degree-reduced constraint graph: the edge-links followed by the cloud-links.

theorem Cslib.PCP.ConstraintGraph.satisfiable_degreeReduce {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} (H : (v : V) → RotationMap (G.Cloud v) D) (h : G.Satisfiable) : (G.degreeReduce H).toConstraintGraph.Satisfiable

Completeness of degree reduction: labelling every half-edge by the label of its vertex turns a labelling satisfying G into one satisfying G.degreeReduce H.

theorem Cslib.PCP.ConstraintGraph.one_add_card_mul_unsatVal_degreeReduce_le {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} (H : (v : V) → RotationMap (G.Cloud v) D) [Fintype E] [Fintype D] [Nonempty α] : (1 + ↑(Fintype.card D)) * (G.degreeReduce H).toConstraintGraph.unsatVal ≤ G.unsatVal

Degree reduction divides the value by at least 1 + |D| Dinur, Section 3.1: labelling the half-edges by the labels of their vertices violates the edge-links of the violated edges only, which are a proportion 1 / (1 + |D|) of the darts at their half-edges.

Soundness

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_degreeReduce {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} (H : (v : V) → RotationMap (G.Cloud v) D) [Fintype E] [DecidableEq V] [Fintype D] {μ : ℝ} [Nonempty α] (hH : ∀ (v : V), (H v).spectralExpansion ≤ μ) : min 1 ((1 - μ) * ↑(Fintype.card D)) / (2 * (1 + ↑(Fintype.card D))) * G.unsatVal ≤ (G.degreeReduce H).toConstraintGraph.unsatVal

Soundness of degree reduction Dinur, Section 3.1: if the multigraphs on the clouds have spectral expansion at most μ, degree reduction divides the value by at most 2 (1 + |D|) / min 1 ((1 - μ) |D|), whatever the alphabet.

theorem Cslib.PCP.ConstraintGraph.satisfiable_degreeReduce_iff {V : Type u_1} {E : Type u_2} {D : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} (H : (v : V) → RotationMap (G.Cloud v) D) [Fintype E] [DecidableEq V] [Fintype D] [Nonempty D] [Nonempty α] {μ : ℝ} (hμ : μ < 1) (hH : ∀ (v : V), (H v).spectralExpansion ≤ μ) : (G.degreeReduce H).toConstraintGraph.Satisfiable ↔ G.Satisfiable

Degree reduction preserves satisfiability when the multigraphs on the clouds are expanders: their degree is positive and their spectral expansions are at most some μ < 1.