Subgraph Isomorphism is NP-complete

SUBGRAPH ISOMORPHISM: does the host graph contain a subgraph isomorphic to the pattern graph? Equivalently – and this is the definition used here, DescriptiveComplexity.SubgraphIsoOn – is there an injective homomorphism of the pattern into the host? (Not an induced subgraph: non-edges of the pattern are unconstrained, which is the standard reading and the one that makes Clique a special case.)

Two graphs in one structure

An instance carries two graphs, so FirstOrder.Language.twoGraphs has two unary marks separating the pattern vertices from the host vertices and two binary relations for the two adjacency relations. As with the set systems of DescriptiveComplexity.Problems.SetFamily, nothing forces an element of the universe to be a vertex of either graph: elements outside both marks are junk that no condition mentions, which is exactly what lets a first-order interpretation build such a structure inside a tagged power of its input universe. The guessed map is likewise unconstrained off the pattern.

This vocabulary pattern – several structures side by side in one universe, separated by marks – is the natural home for the remaining combinatorial-packing problems (Exact Cover, 3-Dimensional Matching), where the same trick applies.

Hardness: a clique is a complete pattern

The reduction is from Clique (DescriptiveComplexity.clique_fo_reduction_subgraphIso, tag Bool, dimension 1, quantifier-free): the host is the input graph and the pattern is the complete graph on its marked set, so an injective homomorphism of the pattern is precisely a clique at least as large as the marked set. The threshold of Clique is thus consumed by the shape of the pattern rather than by a counting argument – no Set.ncard reasoning appears in this file beyond the embedding form DescriptiveComplexity.cliqueOn_iff_embedding that Clique already provides.

inductive FirstOrder.Language.twoGraphsRel : ℕ → Type

Relation symbols of the language of pattern-and-host graphs.

• patV : twoGraphsRel 1

  patV a: a is a vertex of the pattern graph.

• hostV : twoGraphsRel 1

  hostV a: a is a vertex of the host graph.

• patE : twoGraphsRel 2

  patE a b: there is an edge of the pattern from a to b.

• hostE : twoGraphsRel 2

  hostE a b: there is an edge of the host from a to b.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqTwoGraphsRel {a✝ : ℕ} : DecidableEq (twoGraphsRel a✝)

Equations

• FirstOrder.Language.instDecidableEqTwoGraphsRel = FirstOrder.Language.instDecidableEqTwoGraphsRel.decEq

def FirstOrder.Language.instDecidableEqTwoGraphsRel.decEq {a✝ : ℕ} (x✝ x✝¹ : twoGraphsRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

def FirstOrder.Language.twoGraphs : Language

The relational language of pattern-and-host graphs: two graphs sharing a universe, each with its own vertex mark and adjacency relation.

Equations

• FirstOrder.Language.twoGraphs = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.twoGraphsRel }

instance FirstOrder.Language.instIsRelationalTwoGraphs : Language.twoGraphs.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.tgPatV : Language.twoGraphs.Relations 1

The pattern-vertex symbol.

Equations

• FirstOrder.Language.tgPatV = FirstOrder.Language.twoGraphsRel.patV

@[reducible, inline]

abbrev FirstOrder.Language.tgHostV : Language.twoGraphs.Relations 1

The host-vertex symbol.

Equations

• FirstOrder.Language.tgHostV = FirstOrder.Language.twoGraphsRel.hostV

@[reducible, inline]

abbrev FirstOrder.Language.tgPatE : Language.twoGraphs.Relations 2

The pattern-adjacency symbol.

Equations

• FirstOrder.Language.tgPatE = FirstOrder.Language.twoGraphsRel.patE

@[reducible, inline]

abbrev FirstOrder.Language.tgHostE : Language.twoGraphs.Relations 2

The host-adjacency symbol.

Equations

• FirstOrder.Language.tgHostE = FirstOrder.Language.twoGraphsRel.hostE

The generic property

def DescriptiveComplexity.SubgraphIsoOn {A : Type} (PV HV : A → Prop) (PE HE : A → A → Prop) : Prop

Some map sends the PV-vertices injectively into the HV-vertices, carrying PE-edges to HE-edges: an injective homomorphism of the pattern into the host.

Equations

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

theorem DescriptiveComplexity.SubgraphIsoOn.of_equiv {A B : Type} (u : B ≃ A) {PVB HVB : B → Prop} {PEB HEB : B → B → Prop} {PVA HVA : A → Prop} {PEA HEA : A → A → Prop} (hPV : ∀ (b : B), PVB b ↔ PVA (u b)) (hHV : ∀ (b : B), HVB b ↔ HVA (u b)) (hPE : ∀ (b b' : B), PEB b b' ↔ PEA (u b) (u b')) (hHE : ∀ (b b' : B), HEB b b' ↔ HEA (u b) (u b')) (h : SubgraphIsoOn PVB HVB PEB HEB) : SubgraphIsoOn PVA HVA PEA HEA

