nothing to prove
Definition
A tree decomposition of a finite simple graph consists of a finite tree and a bag 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 .
The treewidth is the least such that has a tree decomposition with every bag of size at most .
Lean source
| 1 | import Mathlib.Combinatorics.SimpleGraph.Acyclic |
| 2 | import Mathlib.Data.Nat.Lattice |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Treewidth |
| 7 | type: definition |
| 8 | --- |
| 9 | A tree decomposition of a finite simple graph $G$ consists of a finite tree |
| 10 | $T$ and a bag $X_t \subseteq V(G)$ at each node $t$ such that every graph |
| 11 | vertex occurs in a bag, the endpoints of every graph edge occur together in a |
| 12 | bag, and the nodes whose bags contain any fixed vertex induce a connected |
| 13 | subgraph of $T$. |
| 14 | |
| 15 | The treewidth $\operatorname{tw}(G)$ is the least $w$ such that $G$ has a |
| 16 | tree decomposition with every bag of size at most $w+1$. |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | A tree decomposition always exists (a single node whose bag is all of |
| 21 | $V(G)$), so the infimum in `treewidth` ranges over a nonempty set. The |
| 22 | `Fintype` and `DecidableEq` hypotheses of `treewidth` are the uniform |
| 23 | signature shared by all graph parameters in this archive. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax1.Treewidth |
| 27 | |
| 28 | /-- A tree decomposition of a simple graph: a finite tree of nodes with a bag |
| 29 | of graph vertices at each node, such that the bags cover every vertex and |
| 30 | every edge, and the nodes whose bags contain any fixed vertex induce a |
| 31 | connected subgraph of the tree. -/ |
| 32 | structure 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` |
| 53 | vertices. -/ |
| 54 | def 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 |
| 58 | graph has a tree decomposition with bags of at most `w + 1` vertices. -/ |
| 59 | noncomputable def treewidth {V : Type} [Fintype V] [DecidableEq V] |
| 60 | (G : SimpleGraph V) : ℕ := |
| 61 | sInf {w | HasTreewidthAtMost G w} |
| 62 | |
| 63 | end Lax1.Treewidth |
| 64 |
Formalization notes
A tree decomposition always exists (a single node whose bag is all of
), so the infimum in treewidth ranges over a nonempty set. The
Fintype and DecidableEq hypotheses of treewidth are the uniform
signature shared by all graph parameters in this archive.
Imported
none