Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Nice tree decompositions of small width are found in fixed-parameter time

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

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Bodlaender's theorem. For every constant kk one can decide in linear time whether a graph has treewidth at most kk, and if so construct a tree decomposition of width at most kk; the dependence on kk is 2O(k3)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 algorithm reduces to a graph with a constant fraction fewer vertices — either by contracting a maximal matching among the low-degree vertices, or by removing the "I-simplicial" vertices of the graph with the edges added between vertices that have k+1k+1 common low-degree neighbours — solves that recursively, lifts the answer to a decomposition of width at most 2k+12k+1, and hands that to BodlaenderKloks.improveDecompositionBodlaenderKloks.improveDecomposition.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.GraphWords
    2import Lax808846.Ram
    3
    4/-!
    5---
    6title: Nice tree decompositions of small width are found in fixed-parameter time
    7type: theorem
    8---
    9**Bodlaender's theorem.** For every constant kk one can decide in linear time whether a graph
    10has treewidth at most kk, and if so construct a tree decomposition of width at most kk; the
    11dependence on kk is 2O(k3)2^{O(k^3)}. Kloks' construction turns a tree decomposition into a nice
    12one of the same width in time linear in its size, so the same holds for nice decompositions.
    13
    14H. L. Bodlaender, *"A linear-time algorithm for finding tree-decompositions of small
    15treewidth"*, SIAM Journal on Computing 25 (1996) 1305–1317; T. Kloks, *"Treewidth: Computations
    16and Approximations"*, Lecture Notes in Computer Science 842, Springer 1994. A simplified
    17presentation of the whole algorithm is E. Althaus and S. Ziegler, *"Optimal tree decompositions
    18revisited: a simpler linear-time FPT algorithm"*, arXiv:1912.09144 (2020).
    19
    20The algorithm reduces to a graph with a constant fraction fewer vertices — either by contracting
    21a maximal matching among the low-degree vertices, or by removing the "I-simplicial" vertices of
    22the graph with the edges added between vertices that have k+1k+1 common low-degree neighbours —
    23solves that recursively, lifts the answer to a decomposition of width at most 2k+12k+1, and hands
    24that to `BodlaenderKloks.improveDecomposition`.
    25
    26# Formalization notes
    27
    28The input is the word of the graph (see `GraphWords`) followed by the bound `k`. The output is
    29either `[0]`, admissible only when the graph has no tree decomposition of width at most `k` (in
    30the archive's sense), or `1` followed by the word of a nice tree decomposition of width at most
    31`k`. The output is a relation and not a function, since a graph has many decompositions: the
    32program may produce any one of them.
    33
    34The bound is `c * 2 ^ (c * k ^ 3) * (|g| + 2) ^ c`: the paper's is linear in the number of
    35vertices, while the input has length quadratic in it, and the statement is polynomial in the
    36length of the word, which is what a consumer needs. The guard on the word length is what makes
    37the statement true: the program's tables have size `2 ^ (c * k ^ 3)` times a polynomial in the
    38length of the word, so a machine of too small a word length cannot hold them; the hypothesis is
    39an explicit inequality against `2 ^ W`, checkable from the input alone, and it ranges over the
    40entries of the word so that every entry, and every number the output contains (node numbers are
    41bounded by the running time), is a word. Nothing is claimed for word lengths that violate it.
    42
    43The program and the constant are quantified before the word length, the graph and the bound,
    44so one program serves them all.
    45-/
    46
    47namespace Lax117284.BodlaenderGeneral
    48
    49open Lax808846.Ram Lax117284.GraphWords
    50
    51open Classical in
    52/-- **Bodlaender's theorem with Kloks' niceness, on a word RAM.** One program and one constant
    53serve every word length `W`, every graph `G` on `n` vertices and every bound `k`, provided the
    54word — the graph followed by `k` — fits with room for `c * 2 ^ (c * k ^ 3)` times a polynomial
    55in its length. On such a word the program halts within `c * 2 ^ (c * k ^ 3) * (|g| + 2) ^ c`
    56instructions, writing `[0]` if the graph has no tree decomposition of width at most `k`, and `1`
    57followed by the word of a nice tree decomposition of width at most `k` otherwise. -/
    58axiom niceDecomposition_computable :
    59 ∃ (prog : Program) (c : ℕ), ∀ (W k n : ℕ) (G : SimpleGraph (Fin n)) (g : List ℕ),
    60 EncodesGraph g G →
    61 (∀ v ∈ g ++ [k], c * 2 ^ (c * k ^ 3) * ((g ++ [k]).length + v + 1) ^ c ≤ 2 ^ W) →
    62 ∃ (out : List ℕ) (t : ℕ), t ≤ c * 2 ^ (c * k ^ 3) * (g.length + 2) ^ c ∧
    63 RunsTo W prog (g ++ [k]) out t ∧
    64 (out = [0] ∧ ¬ Lax228581.Treewidth.HasTreewidthAtMost G k ∨
    65 ∃ D, out = 1 :: D ∧ NiceDecomposition G k D)
    66
    67end Lax117284.BodlaenderGeneral
    68
    Show Proof
    Formalization notes

    The input is the word of the graph (see GraphWordsGraphWords) followed by the bound kk. The output is either [0][0], admissible only when the graph has no tree decomposition of width at most kk (in the archive's sense), or 11 followed by the word of a nice tree decomposition of width at most kk. The output is a relation and not a function, since a graph has many decompositions: the program may produce any one of them.

    The bound is c∗2(c∗k3)∗(∣g∣+2)cc * 2 ^ (c * k ^ 3) * (|g| + 2) ^ c: the paper's is linear in the number of vertices, while the input has length quadratic in it, and the statement is polynomial in the length of the word, which is what a consumer needs. The guard on the word length is what makes the statement true: the program's tables have size 2(c∗k3)2 ^ (c * k ^ 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 2W2 ^ 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…