Graph homomorphism

AbbreviationGraph-homomorphism instances#✓fully proved

A graph-homomorphism instance is a quadruple \((n, E, m, F)\) where \(n\) is a natural number (the number of source vertices), \(E\) is a list of pairs of natural numbers (the source edges), \(m\) is a natural number (the number of target vertices) and \(F\) is a list of pairs of natural numbers (the target edges).

abbrev GraphHomomorphismInstance := ℕ × List (ℕ × ℕ) × ℕ × List (ℕ × ℕ)

Used by 4

Used byGRAPH HOMOMORPHISM as a decision problem · Feasible graph-homomorphism instances · Target graph of a graph-homomorphism instance · Well-formed graph-homomorphism instances

DefinitionTarget graph of a graph-homomorphism instance#✓fully proved

The target graph of a graph-homomorphism instance \((n, E, m, F)\) is the simple graph on \(\{0, \dots, m - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(F\). Pairs of \(F\) with an endpoint at least \(m\) contribute no edge.

def GraphTarget (i : GraphHomomorphismInstance) : SimpleGraph (Fin i.2.2.1) :=
  Cslib.Complexity.Karp.edgeGraph i.2.2.1 i.2.2.2

Uses 2 · Used by 1

Statement usesGraph of an edge list · Graph-homomorphism instances

Used byFeasible graph-homomorphism instances

DefinitionWell-formed graph-homomorphism instances#✓fully proved

A graph-homomorphism instance \((n, E, m, F)\) is well formed when \(E\) has no repeated entries, every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\), \(F\) has no repeated entries, and every pair \((u, v)\) in \(F\) satisfies \(u < m\), \(v < m\), \(u \ne v\) and \((v, u) \notin F\).

def WellFormed (i : GraphHomomorphismInstance) : Prop :=
  i.2.1.Nodup ∧ (∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.1) ∧
    i.2.2.2.Nodup ∧ ∀ e ∈ i.2.2.2, e.1 < i.2.2.1 ∧ e.2 < i.2.2.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.2.2

Uses 1 · Used by 1

Statement usesGraph-homomorphism instances

Used byGRAPH HOMOMORPHISM as a decision problem

DefinitionFeasible graph-homomorphism instances#✓fully proved

A graph-homomorphism instance \((n, E, m, F)\) is feasible when there is a map \(f : \{0, \dots, n - 1\} \to \{0, \dots, m - 1\}\) such that, for every pair \((u, v)\) in \(E\) with \(u < n\) and \(v < n\), the vertices \(f(u)\) and \(f(v)\) are adjacent in the target graph of the instance, that is, \(f(u) \ne f(v)\) and \((f(u), f(v))\) or \((f(v), f(u))\) belongs to \(F\). Pairs of \(E\) with an endpoint at least \(n\) impose no condition.

def GraphHomomorphismFeasible
    (i : GraphHomomorphismInstance) : Prop :=
  ∃ f : Fin i.1 → Fin i.2.2.1,
    ∀ e ∈ i.2.1, ∀ (h1 : e.1 < i.1) (h2 : e.2 < i.1),
      (GraphTarget i).Adj (f ⟨e.1, h1⟩) (f ⟨e.2, h2⟩)

Uses 2 · Used by 1

Statement usesGraph-homomorphism instances · Target graph of a graph-homomorphism instance

Used byGRAPH HOMOMORPHISM as a decision problem

DefinitionGRAPH HOMOMORPHISM as a decision problem#✓fully proved

The decision problem GRAPH HOMOMORPHISM accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a graph-homomorphism instance \((n, E, m, F)\) that is well formed (neither \(E\) nor \(F\) has repeated entries, every pair \((u, v)\) in \(E\) has \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\), and every pair \((u, v)\) in \(F\) has \(u < m\), \(v < m\), \(u \ne v\) and \((v, u) \notin F\)) and for which there is a map \(f : \{0, \dots, n - 1\} \to \{0, \dots, m - 1\}\) such that, for every pair \((u, v)\) in \(E\), \(f(u) \ne f(v)\) and \((f(u), f(v))\) or \((f(v), f(u))\) belongs to \(F\). Bitstrings that do not decode are rejected.

noncomputable def graphHomomorphismDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := GraphHomomorphismInstance) x with
  | some i => decide (WellFormed i ∧ GraphHomomorphismFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible graph-homomorphism instances · Graph-homomorphism instances · Well-formed graph-homomorphism instances · Decision problems

Used byGRAPH HOMOMORPHISM is NP-complete

TheoremGRAPH HOMOMORPHISM is NP-complete#●ready to prove

The decision problem GRAPH HOMOMORPHISM belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

public theorem_wanted graphHomomorphism_npComplete :
    graphHomomorphismDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L graphHomomorphismDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), GRAPH HOMOMORPHISM; P. Hell and J. Nesetril, "On the complexity of H-coloring" (1990).

Uses 5

Statement usesPolynomial-time many-one reduction · GRAPH HOMOMORPHISM as a decision problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.