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.

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

H. L. Bodlaender, "A linear-time algorithm for finding tree-decompositions of small treewidth", SIAM Journal on Computing 25 (1996) 1305–1317; T. Kloks, "Treewidth: Computations and Approximations", Lecture Notes in Computer Science 842, Springer 1994. A simplified presentation of the whole algorithm is E. Althaus and S. Ziegler, "Optimal tree decompositions revisited: a simpler linear-time FPT algorithm", arXiv:1912.09144 (2020).

The formalized algorithm inserts vertices one at a time, adding each new vertex to every bag of the preceding decomposition and applying the characteristic dynamic program to recover width at most $k$. Compression controls the size of intermediate decompositions. This gives a polynomial dependence on the encoded graph length. The exported improvement theorem is derived from this graph algorithm.