Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax17.Treewidth

Treewidth

concepts/Lax17/Treewidth.lean · lax-17

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    A tree decomposition of a finite simple graph consists of a finite tree and a bag of graph vertices at every tree node. Every graph vertex occurs in a bag, the endpoints of every graph edge occur together in a bag, and the tree nodes whose bags contain any fixed graph vertex induce a connected subtree.

    The width of a decomposition is its largest bag cardinality minus one, using natural-number subtraction. The treewidth of a graph is the least width of any of its tree decompositions. The natural-number convention gives the empty graph treewidth zero.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Acyclic
    2
    3/-!
    4---
    5title: Treewidth
    6type: definition
    7---
    8A tree decomposition of a finite simple graph consists of a finite tree and
    9a bag of graph vertices at every tree node. Every graph vertex occurs in a
    10bag, the endpoints of every graph edge occur together in a bag, and the tree
    11nodes whose bags contain any fixed graph vertex induce a connected subtree.
    12
    13The width of a decomposition is its largest bag cardinality minus one, using
    14natural-number subtraction. The treewidth of a graph is the least width of
    15any of its tree decompositions. The natural-number convention gives the empty
    16graph treewidth zero.
    17-/
    18
    19namespace Lax17.Treewidth
    20
    21universe u
    22
    23/-- A finite tree decomposition of a simple graph. -/
    24structure TreeDecomposition {V : Type u} [DecidableEq V]
    25 (G : SimpleGraph V) where
    26 /-- The node type of the decomposition tree. -/
    27 Node : Type
    28 /-- The decomposition tree has finitely many nodes. -/
    29 [nodeFintype : Fintype Node]
    30 /-- Decomposition-tree nodes have decidable equality. -/
    31 [nodeDecidableEq : DecidableEq Node]
    32 /-- The tree on decomposition nodes. -/
    33 tree : SimpleGraph Node
    34 /-- The node graph is a tree. -/
    35 isTree : tree.IsTree
    36 /-- The bag assigned to each decomposition node. -/
    37 bag : Node → Finset V
    38 /-- Every graph vertex occurs in a bag. -/
    39 vertex_mem_bag : ∀ v : V, ∃ i : Node, v ∈ bag i
    40 /-- The endpoints of every graph edge occur together in a bag. -/
    41 edge_mem_bag :
    42 ∀ ⦃x y : V⦄, G.Adj x y → ∃ i : Node, x ∈ bag i ∧ y ∈ bag i
    43 /-- Bags containing a fixed graph vertex induce a connected subtree. -/
    44 bag_indices_connected :
    45 ∀ v : V, (tree.induce {i : Node | v ∈ bag i}).Connected
    46
    47namespace TreeDecomposition
    48
    49/-- The maximum bag cardinality minus one. -/
    50noncomputable def width {V : Type u} [DecidableEq V]
    51 {G : SimpleGraph V} (D : TreeDecomposition G) : ℕ :=
    52 letI : Fintype D.Node := D.nodeFintype
    53 (Finset.univ.sup fun i : D.Node => (D.bag i).card) - 1
    54
    55end TreeDecomposition
    56
    57/-- `G` has a tree decomposition of width at most `k`. -/
    58def HasTreewidthAtMost {V : Type u} [Fintype V] [DecidableEq V]
    59 (G : SimpleGraph V) (k : ℕ) : Prop :=
    60 ∃ D : TreeDecomposition G, D.width ≤ k
    61
    62/-- The least width of a tree decomposition of `G`.
    63
    64The fallback makes the definition total. For a finite graph it is unreachable,
    65because the decomposition with one bag containing every vertex always exists.
    66-/
    67noncomputable def treewidth {V : Type u} [Fintype V] [DecidableEq V]
    68 (G : SimpleGraph V) : ℕ :=
    69 letI := Classical.decPred (HasTreewidthAtMost G)
    70 letI := Classical.propDecidable (∃ k, HasTreewidthAtMost G k)
    71 if h : ∃ k, HasTreewidthAtMost G k then Nat.find h else 0
    72
    73end Lax17.Treewidth
    74

    Builds on

    none

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…