SubgraphIsoOn transports along an equivalence commuting with the four predicates.

theorem DescriptiveComplexity.SubgraphIsoOn.equiv_iff {A B : Type} (u : B ≃ A) {PVB HVB : B → Prop} {PEB HEB : B → B → Prop} {PVA HVA : A → Prop} {PEA HEA : A → A → Prop} (hPV : ∀ (b : B), PVB b ↔ PVA (u b)) (hHV : ∀ (b : B), HVB b ↔ HVA (u b)) (hPE : ∀ (b b' : B), PEB b b' ↔ PEA (u b) (u b')) (hHE : ∀ (b b' : B), HEB b b' ↔ HEA (u b) (u b')) : SubgraphIsoOn PVB HVB PEB HEB ↔ SubgraphIsoOn PVA HVA PEA HEA

SubgraphIsoOn transports along an equivalence, iff version.

The problem

def DescriptiveComplexity.TGPatV {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (a : A) : Prop

Being a vertex of the pattern graph.

Equations

• DescriptiveComplexity.TGPatV a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tgPatV ![a]

def DescriptiveComplexity.TGHostV {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (a : A) : Prop

Being a vertex of the host graph.

Equations

• DescriptiveComplexity.TGHostV a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tgHostV ![a]

def DescriptiveComplexity.TGPatE {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (a b : A) : Prop

Adjacency in the pattern graph.

Equations

• DescriptiveComplexity.TGPatE a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tgPatE ![a, b]

def DescriptiveComplexity.TGHostE {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (a b : A) : Prop

Adjacency in the host graph.

Equations

• DescriptiveComplexity.TGHostE a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tgHostE ![a, b]

def DescriptiveComplexity.HasSubgraphIso (A : Type) [FirstOrder.Language.twoGraphs.Structure A] : Prop

The host graph contains a subgraph isomorphic to the pattern graph. (Finiteness of the universe is required only for uniformity with the rest of the catalog; the property itself makes sense in general.)

Equations

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

theorem DescriptiveComplexity.hasSubgraphIso_iso {A B : Type} [FirstOrder.Language.twoGraphs.Structure A] [FirstOrder.Language.twoGraphs.Structure B] (e : FirstOrder.Language.twoGraphs.Equiv A B) : HasSubgraphIso A ↔ HasSubgraphIso B

The subgraph-isomorphism property is isomorphism-invariant.

def DescriptiveComplexity.SubgraphIso : DecisionProblem FirstOrder.Language.twoGraphs

SUBGRAPH ISOMORPHISM, as a problem on pattern-and-host structures: does the host contain a subgraph isomorphic to the pattern?

Equations

• DescriptiveComplexity.SubgraphIso = { Holds := fun (A : Type) (inst : FirstOrder.Language.twoGraphs.Structure A) => DescriptiveComplexity.HasSubgraphIso A, iso_invariant := ⋯ }

Clique reduces to Subgraph Isomorphism

def DescriptiveComplexity.cliquePatternInterp : FOInterpretation FirstOrder.Language.markedGraph FirstOrder.Language.twoGraphs Bool 1

The interpretation of Clique into Subgraph Isomorphism: the tag true carries the pattern – the complete graph on the marked set – and the tag false the host, which is the input graph.

Equations

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

def DescriptiveComplexity.patPt {A : Type} (v : A) : cliquePatternInterp.Map A

The pattern copy of a vertex.

Equations

• DescriptiveComplexity.patPt v = (true, fun (x : Fin 1) => v)

def DescriptiveComplexity.hostPt {A : Type} (v : A) : cliquePatternInterp.Map A

The host copy of a vertex.

Equations

• DescriptiveComplexity.hostPt v = (false, fun (x : Fin 1) => v)

theorem DescriptiveComplexity.patPt_injective {A : Type} : Function.Injective patPt

theorem DescriptiveComplexity.hostPt_injective {A : Type} : Function.Injective hostPt

theorem DescriptiveComplexity.patPt_eta {A : Type} (w : Fin 1 → A) : (true, w) = patPt (w 0)

theorem DescriptiveComplexity.hostPt_eta {A : Type} (w : Fin 1 → A) : (false, w) = hostPt (w 0)

@[simp]

theorem DescriptiveComplexity.clPat_patV {A : Type} [FirstOrder.Language.markedGraph.Structure A] (v : A) : TGPatV (patPt v) ↔ MGMarked v

@[simp]

theorem DescriptiveComplexity.clPat_patV_host {A : Type} [FirstOrder.Language.markedGraph.Structure A] (v : A) : ¬TGPatV (hostPt v)

@[simp]

theorem DescriptiveComplexity.clPat_hostV {A : Type} [FirstOrder.Language.markedGraph.Structure A] (v : A) : TGHostV (hostPt v)

@[simp]

theorem DescriptiveComplexity.clPat_hostV_pat {A : Type} [FirstOrder.Language.markedGraph.Structure A] (v : A) : ¬TGHostV (patPt v)

@[simp]

theorem DescriptiveComplexity.clPat_patE {A : Type} [FirstOrder.Language.markedGraph.Structure A] (u v : A) : TGPatE (patPt u) (patPt v) ↔ u ≠ v ∧ MGMarked u ∧ MGMarked v

@[simp]

theorem DescriptiveComplexity.clPat_hostE {A : Type} [FirstOrder.Language.markedGraph.Structure A] (u v : A) : TGHostE (hostPt u) (hostPt v) ↔ u ≠ v ∧ MGAdj u v

theorem DescriptiveComplexity.patV_eq_patPt {A : Type} [FirstOrder.Language.markedGraph.Structure A] {p : cliquePatternInterp.Map A} (h : TGPatV p) : ∃ (v : A), p = patPt v

Only pattern copies are pattern vertices.

theorem DescriptiveComplexity.hostV_eq_hostPt {A : Type} [FirstOrder.Language.markedGraph.Structure A] {p : cliquePatternInterp.Map A} (h : TGHostV p) : ∃ (v : A), p = hostPt v

Only host copies are host vertices, so the image of a pattern vertex is a host copy.

theorem DescriptiveComplexity.hasLargeClique_iff_subgraphIso_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasLargeClique A ↔ HasSubgraphIso (cliquePatternInterp.Map A)

Correctness of the interpretation: a graph has a clique at least as large as its marked set iff the complete graph on that marked set embeds into it.

def DescriptiveComplexity.clique_fo_reduction_subgraphIso : FOReduction Clique SubgraphIso

Clique FO-reduces to Subgraph Isomorphism: the pattern is the complete graph on the marked set, the host is the input graph.

Equations

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

Membership

def DescriptiveComplexity.isoGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Subgraph Isomorphism: one binary relation variable, the guessed map.

Equations

• DescriptiveComplexity.isoGuessBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 2 }

def DescriptiveComplexity.sgMapRel : isoGuessBlock.lang.Relations 2

The symbol of the guessed map.

Equations

• DescriptiveComplexity.sgMapRel = ⟨(), DescriptiveComplexity.sgMapRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.subgraphSOLang : FirstOrder.Language

The vocabulary of the kernel: pattern-and-host structures together with the guessed map.

Equations

• DescriptiveComplexity.subgraphSOLang = FirstOrder.Language.twoGraphs.sum DescriptiveComplexity.isoGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.sgPatVSym : subgraphSOLang.Relations 1

The pattern-vertex symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.sgPatVSym = Sum.inl FirstOrder.Language.tgPatV

@[reducible, inline]

abbrev DescriptiveComplexity.sgHostVSym : subgraphSOLang.Relations 1

The host-vertex symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.sgHostVSym = Sum.inl FirstOrder.Language.tgHostV

@[reducible, inline]

abbrev DescriptiveComplexity.sgPatESym : subgraphSOLang.Relations 2

The pattern-adjacency symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.sgPatESym = Sum.inl FirstOrder.Language.tgPatE

@[reducible, inline]

abbrev DescriptiveComplexity.sgHostESym : subgraphSOLang.Relations 2

The host-adjacency symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.sgHostESym = Sum.inl FirstOrder.Language.tgHostE

@[reducible, inline]

abbrev DescriptiveComplexity.sgMapSym : subgraphSOLang.Relations 2

The guessed-map symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.sgMapSym = Sum.inr DescriptiveComplexity.sgMapRel

noncomputable def DescriptiveComplexity.subgraphKernel : subgraphSOLang.Sentence

The first-order kernel of the Σ₁ definition of Subgraph Isomorphism.

Equations

• DescriptiveComplexity.subgraphKernel = DescriptiveComplexity.sgTotalClause✝ ⊓ (DescriptiveComplexity.sgInjClause✝ ⊓ DescriptiveComplexity.sgEdgeClause✝)

theorem DescriptiveComplexity.subgraphIso_sigmaSODefinable : SigmaSODefinable 1 SubgraphIso

Subgraph Isomorphism is Σ₁-definable: existentially guess the map, then check first-order that it sends pattern vertices to host vertices, injectively, carrying pattern edges to host edges.

NP-completeness

theorem DescriptiveComplexity.subgraphIso_mem_NP : NP.Mem SubgraphIso

Subgraph Isomorphism is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.subgraphIso_NP_hard : NP.Hard SubgraphIso

Subgraph Isomorphism is NP-hard: Clique, which is NP-hard, reduces to it by taking the complete graph on the marked set as pattern.

theorem DescriptiveComplexity.subgraphIso_NP_complete : NP.Complete SubgraphIso

Subgraph Isomorphism is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.