Lax Lean Archive

Lax48.Treewidth

Treewidth

concepts/Lax48/Treewidth.lean · lax-48

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

    In the paper

    • page 2 of this submission's paper

    Definition

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

    The treewidth of G is the least w such that G has a tree decomposition with every bag of size at most w + 1.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Acyclic
    2import Mathlib.Data.Nat.Lattice
    3
    4/-!
    5---
    6title: Treewidth
    7type: definition
    8---
    9A tree decomposition of a finite simple graph *G* consists of a finite tree
    10*T* and a bag of graph vertices at each node such that every graph
    11vertex occurs in a bag, the endpoints of every graph edge occur together in a
    12bag, and the nodes whose bags contain any fixed vertex induce a connected
    13subgraph of *T*.
    14
    15The treewidth of *G* is the least *w* such that *G* has a tree
    16decomposition with every bag of size at most *w* + 1.
    17
    18# Formalization notes
    19
    20A tree decomposition always exists (a single node whose bag is all of the
    21vertices), so the infimum in `treewidth` ranges over a nonempty set. The
    22`Fintype` and `DecidableEq` hypotheses of `treewidth` are the uniform
    23signature shared by all graph parameters in this archive.
    24-/
    25
    26namespace Lax48.Treewidth
    27
    28/-- A tree decomposition of a simple graph: a finite tree of nodes with a bag
    29of graph vertices at each node, such that the bags cover every vertex and
    30every edge, and the nodes whose bags contain any fixed vertex induce a
    31connected subgraph of the tree. -/
    32structure TreeDecomposition {V : Type} (G : SimpleGraph V) where
    33 /-- The node type of the decomposition tree. -/
    34 Node : Type
    35 /-- The decomposition tree is finite. -/
    36 [nodeFintype : Fintype Node]
    37 /-- The graph on the decomposition nodes. -/
    38 tree : SimpleGraph Node
    39 /-- The node graph is a tree. -/
    40 isTree : tree.IsTree
    41 /-- The bag assigned to each decomposition node. -/
    42 bag : Node → Finset V
    43 /-- Every graph vertex appears in at least one bag. -/
    44 vertex_mem_bag : ∀ v : V, ∃ i : Node, v ∈ bag i
    45 /-- Every graph edge has both endpoints together in at least one bag. -/
    46 edge_mem_bag : ∀ ⦃u v : V⦄, G.Adj u v → ∃ i : Node, u ∈ bag i ∧ v ∈ bag i
    47 /-- For each graph vertex, the nodes whose bags contain it induce a
    48 connected subgraph of the tree. -/
    49 bag_indices_connected :
    50 ∀ v : V, (tree.induce {i : Node | v ∈ bag i}).Connected
    51
    52/-- `G` has a tree decomposition all of whose bags have at most `w + 1`
    53vertices. -/
    54def HasTreewidthAtMost {V : Type} (G : SimpleGraph V) (w : ℕ) : Prop :=
    55 ∃ D : TreeDecomposition G, ∀ i, (D.bag i).card ≤ w + 1
    56
    57/-- The treewidth of a finite simple graph: the least `w` such that the
    58graph has a tree decomposition with bags of at most `w + 1` vertices. -/
    59noncomputable def treewidth {V : Type} [Fintype V] [DecidableEq V]
    60 (G : SimpleGraph V) : ℕ :=
    61 sInf {w | HasTreewidthAtMost G w}
    62
    63end Lax48.Treewidth
    64

    Formalization notes

    A tree decomposition always exists (a single node whose bag is all of the vertices), so the infimum in treewidthtreewidth ranges over a nonempty set. The FintypeFintype and DecidableEqDecidableEq hypotheses of treewidthtreewidth are the uniform signature shared by all graph parameters in this archive.

    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…