Constraint graphs and their unsatisfiability value

The combinatorial core of Dinur's proof of the PCP theorem. A constraint graph over an alphabet α is a finite multigraph whose edges each carry a binary constraint on the labels of their endpoints; an assignment labels the vertices, and the unsatisfiability value unsatVal is the least fraction of edges any assignment leaves unsatisfied.

Dinur's amplification step is a transformation of constraint graphs that preserves satisfiability (unsatVal = 0) while doubling unsatVal otherwise, so all of that argument is phrased in terms of the definitions here.

Design

• Vertices are Fin numVerts and edges are indexed by Fin numEdges, so parallel edges and self-loops are allowed. Both are essential: powering a constraint graph produces many parallel walk-edges, and the degree-reduction and expanderization steps add edges to a graph that may already have them.
• Edges are directed (tail/head) and constraints are Bool-valued functions of the two endpoint labels, which keeps everything decidable and computable. Undirected graphs are modelled by including both orientations, which the analysis of random walks will require explicitly rather than implicitly.
• unsatFrac divides by numEdges, so an edgeless graph gets value 0 by Lean's x / 0 = 0 convention. Every lemma below is stated so that this is the mathematically correct answer.

Main definitions

• ConstraintGraph, ConstraintGraph.Assignment, ConstraintGraph.Satisfies
• ConstraintGraph.unsatFrac — the fraction of edges an assignment fails
• ConstraintGraph.unsatVal — the minimum of unsatFrac over all assignments
• ConstraintGraph.Satisfiable

Main results

• unsatFrac_eq_zero_iff — an assignment wastes no edges exactly when it satisfies them all
• exists_assignment_unsatFrac_eq_unsatVal — the minimum is attained
• unsatVal_eq_zero_iff_satisfiable — the gap-0 case is satisfiability
• unsatVal_nonneg, unsatVal_le_one

structure Complexity.ConstraintGraph (α : Type) : Type

A constraint graph over the alphabet α: a finite multigraph on the vertices Fin numVerts, with edges indexed by Fin numEdges, each edge carrying a binary constraint on the labels of its endpoints.

• numVerts : ℕ

  The number of vertices; the vertices are Fin numVerts.

• numEdges : ℕ

  The number of edges; the edges are indexed by Fin numEdges, so parallel edges and self-loops are allowed.

• tail : Fin self.numEdges → Fin self.numVerts

  The source of an edge.

• head : Fin self.numEdges → Fin self.numVerts

  The target of an edge.

• rel : Fin self.numEdges → α → α → Bool

  The constraint carried by an edge, as a predicate on the labels of its tail and its head, in that order.

@[reducible, inline]

abbrev Complexity.ConstraintGraph.Assignment {α : Type} (G : ConstraintGraph α) : Type

An assignment labels every vertex with a symbol of the alphabet.

Equations

• G.Assignment = (Fin G.numVerts → α)

def Complexity.ConstraintGraph.satisfies {α : Type} (G : ConstraintGraph α) (a : G.Assignment) (e : Fin G.numEdges) : Bool

Whether the assignment a satisfies the edge e, as a Bool.

Equations

• G.satisfies a e = G.rel e (a (G.tail e)) (a (G.head e))

def Complexity.ConstraintGraph.Satisfies {α : Type} (G : ConstraintGraph α) (a : G.Assignment) (e : Fin G.numEdges) : Prop

The assignment a satisfies the edge e.

Equations

• G.Satisfies a e = (G.satisfies a e = true)

@[instance_reducible]

instance Complexity.ConstraintGraph.instDecidableSatisfies {α : Type} (G : ConstraintGraph α) (a : G.Assignment) (e : Fin G.numEdges) : Decidable (G.Satisfies a e)

Equations

• G.instDecidableSatisfies a e = Complexity.ConstraintGraph.instDecidableSatisfies._aux_1 G a e

theorem Complexity.ConstraintGraph.satisfies_iff {α : Type} {G : ConstraintGraph α} {a : G.Assignment} {e : Fin G.numEdges} : G.Satisfies a e ↔ G.rel e (a (G.tail e)) (a (G.head e)) = true

def Complexity.ConstraintGraph.unsatEdges {α : Type} (G : ConstraintGraph α) (a : G.Assignment) : Finset (Fin G.numEdges)

The edges left unsatisfied by a.

Equations

• G.unsatEdges a = {e : Fin G.numEdges | ¬G.Satisfies a e}

@[simp]

theorem Complexity.ConstraintGraph.mem_unsatEdges {α : Type} {G : ConstraintGraph α} {a : G.Assignment} {e : Fin G.numEdges} : e ∈ G.unsatEdges a ↔ ¬G.Satisfies a e

def Complexity.ConstraintGraph.unsatFrac {α : Type} (G : ConstraintGraph α) (a : G.Assignment) : ℚ

