Nice Tree Decompositions of Small Width Are Found in Fixed-Parameter Time

Lax117284.Bodlaender · concepts/Lax117284/Bodlaender.lean · lax-117284

proven

Loading review…

Natural Language Statement

Definition

A tree decomposition of a graph is a tree whose nodes carry bags of vertices such that every vertex and every edge lies in a bag and the nodes whose bags contain a fixed vertex form a connected subtree; its width is the largest bag size minus one. It is nice if its nodes are of four kinds: a leaf, an introduce node whose bag is the bag of its single child plus one vertex, a forget node whose bag is the bag of its single child minus one vertex, and a join node with two children whose bags equal its own.

Bodlaender's theorem. For every constant $w$ one can decide in linear time whether a graph has treewidth at most $w$ , and if so construct a tree decomposition of width at most $w$ ; the dependence on $w$ is $2^{O(w^3)}$ . Kloks' construction turns any tree decomposition of width $w$ into a nice one of the same width in time linear in the size of the decomposition, so the same holds for nice decompositions.

Bodlaender, "A linear-time algorithm for finding tree-decompositions of small treewidth", SIAM Journal on Computing 25 (1996) 1305–1317; Kloks, "Treewidth: Computations and Approximations", Lecture Notes in Computer Science 842, Springer 1994. Cited by Heeger–Hermelin–Itzhaki–Molter–Shabtay for Theorem 4's second bullet.

Concept map

6 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

def✓Lax117284.Bodlaender

⊢Lax117284Proofs.BodlaenderProved.niceDecomposition_computable_proved

In the paper

