Maximum leaf spanning tree

AbbreviationInstances of MAXIMUM LEAF SPANNING TREE#✓fully proved

An instance of MAXIMUM LEAF SPANNING TREE is a triple \((n, es, K)\) of a natural number \(n\) (the number of vertices), a list \(es\) of pairs of natural numbers (the edge list) and a natural number \(K\) (the bound on the number of leaves).

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

Used by 3

Used byThe decision problem MAXIMUM LEAF SPANNING TREE · Feasible MAXIMUM LEAF SPANNING TREE instances · Well-formed MAXIMUM LEAF SPANNING TREE instances

DefinitionWell-formed MAXIMUM LEAF SPANNING TREE instances#✓fully proved

An instance \((n, es, K)\) of MAXIMUM LEAF SPANNING TREE is well formed when \(n > 0\), the list \(es\) has no repeated entries, and every entry \((u, v)\) of \(es\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and \((v, u)\) is not an entry of \(es\).

def WellFormed (i : MaximumLeafSpanningTreeInstance) : Prop :=
  0 < i.1 ∧ 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

Uses 1 · Used by 1

Statement usesInstances of MAXIMUM LEAF SPANNING TREE

Used byThe decision problem MAXIMUM LEAF SPANNING TREE

DefinitionFeasible MAXIMUM LEAF SPANNING TREE instances#✓fully proved

An instance \((n, es, K)\) of MAXIMUM LEAF SPANNING TREE is feasible when there are a sublist \(T\) of \(es\) (a list obtained from \(es\) by deleting entries) with no repeated entries and exactly \(n - 1\) entries, and a set \(L\) of at least \(K\) vertices in \(\{0, \dots, n - 1\}\), such that the simple graph on \(\{0, \dots, n - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) is an entry of \(T\) is connected, and each vertex in \(L\) is an endpoint of exactly one entry of \(T\).

def MaximumLeafSpanningTreeFeasible
    (i : MaximumLeafSpanningTreeInstance) : Prop :=
  ∃ T : List (ℕ × ℕ), T.Sublist i.2.1 ∧ T.Nodup ∧ T.length = i.1 - 1 ∧
    (Cslib.Complexity.Karp.edgeGraph i.1 T).Connected ∧
    ∃ leaves : Finset (Fin i.1), i.2.2 ≤ leaves.card ∧
      ∀ v ∈ leaves, ∃! e ∈ T, e.1 = (v : ℕ) ∨ e.2 = (v : ℕ)

Uses 2 · Used by 1

Statement usesGraph of an edge list · Instances of MAXIMUM LEAF SPANNING TREE

Used byThe decision problem MAXIMUM LEAF SPANNING TREE

DefinitionThe decision problem MAXIMUM LEAF SPANNING TREE#✓fully proved

The decision problem MAXIMUM LEAF SPANNING TREE accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of instances, to an instance \((n, es, K)\) of MAXIMUM LEAF SPANNING TREE that is well formed and feasible (its graph has a spanning tree with at least \(K\) leaves). Bitstrings that do not decode are rejected.

noncomputable def maximumLeafSpanningTreeDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MaximumLeafSpanningTreeInstance) x with
  | some i => decide (WellFormed i ∧ MaximumLeafSpanningTreeFeasible 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 MAXIMUM LEAF SPANNING TREE instances · Instances of MAXIMUM LEAF SPANNING TREE · Well-formed MAXIMUM LEAF SPANNING TREE instances · Decision problems

Used byMAXIMUM LEAF SPANNING TREE is NP-complete

TheoremMAXIMUM LEAF SPANNING TREE is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MAXIMUM LEAF SPANNING TREE.

Uses 5

Statement usesPolynomial-time many-one reduction · The decision problem MAXIMUM LEAF SPANNING TREE · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.