Subgraph isomorphism

AbbreviationSubgraph-isomorphism instances#✓fully proved

A subgraph-isomorphism instance is a tuple \((n, E_G, m, E_H)\) of a natural number \(n\) (the number of host vertices), a list \(E_G\) of pairs of natural numbers (the host edges), a natural number \(m\) (the number of pattern vertices) and a list \(E_H\) of pairs of natural numbers (the pattern edges).

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

Used by 4

Used byHost graph of a subgraph-isomorphism instance · SUBGRAPH ISOMORPHISM as a decision problem · Feasible subgraph-isomorphism instances · Well-formed subgraph-isomorphism instances

DefinitionHost graph of a subgraph-isomorphism instance#✓fully proved

For a subgraph-isomorphism instance \((n, E_G, m, E_H)\), the host graph is the graph of the edge list \(E_G\) on \(n\) vertices: the simple graph on \(\{0, \dots, n - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E_G\).

def GraphHost (i : SubgraphIsomorphismInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2.1

Uses 2 · Used by 1

Statement usesGraph of an edge list · Subgraph-isomorphism instances

Used byFeasible subgraph-isomorphism instances

DefinitionWell-formed subgraph-isomorphism instances#✓fully proved

A subgraph-isomorphism instance \((n, E_G, m, E_H)\) is well formed when the list \(E_G\) has no repeated entries and every \((u, v) \in E_G\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E_G\), and likewise the list \(E_H\) has no repeated entries and every \((u, v) \in E_H\) satisfies \(u < m\), \(v < m\), \(u \ne v\) and \((v, u) \notin E_H\).

def WellFormed (i : SubgraphIsomorphismInstance) : 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 usesSubgraph-isomorphism instances

Used bySUBGRAPH ISOMORPHISM as a decision problem

DefinitionFeasible subgraph-isomorphism instances#✓fully proved

A subgraph-isomorphism instance \((n, E_G, m, E_H)\) is feasible when there is an injective map \(f : \{0, \dots, m - 1\} \to \{0, \dots, n - 1\}\) such that for every \((u, v) \in E_H\) with \(u < m\) and \(v < m\), the vertices \(f(u)\) and \(f(v)\) are adjacent in the host graph of the instance.

def SubgraphIsomorphismFeasible
    (i : SubgraphIsomorphismInstance) : Prop :=
  ∃ f : Fin i.2.2.1 → Fin i.1, Function.Injective f ∧
    ∀ e ∈ i.2.2.2, ∀ (h1 : e.1 < i.2.2.1) (h2 : e.2 < i.2.2.1),
      (GraphHost i).Adj (f ⟨e.1, h1⟩) (f ⟨e.2, h2⟩)

Uses 2 · Used by 1

Statement usesHost graph of a subgraph-isomorphism instance · Subgraph-isomorphism instances

Used bySUBGRAPH ISOMORPHISM as a decision problem

DefinitionSUBGRAPH ISOMORPHISM as a decision problem#✓fully proved

The decision problem SUBGRAPH ISOMORPHISM accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of subgraph-isomorphism instances, to an instance that is well formed and feasible. Bitstrings that do not decode to an instance are rejected.

noncomputable def subgraphIsomorphismDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := SubgraphIsomorphismInstance) x with
  | some i => decide (WellFormed i ∧ SubgraphIsomorphismFeasible 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 subgraph-isomorphism instances · Subgraph-isomorphism instances · Well-formed subgraph-isomorphism instances · Decision problems

Used bySUBGRAPH ISOMORPHISM is NP-complete

TheoremSUBGRAPH ISOMORPHISM is NP-complete#●ready to prove

The decision problem SUBGRAPH ISOMORPHISM belongs to NP, and every decision problem \(L\) in NP has a polynomial-time many-one reduction to SUBGRAPH ISOMORPHISM.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), SUBGRAPH ISOMORPHISM.

Uses 5

Statement usesPolynomial-time many-one reduction · SUBGRAPH ISOMORPHISM 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.