page 1 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax808846.Ram
2	import Lax117284.InstanceEncoding
3	import Lax117284.ConflictGraph
4
5	/-!
6	---
7	title: Nice Tree Decompositions of Small Width Are Found in Fixed-Parameter Time
8	type: definition
9	---
10	A tree decomposition of a graph is a tree whose nodes carry bags of vertices such that every
11	vertex and every edge lies in a bag and the nodes whose bags contain a fixed vertex form a
12	connected subtree; its width is the largest bag size minus one. It is nice if its nodes are of
13	four kinds: a leaf, an introduce node whose bag is the bag of its single child plus one
14	vertex, a forget node whose bag is the bag of its single child minus one vertex, and a join
15	node with two children whose bags equal its own.
16
17	Bodlaender's theorem. For every constant `w` one can decide in linear time whether a graph
18	has treewidth at most `w`, and if so construct a tree decomposition of width at most `w`; the
19	dependence on `w` is `2^{O(w^3)}`. Kloks' construction turns any tree decomposition of width `w`
20	into a nice one of the same width in time linear in the size of the decomposition, so the same
21	holds for nice decompositions.
22
23	Bodlaender, "A linear-time algorithm for finding tree-decompositions of small treewidth",
24	SIAM Journal on Computing 25 (1996) 1305–1317; Kloks, *"Treewidth: Computations and
25	Approximations"*, Lecture Notes in Computer Science 842, Springer 1994. Cited by
26	Heeger–Hermelin–Itzhaki–Molter–Shabtay for Theorem 4's second bullet.
27
28	# Formalization Notes
29
30	The cited theorem is stated for the graphs this development runs it on: the overall conflict
31	graph of an instance. A word presents that graph as its adjacency matrix: the number `n` of
32	clients, then the `n * n` entries of the matrix row by row, each `1` for adjacent and `0` for not,
33	and the bound `w` on the width is appended as a last entry. Reading the graph off an instance
34	takes time polynomial in the instance, so it is a step of the algorithm that uses the theorem
35	and not of the theorem itself; the running time of the theorem is measured in the length of the
36	graph's word, polynomially, and is `2^{c w^3}` in the bound, which is what the linear-time
37	algorithm takes once the graph is in this form.
38
39	The output is either `[0]`, which is admissible only when the graph has no tree decomposition
40	of width at most `w` (in the archive's sense), or `1` followed by the word of a nice tree
41	decomposition of width at most `w`. A nice decomposition is a word `N` followed by `N` records
42	of three numbers, one for each node in an order in which every node comes after its children: the
43	kind of the node (`0` leaf, `1` introduce, `2` forget, `3` join), a vertex (for introduce and
44	forget nodes) and a node (the second child of a join node). The first child of a non-leaf is the
45	node just before it. Bags are not written: they are determined from the leaves upward, a leaf
46	having the empty bag. `NiceDecomposition` says that this describes a tree, that its bags
47	cover the vertices and the edges, that they are connected as required, and that the bags have at
48	most `w + 1` vertices. It is the archive's tree decomposition written out for words.
49
50	The output is a relation and not a function, since a graph has many decompositions: the program
51	may produce any one of them.
52
53	The guard on the word length is what makes the statement true. The program's tables have size
54	`2^{c w^3}` times a polynomial in the length of the word, so a machine of too small a word length
55	cannot hold them; the hypothesis is an explicit inequality against `2 ^ W`, checkable from the
56	input alone, and it ranges over the entries of the word so that every entry, and every number the
57	output contains (node numbers are bounded by the running time), is a word. Nothing is claimed
58	for word lengths that violate it.
59
60	The program and the constant are quantified before the word length, the graph and the
61	bound, so one program serves them all.
62	-/
63
64	namespace Lax117284.Bodlaender
65
66	open Lax808846.Ram Lax117284.Scheduling Lax117284.ConflictGraph
67
68	-- The word of a decomposition.
69
70	/-- The number of nodes of the decomposition word `D`: its first entry. -/
71	def nodeCount (D : List ℕ) : ℕ := D.getD 0 0
72
73	/-- The kind of node `i`: `0` leaf, `1` introduce, `2` forget, `3` join. -/
74	def kind (D : List ℕ) (i : ℕ) : ℕ := D.getD (1 + 3 * i) 0
75
76	/-- The vertex of node `i`, for an introduce or a forget node. -/
77	def vertex (D : List ℕ) (i : ℕ) : ℕ := D.getD (2 + 3 * i) 0
78
79	/-- The second child of node `i`, for a join node. -/
80	def other (D : List ℕ) (i : ℕ) : ℕ := D.getD (3 + 3 * i) 0
81
82	/-- The bag of node `i` among the vertices `0 … n - 1`, from the leaves up: the empty bag at a
83	leaf, the child's bag plus the vertex at an introduce node, minus it at a forget node, and the
84	child's bag at a join node. The first child of node `i + 1` is node `i`. -/
85	def bagAt (n : ℕ) (D : List ℕ) : ℕ → Finset (Fin n)
86	\| 0 => ∅
87	\| i + 1 =>
88	if kind D (i + 1) = 1 then
89	if h : vertex D (i + 1) < n then insert ⟨vertex D (i + 1), h⟩ (bagAt n D i)
90	else bagAt n D i
91	else if kind D (i + 1) = 2 then
92	if h : vertex D (i + 1) < n then (bagAt n D i).erase ⟨vertex D (i + 1), h⟩
93	else bagAt n D i
94	else if kind D (i + 1) = 3 then bagAt n D i
95	else ∅
96
97	/-- Node `c` is a child of node `p`. -/
98	def IsChild (D : List ℕ) (c p : ℕ) : Prop :=
99	p < nodeCount D ∧
100	((kind D p = 1 ∨ kind D p = 2) ∧ c + 1 = p ∨ kind D p = 3 ∧ (c + 1 = p ∨ c = other D p))
101
102	/-- The graph on the nodes `0 … N - 1` whose edges join a node to its children. -/
103	def treeGraph (D : List ℕ) : SimpleGraph (Fin (nodeCount D)) where
104	Adj a b := a ≠ b ∧ (IsChild D a.val b.val ∨ IsChild D b.val a.val)
105	symm := ⟨fun _ _ h => ⟨h.1.symm, h.2.symm⟩⟩
106	loopless := ⟨fun _ h => h.1 rfl⟩
107
108	/-- **`D` is the word of a nice tree decomposition of the overall conflict graph of `I` of width
109	at most `w`.** -/
110	structure NiceDecomposition (I : Instance) (w : ℕ) (D : List ℕ) : Prop where
111	/-- The word is `N` followed by three numbers for each of the `N` nodes. -/
112	length_eq : D.length = 1 + 3 * nodeCount D
113	/-- There is a node. -/
114	nonempty : 0 < nodeCount D
115	/-- Every node is a leaf, or an introduce node over the node before it whose vertex is not in
116	that node's bag, or a forget node over the node before it whose vertex is in that node's bag,
117	or a join node whose two children, the node before it and an earlier node, have its bag. -/
118	shape : ∀ i, i < nodeCount D →
119	kind D i = 0 ∨
120	(0 < i ∧ kind D i = 1 ∧ vertex D i < I.clients ∧
121	∀ h : vertex D i < I.clients, (⟨vertex D i, h⟩ : Fin I.clients) ∉ bagAt I.clients D (i - 1)) ∨
122	(0 < i ∧ kind D i = 2 ∧ vertex D i < I.clients ∧
123	∀ h : vertex D i < I.clients, (⟨vertex D i, h⟩ : Fin I.clients) ∈ bagAt I.clients D (i - 1)) ∨
124	(0 < i ∧ kind D i = 3 ∧ other D i + 1 < i ∧
125	bagAt I.clients D (other D i) = bagAt I.clients D (i - 1))
126	/-- Every node other than the last has exactly one parent. -/
127	parent : ∀ c, c + 1 < nodeCount D → ∃! p, IsChild D c p
128	/-- The nodes form a tree. -/
129	isTree : (treeGraph D).IsTree
130	/-- Every client is in a bag. -/
131	covers : ∀ v : Fin I.clients, ∃ i, i < nodeCount D ∧ v ∈ bagAt I.clients D i
132	/-- Every two clients whose jobs conflict on some day are in a bag together. -/
133	edges : ∀ u v : Fin I.clients, (overallGraph I).Adj u v →
134	∃ i, i < nodeCount D ∧ u ∈ bagAt I.clients D i ∧ v ∈ bagAt I.clients D i
135	/-- The nodes whose bags contain a fixed client form a connected subtree. -/
136	connected : ∀ v : Fin I.clients,
137	((treeGraph D).induce {i : Fin (nodeCount D) \| v ∈ bagAt I.clients D i}).Connected
138	/-- Every bag has at most `w + 1` clients. -/
139	width : ∀ i, i < nodeCount D → (bagAt I.clients D i).card ≤ w + 1
140
141	open Classical in
142	/-- `g` is the word of the overall conflict graph of `I`: the number of clients, then the
143	adjacency matrix row by row. -/
144	structure EncodesGraph (g : List ℕ) (I : Instance) : Prop where
145	/-- The word is the count followed by the matrix. -/
146	length_eq : g.length = 1 + I.clients * I.clients
147	/-- The first entry is the number of clients. -/
148	head_eq : g.getD 0 0 = I.clients
149	/-- The entry of the row `u` and column `v` is `1` when the two clients are adjacent and `0`
150	otherwise. -/
151	adj_eq : ∀ u v : Fin I.clients,
152	g.getD (1 + u.val * I.clients + v.val) 0 = if (overallGraph I).Adj u v then 1 else 0
153
154	/-- **Bodlaender's theorem with Kloks' niceness, for the overall conflict graph of an instance
155	given as a word.** One program and one constant serve every word length `W`, every graph and every
156	bound `w`, provided the word — the graph followed by `w` — fits with room for
157	`c * 2 ^ (c * w ^ 3)` times a polynomial in its length. On such a word the program halts within
158	`c * 2 ^ (c * w ^ 3) * (\|g\| + 2) ^ c` instructions, writing `[0]` if the graph has no tree
159	decomposition of width at most `w`, and `1` followed by the word of a nice tree decomposition of
160	width at most `w` otherwise. -/
161	axiom niceDecomposition_computable :
162	∃ (prog : Program) (c : ℕ), ∀ (W w : ℕ) (g : List ℕ) (I : Instance),
163	EncodesGraph g I →
164	(∀ v ∈ g ++ [w], c * 2 ^ (c * w ^ 3) * ((g ++ [w]).length + v + 1) ^ c ≤ 2 ^ W) →
165	∃ (out : List ℕ) (t : ℕ), t ≤ c * 2 ^ (c * w ^ 3) * (g.length + 2) ^ c ∧
166	RunsTo W prog (g ++ [w]) out t ∧
167	(out = [0] ∧ ¬ Lax228581.Treewidth.HasTreewidthAtMost (overallGraph I) w ∨
168	∃ D, out = 1 :: D ∧ NiceDecomposition I w D)
169
170	end Lax117284.Bodlaender
171

Show Proof

Formalization Notes

The cited theorem is stated for the graphs this development runs it on: the overall conflict graph of an instance. A word presents that graph as its adjacency matrix: the number $n$ of clients, then the $n * n$ entries of the matrix row by row, each $1$ for adjacent and $0$ for not, and the bound $w$ on the width is appended as a last entry. Reading the graph off an instance takes time polynomial in the instance, so it is a step of the algorithm that uses the theorem and not of the theorem itself; the running time of the theorem is measured in the length of the graph's word, polynomially, and is $2^{c w^3}$ in the bound, which is what the linear-time algorithm takes once the graph is in this form.

The output is either $[0]$ , which is admissible only when the graph has no tree decomposition of width at most $w$ (in the archive's sense), or $1$ followed by the word of a nice tree decomposition of width at most $w$ . A nice decomposition is a word $N$ followed by $N$ records of three numbers, one for each node in an order in which every node comes after its children: the kind of the node ( $0$ leaf, $1$ introduce, $2$ forget, $3$ join), a vertex (for introduce and forget nodes) and a node (the second child of a join node). The first child of a non-leaf is the node just before it. Bags are not written: they are determined from the leaves upward, a leaf having the empty bag. $NiceDecomposition$ says that this describes a tree, that its bags cover the vertices and the edges, that they are connected as required, and that the bags have at most $w + 1$ vertices. It is the archive's tree decomposition written out for words.

The output is a relation and not a function, since a graph has many decompositions: the program may produce any one of them.

The guard on the word length is what makes the statement true. The program's tables have size $2^{c w^3}$ times a polynomial in the length of the word, so a machine of too small a word length cannot hold them; the hypothesis is an explicit inequality against $2 ^ W$ , checkable from the input alone, and it ranges over the entries of the word so that every entry, and every number the output contains (node numbers are bounded by the running time), is a word. Nothing is claimed for word lengths that violate it.

The program and the constant are quantified before the word length, the graph and the bound, so one program serves them all.

Builds on

Used by

none

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Nice Tree Decompositions of Small Width Are Found in Fixed-Parameter Time

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments