Label Cover and the Unique Games Conjecture

Both problems are binary constraint satisfaction problems on executable constraint graphs (Cslib.PCP.Encoded.Graph), whose edges carry the table of a function.

• Label Cover Arora and Barak, Chapter 22: a bipartite graph whose edges go from a left vertex, labelled in β, to a right vertex, labelled in γ, each carrying a projection π : β → γ. An edge is satisfied when π maps the label of its left end to the label of its right end. Left and right vertices are numbered separately: each number carries a pair of labels, of which a left end reads the first and a right end the second (satisfies_toGraph_projectionEval_iff), so a labelling of the numbers is exactly a labelling of the left vertices together with one of the right vertices.
• Unique Games [Kho02]: a constraint graph, not necessarily bipartite, whose edges carry bijections π : α → α; an edge from u to v is satisfied when π maps the label of u to the label of v. Instances with a non-bijective table are outside the promise.

The value of an instance is the largest proportion of its edges that a labelling satisfies, and GapLabelCover β γ c s and GapUniqueGames α c s are the gap problems separating value at least c from value at most s.

The Unique Games Conjecture [Kho02] says that for all ε, δ > 0 there is a number L of labels for which GapUniqueGames (Fin L) (1 - ε) δ is NP-hard. It is stated here as the proposition UniqueGamesConjecture, for the parameters with δ < 1 - ε: for the others the two thresholds do not separate the instances, and GapUniqueGames has no no-instances. The library states the conjecture and does not prove it.

Main definitions

• Cslib.Complexity.projectionEval, Cslib.Complexity.GapLabelCover: Label Cover.
• Cslib.Complexity.permutationEval, Cslib.Complexity.IsUniqueGame, Cslib.Complexity.GapUniqueGames: Unique Games.
• Cslib.Complexity.UniqueGamesConjecture: the conjecture, as a proposition.

Main results

• Cslib.Complexity.satisfies_toGraph_projectionEval_iff, Cslib.Complexity.satisfiable_toGraph_projectionEval_iff: a labelling of a Label Cover instance is a labelling of its left vertices together with one of its right vertices.
• Cslib.Complexity.UniqueGamesConjecture.npHard_of_le: the conjecture yields NP-hardness for every weaker gap.

References

• S. Khot, On the power of unique 2-prover 1-round games
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 22

Label Cover

def Cslib.Complexity.projectionEval {β γ : Type} [DecidableEq γ] (π : β → γ) (x y : β × γ) : Bool

The projection constraint π on the pairs of labels x of the left end and y of the right end of an edge: it holds when π x.1 = y.2.

theorem Cslib.Complexity.satisfies_toGraph_projectionEval_iff {β γ : Type} [DecidableEq γ] (g : PCP.Encoded.Graph (β → γ)) (σ : ℕ → β × γ) (i : Fin g.edges.length) : (g.toGraph projectionEval).Satisfies σ i ↔ (g.edges.get i).constraint (σ (g.edges.get i).src).1 = (σ (g.edges.get i).dst).2

A labelling satisfies an edge of a Label Cover instance when the projection maps the first label of its left end to the second label of its right end.

theorem Cslib.Complexity.satisfiable_toGraph_projectionEval_iff {β γ : Type} [DecidableEq γ] (g : PCP.Encoded.Graph (β → γ)) : (g.toGraph projectionEval).Satisfiable ↔ ∃ (ℓ : ℕ → β) (r : ℕ → γ), ∀ d ∈ g.edges, d.constraint (ℓ d.src) = r d.dst

A Label Cover instance is satisfiable exactly when some labelling ℓ of its left vertices and r of its right vertices satisfies every projection.

noncomputable def Cslib.Complexity.GapLabelCover (β γ : Type) [DecidableEq γ] (c s : ℝ) : PromiseProblem (PCP.Encoded.Graph (β → γ))

The gap problem of Label Cover with left labels β and right labels γ, completeness c and soundness s. Each edge goes from a left vertex src to a right vertex dst and carries the table of a projection β → γ. The value of an instance is the largest proportion of the edges that labellings of the left and the right vertices satisfy. The yes-instances have value at least c, the no-instances value at most s.

Unique Games

def Cslib.Complexity.permutationEval {α : Type} [DecidableEq α] (π : α → α) (a b : α) : Bool

The constraint of a function π on the labels a of the first end and b of the second end of an edge: it holds when π a = b.

def Cslib.Complexity.IsUniqueGame {α : Type} (g : PCP.Encoded.Graph (α → α)) : Prop

A unique game: the table on every edge is a bijection.

noncomputable def Cslib.Complexity.GapUniqueGames (α : Type) [DecidableEq α] (c s : ℝ) : PromiseProblem (PCP.Encoded.Graph (α → α))

The gap problem of Unique Games with labels α, completeness c and soundness s. The instances are unique games: constraint graphs whose edges carry bijections π : α → α, an edge from u to v being satisfied when π maps the label of u to that of v. The value of an instance is the largest proportion of the edges that a labelling satisfies. The yes-instances have value at least c, the no-instances value at most s.

theorem Cslib.Complexity.GapUniqueGames_mono {α : Type} [DecidableEq α] {c c' s s' : ℝ} (hc : c' ≤ c) (hs : s ≤ s') (hsc : s' < c') : (GapUniqueGames α c s).yes ⊆ (GapUniqueGames α c' s').yes ∧ (GapUniqueGames α c s).no ⊆ (GapUniqueGames α c' s').no

Weakening the gap of GapUniqueGames enlarges its promise.

def Cslib.Complexity.UniqueGamesConjecture : Prop

The Unique Games Conjecture [Kho02]: for all ε, δ > 0 with δ < 1 - ε, there is a number L of labels such that distinguishing unique games on the labels Fin L of value at least 1 - ε from those of value at most δ is NP-hard. Instances are encoded by their vertex counts and edge lists, with constraint tables listing ranks of labels. The constraint graphs need not be bipartite. This is a conjecture, stated and not assumed.

theorem Cslib.Complexity.UniqueGamesConjecture.npHard_of_le (h : UniqueGamesConjecture) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (hεδ : δ < 1 - ε) : ∃ (L : ℕ), ∀ (c s : ℝ), c ≤ 1 - ε → δ ≤ s → s < c → PromiseProblem.NPHard (PCP.Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encFinEnum (Fin L)))) (GapUniqueGames (Fin L) c s)

Under the Unique Games Conjecture, for every ε, δ > 0 with δ < 1 - ε there is a number L of labels such that every weaker gap problem on Fin L, with completeness at most 1 - ε and soundness at least δ, is NP-hard.