Proof of `Optimal Tree Decompositions from a Given One`

groundedproofs/Lax689794Proofs/Fun/Final.lean · lax-689794

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 2 of this submission's paper

Description

The improvement step of Bodlaender–Kloks on a word RAM: given a nice decomposition of width ℓℓ it returns one of width at most kk or [0][0], proved by a dispatcher over the same exact algorithm (if ℓ≤kℓ ≤ k the given decomposition is returned; otherwise the main algorithm runs on the graph and kk).