Steiner tree

AbbreviationSteiner tree instances#✓fully proved

A Steiner tree instance is a quadruple \((n, E, R, K)\) of a natural number \(n\) (the number of vertices), a list \(E\) of triples \((u, v, w)\) of natural numbers (an edge between \(u\) and \(v\) of weight \(w\)), a list \(R\) of natural numbers (the terminals) and a natural number \(K\) (the budget).

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

Used by 4

Used byGraph of a candidate edge set · The STEINER TREE decision problem · Feasible Steiner tree instances · Well-formed Steiner tree instances

DefinitionGraph of a candidate edge set#✓fully proved

Given a Steiner tree instance with vertex count \(n\) and a list \(T\) of triples \((u, v, w)\) of natural numbers, the graph of \(T\) is the simple graph on \(\{0, \dots, n - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j, w)\) or \((j, i, w)\) belongs to \(T\) for some natural number \(w\). Weights are ignored, and triples with an endpoint at least \(n\) contribute no edge.

def Graph (i : SteinerTreeInstance) (T : List (ℕ × ℕ × ℕ)) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 (T.map fun e => (e.1, e.2.1))

Uses 2 · Used by 1

Statement usesGraph of an edge list · Steiner tree instances

Used byFeasible Steiner tree instances

DefinitionWell-formed Steiner tree instances#✓fully proved

A Steiner tree instance with vertex count \(n\), edge list \(E\) of triples \((u, v, w)\) and terminal list \(R\) is well formed when \(E\) has no repeated entries; every \((u, v, w)\) in \(E\) has \(u < n\), \(v < n\), \(u \ne v\) and \(w > 0\); any two entries of \(E\) with the same endpoints, in the same or the reverse order, are equal; \(R\) has no repeated entries; and every terminal in \(R\) is less than \(n\).

def WellFormed (i : SteinerTreeInstance) : Prop :=
  i.2.1.Nodup ∧
    (∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2.1 < i.1 ∧ e.1 ≠ e.2.1 ∧ 0 < e.2.2) ∧
    (∀ e1 ∈ i.2.1, ∀ e2 ∈ i.2.1,
      (e1.1 = e2.1 ∧ e1.2.1 = e2.2.1 ∨ e1.1 = e2.2.1 ∧ e1.2.1 = e2.1) → e1 = e2) ∧
    i.2.2.1.Nodup ∧ ∀ t ∈ i.2.2.1, t < i.1

Uses 1 · Used by 1

Statement usesSteiner tree instances

Used byThe STEINER TREE decision problem

DefinitionFeasible Steiner tree instances#✓fully proved

A Steiner tree instance with vertex count \(n\), edge list \(E\) of triples \((u, v, w)\), terminal list \(R\) and budget \(K\) is feasible when every terminal in \(R\) is less than \(n\) and there is a sublist \(T\) of \(E\) (a not necessarily contiguous subsequence) whose weights \(w\) sum to at most \(K\) such that any two terminals in \(R\) are joined by a path in the graph of \(T\), the simple graph on \(\{0, \dots, n - 1\}\) in which distinct vertices are adjacent when they are the endpoints \(u, v\) of some triple in \(T\).

def SteinerTreeFeasible
    (i : SteinerTreeInstance) : Prop :=
  ∃ T : List (ℕ × ℕ × ℕ), T.Sublist i.2.1 ∧ (T.map (fun e => e.2.2)).sum ≤ i.2.2.2 ∧
    (∀ t ∈ i.2.2.1, t < i.1) ∧
    ∀ a ∈ i.2.2.1, ∀ ha : a < i.1, ∀ b ∈ i.2.2.1, ∀ hb : b < i.1,
      (Graph i T).Reachable ⟨a, ha⟩ ⟨b, hb⟩

Uses 2 · Used by 1

Statement usesGraph of a candidate edge set · Steiner tree instances

Used byThe STEINER TREE decision problem

DefinitionThe STEINER TREE decision problem#✓fully proved

The decision problem STEINER TREE accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of Steiner tree instances, to a Steiner tree instance that is both well formed and feasible. Bitstrings that do not decode are rejected.

noncomputable def steinerTreeDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := SteinerTreeInstance) x with
  | some i => decide (WellFormed i ∧ SteinerTreeFeasible 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 Steiner tree instances · Steiner tree instances · Well-formed Steiner tree instances · Decision problems

Used bySTEINER TREE is NP-complete

TheoremSTEINER TREE is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), STEINER TREE IN GRAPHS; R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

Statement usesPolynomial-time many-one reduction · The STEINER TREE 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.