Induced subgraph isomorphism

AbbreviationInduced-subgraph-isomorphism instance#✓fully proved

An instance of INDUCED SUBGRAPH ISOMORPHISM is a quadruple \((n, E, k, F)\) consisting of a natural number \(n\) (the number of host vertices), a list \(E\) of pairs of natural numbers (the host edges), a natural number \(k\) (the number of pattern vertices) and a list \(F\) of pairs of natural numbers (the pattern edges).

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

Used by 5

Used byHost graph of an induced-subgraph-isomorphism instance · Pattern graph of an induced-subgraph-isomorphism instance · INDUCED SUBGRAPH ISOMORPHISM as a decision problem · Induced embedding of the pattern into the host · Well-formed induced-subgraph-isomorphism instance

DefinitionHost graph of an induced-subgraph-isomorphism instance#✓fully proved

For an instance \((n, E, k, F)\), the host graph is the graph of the edge list \(E\) 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\).

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

Uses 2 · Used by 1

Statement usesGraph of an edge list · Induced-subgraph-isomorphism instance

Used byInduced embedding of the pattern into the host

DefinitionPattern graph of an induced-subgraph-isomorphism instance#✓fully proved

For an instance \((n, E, k, F)\), the pattern graph is the graph of the edge list \(F\) on \(k\) vertices: the simple graph on \(\{0, \dots, k - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(F\).

def GraphPattern (i : InducedSubgraphIsomorphismInstance) :
    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 · Induced-subgraph-isomorphism instance

Used byInduced embedding of the pattern into the host

DefinitionWell-formed induced-subgraph-isomorphism instance#✓fully proved

An instance \((n, E, k, F)\) is well-formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\), and likewise the list \(F\) has no repeated entries and every pair \((u, v)\) in \(F\) satisfies \(u < k\), \(v < k\), \(u \ne v\) and \((v, u) \notin F\).

def WellFormed (i : InducedSubgraphIsomorphismInstance) : 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 usesInduced-subgraph-isomorphism instance

Used byINDUCED SUBGRAPH ISOMORPHISM as a decision problem

DefinitionInduced embedding of the pattern into the host#✓fully proved

An instance \((n, E, k, F)\) is feasible when there is an injective map \(f\) from \(\{0, \dots, k - 1\}\) to \(\{0, \dots, n - 1\}\) such that, for all \(a, b \in \{0, \dots, k - 1\}\), the vertices \(a\) and \(b\) are adjacent in the pattern graph if and only if \(f(a)\) and \(f(b)\) are adjacent in the host graph.

def InducedSubgraphIsomorphismFeasible
    (i : InducedSubgraphIsomorphismInstance) : Prop :=
  ∃ f : Fin i.2.2.1 → Fin i.1, Function.Injective f ∧
    ∀ a b : Fin i.2.2.1,
      (GraphPattern i).Adj a b ↔ (GraphHost i).Adj (f a) (f b)

Uses 3 · Used by 1

Statement usesHost graph of an induced-subgraph-isomorphism instance · Pattern graph of an induced-subgraph-isomorphism instance · Induced-subgraph-isomorphism instance

Used byINDUCED SUBGRAPH ISOMORPHISM as a decision problem

DefinitionINDUCED SUBGRAPH ISOMORPHISM as a decision problem#✓fully proved

The decision problem INDUCED SUBGRAPH ISOMORPHISM accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance \((n, E, k, F)\) (host vertex count, host edge list, pattern vertex count, pattern edge list) that is well-formed and for which there is an injective map \(f\) from \(\{0, \dots, k - 1\}\) to \(\{0, \dots, n - 1\}\) such that, for all \(a\) and \(b\), the vertices \(a\) and \(b\) are adjacent in the pattern graph if and only if \(f(a)\) and \(f(b)\) are adjacent in the host graph. Bitstrings that do not decode to an instance are rejected.

noncomputable def inducedSubgraphIsomorphismDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := InducedSubgraphIsomorphismInstance) x with
  | some i => decide (WellFormed i ∧ InducedSubgraphIsomorphismFeasible 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 · Induced embedding of the pattern into the host · Induced-subgraph-isomorphism instance · Well-formed induced-subgraph-isomorphism instance · Decision problems

Used byINDUCED SUBGRAPH ISOMORPHISM is NP-complete

TheoremINDUCED SUBGRAPH ISOMORPHISM is NP-complete#●ready to prove

The decision problem INDUCED SUBGRAPH ISOMORPHISM is in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

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

Uses 5

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

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.