Enlarging the alphabet of a constraint graph

Dinur's round is an endomorphism of constraint graphs over one fixed alphabet — the one its composition step produces — while the reduction from 3-SAT lands in an alphabet of its own. This module bridges the two: an injection of alphabets carries a constraint graph to a graph over the larger alphabet, keeping the same vertices and edges, and preserving satisfiability in both directions.

An edge of the lifted graph accepts a pair of symbols exactly when both are images and the originals satisfied the original edge. So an assignment using a symbol outside the image fails every edge at that vertex, and a satisfying assignment of the lift can be pulled back.

Main definitions

• Complexity.ConstraintGraph.lift — the graph over the larger alphabet

Main results

• Complexity.ConstraintGraph.satisfiable_lift_iff — satisfiability is preserved

def Complexity.ConstraintGraph.lift {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) (f : α → β) : ConstraintGraph β

The same graph, read over a larger alphabet along f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.ConstraintGraph.rel_lift {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) (f : α → β) (e : Fin (G.lift f).numEdges) (b₁ b₂ : β) : (G.lift f).rel e b₁ b₂ = decide (∃ (a₁ : α) (a₂ : α), f a₁ = b₁ ∧ f a₂ = b₂ ∧ G.rel e a₁ a₂ = true)

@[simp]

theorem Complexity.ConstraintGraph.tail_lift {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) (f : α → β) (e : Fin (G.lift f).numEdges) : (G.lift f).tail e = G.tail e

@[simp]

theorem Complexity.ConstraintGraph.head_lift {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) (f : α → β) (e : Fin (G.lift f).numEdges) : (G.lift f).head e = G.head e

@[simp]

theorem Complexity.ConstraintGraph.numEdges_lift {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) (f : α → β) : (G.lift f).numEdges = G.numEdges

@[simp]

theorem Complexity.ConstraintGraph.numVerts_lift {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) (f : α → β) : (G.lift f).numVerts = G.numVerts

theorem Complexity.ConstraintGraph.satisfies_lift_iff {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) (f : α → β) (b : (G.lift f).Assignment) (e : Fin (G.lift f).numEdges) : (G.lift f).Satisfies b e ↔ ∃ (a₁ : α) (a₂ : α), f a₁ = b (G.tail e) ∧ f a₂ = b (G.head e) ∧ G.rel e a₁ a₂ = true

theorem Complexity.ConstraintGraph.satisfiable_lift_iff {α β : Type} [Fintype α] [DecidableEq β] (G : ConstraintGraph α) {f : α → β} (hf : Function.Injective f) [Nonempty α] : (G.lift f).Satisfiable ↔ G.Satisfiable

Satisfiability is unchanged.