Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Paper

Twin-Width Can Be Exponential in Treewidth

11 pages · 7 marked passages · pdflatex · download PDF · lax-48

lax-48

defLax48.TwinWidth

Twin-width

A partition sequence of a finite simple graph G is a sequence of partitions of its vertex set that starts at the partition into singletons, merges two parts into one at every step, and ends at the partition with a single part. Two parts of a same partition are homogeneous if either every pair of vertices across them is adjacent or none is; two non-homogeneous parts are red-adjacent. The red degree of a part is the number of other parts of its partition that are red-adjacent to it.

The twin-width of G is the least d such that G has a partition sequence in which every part of every partition has red degree at most d.

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2	import Mathlib.Data.Set.Card
3	import Mathlib.Data.Nat.Lattice
4
	… module docstring, 25 lines
30
31	namespace Lax48.TwinWidth
32
33	/-- Two vertex sets are homogeneous in `G`: either every pair of vertices
34	across them is adjacent, or none is. -/
35	def Homogeneous {V : Type} (G : SimpleGraph V) (A B : Finset V) : Prop :=
36	(∀ a ∈ A, ∀ b ∈ B, G.Adj a b) ∨ (∀ a ∈ A, ∀ b ∈ B, ¬ G.Adj a b)
37
38	/-- The red degree of a part `A` in a family of parts `P`: the number of
39	other parts of `P` that are not homogeneous with `A`. -/
40	noncomputable def redDegree {V : Type} (G : SimpleGraph V)
41	(P : Finset (Finset V)) (A : Finset V) : ℕ :=
42	{B \| B ∈ P ∧ B ≠ A ∧ ¬ Homogeneous G A B}.ncard
43
44	/-- The partition of a finite vertex type into singletons. -/
45	def singletonPartition (V : Type) [Fintype V] [DecidableEq V] :
46	Finset (Finset V) :=
47	Finset.univ.image fun v : V => ({v} : Finset V)
48
49	/-- A partition sequence of `G` in which every part has red degree at most
50	`d`: starting from the singleton partition, each step merges two parts into
51	one, until a single part remains. -/
52	structure PartitionSequence {V : Type} [Fintype V] [DecidableEq V]
53	(G : SimpleGraph V) (d : ℕ) where
54	/-- The number of merge steps. -/
55	stepCount : ℕ
56	/-- The partition after each number of merge steps. -/
57	partition : ℕ → Finset (Finset V)
58	/-- The sequence starts at the singleton partition. -/
59	starts : partition 0 = singletonPartition V
60	/-- The sequence ends with a single part. -/
61	ends : (partition stepCount).card ≤ 1
62	/-- Each step merges two distinct parts into one and keeps all other
63	parts. -/
64	step_merges :
65	∀ i, i < stepCount → ∃ A ∈ partition i, ∃ B ∈ partition i, A ≠ B ∧
66	partition (i + 1) = insert (A ∪ B) (((partition i).erase A).erase B)
67	/-- Every part of every partition in the sequence has red degree at most
68	`d`. -/
69	redDegree_le :
70	∀ i, i ≤ stepCount → ∀ ⦃A⦄, A ∈ partition i →
71	redDegree G (partition i) A ≤ d
72
73	/-- `G` has a partition sequence in which every part has red degree at most
74	`d`. -/
75	def HasTwinWidthAtMost {V : Type} [Fintype V] [DecidableEq V]
76	(G : SimpleGraph V) (d : ℕ) : Prop :=
77	Nonempty (PartitionSequence G d)
78
79	/-- The twin-width of a finite simple graph: the least `d` such that the
80	graph has a partition sequence in which every part has red degree at most
81	`d`. -/
82	noncomputable def twinWidth {V : Type} [Fintype V] [DecidableEq V]
83	(G : SimpleGraph V) : ℕ :=
84	sInf {d \| HasTwinWidthAtMost G d}
85
86	end Lax48.TwinWidth
87

defLax48.Treewidth

Treewidth

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.

1	import Mathlib.Combinatorics.SimpleGraph.Acyclic
2	import Mathlib.Data.Nat.Lattice
3
	… module docstring, 21 lines
25
26	namespace Lax48.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 Lax48.Treewidth
64

thm✓Lax48.ExponentialSeparation

defLax48.TwinWidth

Twin-width

The twin-width of G is the least d such that G has a partition sequence in which every part of every partition has red degree at most d.

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2	import Mathlib.Data.Set.Card
3	import Mathlib.Data.Nat.Lattice
4
	… module docstring, 25 lines
