Optimal Tree Decompositions from a Given One

Lax689794.BodlaenderKloks · concepts/Lax689794/BodlaenderKloks.lean · lax-689794

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.

The formalized improvement result is derived from the exact graph algorithm. When $l ≤ k$ , the program returns the supplied decomposition; otherwise it runs the graph algorithm with bound $k$ . Since $k < l$ in the latter case, its parameter-dependent bound is also bounded in terms of $l$ . The underlying characteristic dynamic program is used within the graph algorithm's vertex-by-vertex construction.

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✓Lax689794.BodlaenderKloks

⊢Lax689794Proofs.Fun.Final.improveDecomposition_proved

In the paper

page 2 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax689794.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	The formalized improvement result is derived from the exact graph algorithm. When `l ≤ k`,
22	the program returns the supplied decomposition; otherwise it runs the graph algorithm with
23	bound `k`. Since `k < l` in the latter case, its parameter-dependent bound is also bounded
24	in terms of `l`. The underlying characteristic dynamic program is used within the graph
25	algorithm's vertex-by-vertex construction.
26
27	# Formalization Notes
28
29	The input is one word: the graph (see `GraphWords`), the two numbers `k` and `l`, and the word
30	of a nice tree decomposition of width at most `l`. The graph word states its own length, so the
31	three parts are told apart. The given decomposition is nice; Althaus and Ziegler assume it and
32	the conversion of an arbitrary decomposition into a nice one of the same width takes time
33	$O(\ell^2(\|V(T)\| + \|V\|))$ (Kloks), so nothing is lost.
34
35	The output is either `[0]`, admissible only when the graph has no tree decomposition of width
36	at most `k`, or `1` followed by the word of a nice tree decomposition of width at most `k`. It
37	is a relation rather than a function: a graph has many decompositions, and the program may
38	produce any one of them. The output is nice, where the theorem produces an arbitrary
39	decomposition, because the conversion is one more linear-time pass and every consumer wants
40	the nice form.
41
42	The bound is `c * 2 ^ (c * l ^ 3) * (\|input\| + 2) ^ c`. The polynomial factor uses the full encoded input length, including the supplied decomposition.
43	Only the graph portion has length quadratic in the number of vertices; no size bound on the
44	supplied decomposition is assumed. The
45	condition on the word length is an explicit inequality against `2 ^ W`, on every entry of the
46	input: the tables of the algorithm have size `2 ^ (c * l ^ 3)` times a polynomial in the length,
47	so a machine of too small a word length cannot hold them.
48
49	The program and the constant are quantified before the word length, the graph and the two
50	bounds, so one program serves all of them.
51	-/
52
53	namespace Lax689794.BodlaenderKloks
54
55	open Lax808846.Ram Lax689794.GraphWords
56
57	open Classical in
58	/-- The theorem of Bodlaender and Kloks, on a word RAM. One program and one constant serve
59	every word length `W`, every graph `G`, every bound `k` and every nice tree decomposition `D` of
60	`G` of width at most `l`, provided the input `g ++ [k, l] ++ D` fits with room for
61	`c * 2 ^ (c * l ^ 3)` times a polynomial in its length. On such an input the program halts
62	within `c * 2 ^ (c * l ^ 3) * (\|input\| + 2) ^ c` instructions, writing `[0]` if the graph has no
63	tree decomposition of width at most `k`, and `1` followed by the word of a nice tree
64	decomposition of width at most `k` otherwise. -/
65	axiom improveDecomposition :
66	∃ (prog : Program) (c : ℕ), ∀ (W k l : ℕ) (n : ℕ) (G : SimpleGraph (Fin n)) (g D : List ℕ),
67	EncodesGraph g G → NiceDecomposition G l D →
68	(∀ v ∈ g ++ [k, l] ++ D,
69	c * 2 ^ (c * l ^ 3) * ((g ++ [k, l] ++ D).length + v + 1) ^ c ≤ 2 ^ W) →
70	∃ (out : List ℕ) (t : ℕ), t ≤ c * 2 ^ (c * l ^ 3) * ((g ++ [k, l] ++ D).length + 2) ^ c ∧
71	RunsTo W prog (g ++ [k, l] ++ D) out t ∧
72	(out = [0] ∧ ¬ Lax228581.Treewidth.HasTreewidthAtMost G k ∨
73	∃ D', out = 1 :: D' ∧ NiceDecomposition G k D')
74
75	end Lax689794.BodlaenderKloks
76

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 polynomial factor uses the full encoded input length, including the supplied decomposition. Only the graph portion has length quadratic in the number of vertices; no size bound on the supplied decomposition is assumed. 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