The fraction of edges that a leaves unsatisfied. An edgeless graph has value 0.

Equations

• G.unsatFrac a = ↑(G.unsatEdges a).card / ↑G.numEdges

theorem Complexity.ConstraintGraph.unsatFrac_nonneg {α : Type} {G : ConstraintGraph α} (a : G.Assignment) : 0 ≤ G.unsatFrac a

theorem Complexity.ConstraintGraph.card_unsatEdges_le {α : Type} {G : ConstraintGraph α} (a : G.Assignment) : (G.unsatEdges a).card ≤ G.numEdges

theorem Complexity.ConstraintGraph.unsatFrac_le_one {α : Type} {G : ConstraintGraph α} (a : G.Assignment) : G.unsatFrac a ≤ 1

theorem Complexity.ConstraintGraph.unsatFrac_eq_zero_iff {α : Type} {G : ConstraintGraph α} {a : G.Assignment} : G.unsatFrac a = 0 ↔ ∀ (e : Fin G.numEdges), G.Satisfies a e

An assignment wastes no edges exactly when it satisfies every edge. This holds for the edgeless graph too, where both sides are trivially true.

def Complexity.ConstraintGraph.Satisfiable {α : Type} (G : ConstraintGraph α) : Prop

A constraint graph is satisfiable when some assignment satisfies every edge.

Equations

• G.Satisfiable = ∃ (a : G.Assignment), ∀ (e : Fin G.numEdges), G.Satisfies a e

noncomputable def Complexity.ConstraintGraph.unsatVal {α : Type} [Fintype α] [Nonempty α] (G : ConstraintGraph α) : ℚ

The unsatisfiability value: the least fraction of edges any assignment leaves unsatisfied.

Equations

• G.unsatVal = Finset.univ.inf' ⋯ G.unsatFrac

theorem Complexity.ConstraintGraph.unsatVal_le {α : Type} {G : ConstraintGraph α} [Fintype α] [Nonempty α] (a : G.Assignment) : G.unsatVal ≤ G.unsatFrac a

theorem Complexity.ConstraintGraph.le_unsatVal {α : Type} {G : ConstraintGraph α} [Fintype α] [Nonempty α] {c : ℚ} (h : ∀ (a : G.Assignment), c ≤ G.unsatFrac a) : c ≤ G.unsatVal

theorem Complexity.ConstraintGraph.exists_assignment_unsatFrac_eq_unsatVal {α : Type} [Fintype α] [Nonempty α] (G : ConstraintGraph α) : ∃ (a : G.Assignment), G.unsatFrac a = G.unsatVal

The minimum defining unsatVal is attained.

theorem Complexity.ConstraintGraph.unsatVal_nonneg {α : Type} [Fintype α] [Nonempty α] (G : ConstraintGraph α) : 0 ≤ G.unsatVal

theorem Complexity.ConstraintGraph.unsatVal_le_one {α : Type} [Fintype α] [Nonempty α] (G : ConstraintGraph α) : G.unsatVal ≤ 1

theorem Complexity.ConstraintGraph.unsatVal_eq_zero_iff_satisfiable {α : Type} [Fintype α] [Nonempty α] (G : ConstraintGraph α) : G.unsatVal = 0 ↔ G.Satisfiable

The zero-gap case is exactly satisfiability.

theorem Complexity.ConstraintGraph.numEdges_pos_of_not_satisfiable {α : Type} {G : ConstraintGraph α} [Nonempty α] (h : ¬G.Satisfiable) : 0 < G.numEdges

An unsatisfiable graph has an edge, since otherwise any labelling works.

theorem Complexity.ConstraintGraph.inv_numEdges_le_unsatFrac {α : Type} {G : ConstraintGraph α} [Nonempty α] (h : ¬G.Satisfiable) (a : G.Assignment) : 1 / ↑G.numEdges ≤ G.unsatFrac a

On an unsatisfiable graph every assignment fails at least one edge, so its value is at least one edge's worth.

theorem Complexity.ConstraintGraph.inv_numEdges_le_unsatVal {α : Type} {G : ConstraintGraph α} [Fintype α] [Nonempty α] (h : ¬G.Satisfiable) : 1 / ↑G.numEdges ≤ G.unsatVal

theorem Complexity.ConstraintGraph.unsatVal_pos_of_not_satisfiable {α : Type} {G : ConstraintGraph α} [Fintype α] [Nonempty α] (h : ¬G.Satisfiable) : 0 < G.unsatVal

theorem Complexity.ConstraintGraph.not_satisfiable_of_unsatVal_pos {α : Type} [Fintype α] [Nonempty α] {G : ConstraintGraph α} (h : 0 < G.unsatVal) : ¬G.Satisfiable

A positive value certifies unsatisfiability.