30
31	namespace Lax48.TwinWidth
32
33	/-- Two vertex sets are homogeneous in `G`: either every pair of vertices
34	across them is adjacent, or none is. -/
35	def Homogeneous {V : Type} (G : SimpleGraph V) (A B : Finset V) : Prop :=
36	(∀ a ∈ A, ∀ b ∈ B, G.Adj a b) ∨ (∀ a ∈ A, ∀ b ∈ B, ¬ G.Adj a b)
37
38	/-- The red degree of a part `A` in a family of parts `P`: the number of
39	other parts of `P` that are not homogeneous with `A`. -/
40	noncomputable def redDegree {V : Type} (G : SimpleGraph V)
41	(P : Finset (Finset V)) (A : Finset V) : ℕ :=
42	{B \| B ∈ P ∧ B ≠ A ∧ ¬ Homogeneous G A B}.ncard
43
44	/-- The partition of a finite vertex type into singletons. -/
45	def singletonPartition (V : Type) [Fintype V] [DecidableEq V] :
46	Finset (Finset V) :=
47	Finset.univ.image fun v : V => ({v} : Finset V)
48
49	/-- A partition sequence of `G` in which every part has red degree at most
50	`d`: starting from the singleton partition, each step merges two parts into
51	one, until a single part remains. -/
52	structure PartitionSequence {V : Type} [Fintype V] [DecidableEq V]
53	(G : SimpleGraph V) (d : ℕ) where
54	/-- The number of merge steps. -/
55	stepCount : ℕ
56	/-- The partition after each number of merge steps. -/
57	partition : ℕ → Finset (Finset V)
58	/-- The sequence starts at the singleton partition. -/
59	starts : partition 0 = singletonPartition V
60	/-- The sequence ends with a single part. -/
61	ends : (partition stepCount).card ≤ 1
62	/-- Each step merges two distinct parts into one and keeps all other
63	parts. -/
64	step_merges :
65	∀ i, i < stepCount → ∃ A ∈ partition i, ∃ B ∈ partition i, A ≠ B ∧
66	partition (i + 1) = insert (A ∪ B) (((partition i).erase A).erase B)
67	/-- Every part of every partition in the sequence has red degree at most
68	`d`. -/
69	redDegree_le :
70	∀ i, i ≤ stepCount → ∀ ⦃A⦄, A ∈ partition i →
71	redDegree G (partition i) A ≤ d
72
73	/-- `G` has a partition sequence in which every part has red degree at most
74	`d`. -/
75	def HasTwinWidthAtMost {V : Type} [Fintype V] [DecidableEq V]
76	(G : SimpleGraph V) (d : ℕ) : Prop :=
77	Nonempty (PartitionSequence G d)
78
79	/-- The twin-width of a finite simple graph: the least `d` such that the
80	graph has a partition sequence in which every part has red degree at most
81	`d`. -/
82	noncomputable def twinWidth {V : Type} [Fintype V] [DecidableEq V]
83	(G : SimpleGraph V) : ℕ :=
84	sInf {d \| HasTwinWidthAtMost G d}
85
86	end Lax48.TwinWidth
87

⊢Lax48Proofs.Main.exists_treewidth_le_and_two_pow_lt_twinWidth

Loading the paper…

1	import Lax48.Treewidth
2	import Lax48.TwinWidth
3
	… module docstring, 15 lines
19
20	namespace Lax48.ExponentialSeparation
21
22	/-- For every `k`, some finite graph has treewidth at most `2 * k + 4` and
23	twin-width greater than `2 ^ k`. -/
24	axiom exists_treewidth_le_and_two_pow_lt_twinWidth (k : ℕ) :
25	∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
26	Lax48.Treewidth.treewidth G ≤ 2 * k + 4 ∧
27	2 ^ k < Lax48.TwinWidth.twinWidth G
28
29	end Lax48.ExponentialSeparation
30

1	import Lax48.Treewidth
2	import Lax48.TwinWidth
3
	… module docstring, 15 lines
19
20	namespace Lax48.ExponentialSeparation
21
22	/-- For every `k`, some finite graph has treewidth at most `2 * k + 4` and
23	twin-width greater than `2 ^ k`. -/
24	axiom exists_treewidth_le_and_two_pow_lt_twinWidth (k : ℕ) :
25	∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
26	Lax48.Treewidth.treewidth G ≤ 2 * k + 4 ∧
27	2 ^ k < Lax48.TwinWidth.twinWidth G
28
29	end Lax48.ExponentialSeparation
30

Lax Lean Archive

Submission versions

Twin-Width Can Be Exponential in Treewidth

Settings

Your comments