Optimal tree decompositions from a given one

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

proven

Loading review…

Natural Language Statement

Theorem

The theorem of Bodlaender and Kloks. For all $k$ and $\ell$ there is a linear-time algorithm that, given a graph together with a tree decomposition of width at most $\ell$ , decides whether the treewidth of the graph is at most $k$ and, if so, finds a tree decomposition of width at most $k$ . The dependence on $\ell$ is $2^{O(\ell^3)}$ .

H. L. Bodlaender and T. Kloks, "Efficient and constructive algorithms for the pathwidth and treewidth of graphs", Journal of Algorithms 21 (1996) 358–402. A simpler presentation, which this module follows, is E. Althaus and S. Ziegler, "Optimal tree decompositions revisited: a simpler linear-time FPT algorithm", arXiv:1912.09144 (2020), §3; the statement is Theorem 2.10 of H. L. Bodlaender, "A linear-time algorithm for finding tree-decompositions of small treewidth", SIAM Journal on Computing 25 (1996) 1305–1317, where it is used as a black box.

This is the second stage of Bodlaender's algorithm, $BodlaenderGeneral.niceDecomposition_computable$ being the first: the latter builds the decomposition of width at most $2k+1$ this one consumes.

Concept map

4 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax117284.BodlaenderKloks

⊢Lax117284Proofs.Treewidth.Fun.Final.improveDecomposition_proved

In the paper

page 5 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax117284.GraphWords
2	import Lax808846.Ram
3
4	/-!
5	---
6	title: Optimal tree decompositions from a given one
7	type: theorem
8	---
9	The theorem of Bodlaender and Kloks. For all $k$ and $\ell$ there is a linear-time
10	algorithm that, given a graph together with a tree decomposition of width at most $\ell$ ,
11	decides whether the treewidth of the graph is at most $k$ and, if so, finds a tree
12	decomposition of width at most $k$ . The dependence on $\ell$ is $2^{O(\ell^3)}$ .
13
14	H. L. Bodlaender and T. Kloks, *"Efficient and constructive algorithms for the pathwidth and
15	treewidth of graphs"*, Journal of Algorithms 21 (1996) 358–402. A simpler presentation, which
16	this module follows, is E. Althaus and S. Ziegler, *"Optimal tree decompositions revisited:
17	a simpler linear-time FPT algorithm"*, arXiv:1912.09144 (2020), §3; the statement is Theorem
18	2.10 of H. L. Bodlaender, *"A linear-time algorithm for finding tree-decompositions of small
19	treewidth"*, SIAM Journal on Computing 25 (1996) 1305–1317, where it is used as a black box.
20
21	This is the second stage of Bodlaender's algorithm, `BodlaenderGeneral.niceDecomposition_computable`
22	being the first: the latter builds the decomposition of width at most $2k+1$ this one
23	consumes.
24
25	# Formalization notes
26
27	The input is one word: the graph (see `GraphWords`), the two numbers `k` and `l`, and the word
28	of a nice tree decomposition of width at most `l`. The graph word states its own length, so the
29	three parts are told apart. The given decomposition is nice; Althaus and Ziegler assume it and
30	the conversion of an arbitrary decomposition into a nice one of the same width takes time
31	$O(\ell^2(\|V(T)\| + \|V\|))$ (Kloks), so nothing is lost.
32
33	The output is either `[0]`, admissible only when the graph has no tree decomposition of width
34	at most `k`, or `1` followed by the word of a nice tree decomposition of width at most `k`. It
35	is a relation rather than a function: a graph has many decompositions, and the program may
36	produce any one of them. The output is nice, where the theorem produces an arbitrary
37	decomposition, because the conversion is one more linear-time pass and every consumer wants
38	the nice form.
39
40	The bound is `c * 2 ^ (c * l ^ 3) * (\|input\| + 2) ^ c`. The paper's is linear in the number of
41	vertices; on a word RAM given the adjacency matrix the input has length quadratic in the number
42	of vertices, and the statement is polynomial in it, which is all a consumer needs. The
43	condition on the word length is an explicit inequality against `2 ^ W`, on every entry of the
44	input: the tables of the algorithm have size `2 ^ (c * l ^ 3)` times a polynomial in the length,
45	so a machine of too small a word length cannot hold them.
46
47	The program and the constant are quantified before the word length, the graph and the two
48	bounds, so one program serves all of them.
49	-/
50
51	namespace Lax117284.BodlaenderKloks
52
53	open Lax808846.Ram Lax117284.GraphWords
54
55	open Classical in
56	/-- The theorem of Bodlaender and Kloks, on a word RAM. One program and one constant serve
57	every word length `W`, every graph `G`, every bound `k` and every nice tree decomposition `D` of
58	`G` of width at most `l`, provided the input `g ++ [k, l] ++ D` fits with room for
59	`c * 2 ^ (c * l ^ 3)` times a polynomial in its length. On such an input the program halts
60	within `c * 2 ^ (c * l ^ 3) * (\|input\| + 2) ^ c` instructions, writing `[0]` if the graph has no
61	tree decomposition of width at most `k`, and `1` followed by the word of a nice tree
62	decomposition of width at most `k` otherwise. -/
63	axiom improveDecomposition :
64	∃ (prog : Program) (c : ℕ), ∀ (W k l : ℕ) (n : ℕ) (G : SimpleGraph (Fin n)) (g D : List ℕ),
65	EncodesGraph g G → NiceDecomposition G l D →
66	(∀ v ∈ g ++ [k, l] ++ D,
67	c * 2 ^ (c * l ^ 3) * ((g ++ [k, l] ++ D).length + v + 1) ^ c ≤ 2 ^ W) →
68	∃ (out : List ℕ) (t : ℕ), t ≤ c * 2 ^ (c * l ^ 3) * ((g ++ [k, l] ++ D).length + 2) ^ c ∧
69	RunsTo W prog (g ++ [k, l] ++ D) out t ∧
70	(out = [0] ∧ ¬ Lax228581.Treewidth.HasTreewidthAtMost G k ∨
71	∃ D', out = 1 :: D' ∧ NiceDecomposition G k D')
72
73	end Lax117284.BodlaenderKloks
74

Show Proof

Formalization notes

The input is one word: the graph (see $GraphWords$ ), the two numbers $k$ and $l$ , and the word of a nice tree decomposition of width at most $l$ . The graph word states its own length, so the three parts are told apart. The given decomposition is nice; Althaus and Ziegler assume it and the conversion of an arbitrary decomposition into a nice one of the same width takes time $O(\ell^2(|V(T)| + |V|))$ (Kloks), so nothing is lost.

The output is either $[0]$ , admissible only when the graph has no tree decomposition of width at most $k$ , or $1$ followed by the word of a nice tree decomposition of width at most $k$ . It is a relation rather than a function: a graph has many decompositions, and the program may produce any one of them. The output is nice, where the theorem produces an arbitrary decomposition, because the conversion is one more linear-time pass and every consumer wants the nice form.

The bound is $c * 2 ^ (c * l ^ 3) * (|input| + 2) ^ c$ . The paper's is linear in the number of vertices; on a word RAM given the adjacency matrix the input has length quadratic in the number of vertices, and the statement is polynomial in it, which is all a consumer needs. The condition on the word length is an explicit inequality against $2 ^ W$ , on every entry of the input: the tables of the algorithm have size $2 ^ (c * l ^ 3)$ times a polynomial in the length, so a machine of too small a word length cannot hold them.

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

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

Optimal tree decompositions from a given one

Flags

Flag this concept

Natural Language Statement

Theorem

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments