Documentation

LeanPool.PaperIVCliqueTree.TreeDecomposition

From clique forests to tree decompositions #

The adapter preserves every original bag and gives the added connector an empty bag. Nodes containing a vertex still connect through that vertex's original top node; they never need to pass through the connector. In particular, joining several roots does not increase the maximal bag size or the width.

The target interface fixes its node universe to Type, so the adapter uses finite node types in that universe. Graph vertices may live in any universe.

source
def SimpleGraph.CliqueTree.connectorBag {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) :
Option ι → Finset V

Extend the original bags by an empty bag at the connector.

Equations
Instances For
    source
    def SimpleGraph.CliqueTree.vertexBagGraph {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) (v : V) :
    SimpleGraph { x : Option ι // v ∈ T.connectorBag x }

    The subtree induced by bags containing a fixed vertex.

    Equations
    Instances For
      source
      theorem SimpleGraph.CliqueTree.vertexBagGraph_reachable_top {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) (v : V) (i : ι) (hi : v ∈ T.bag i) :
      (T.vertexBagGraph v).Reachable ⟨some i, hi⟩ ⟨some (T.top v), ⋯⟩

      Every bag containing a vertex reaches its original top bag without leaving the induced graph of bags containing that vertex.

      source
      theorem SimpleGraph.CliqueTree.vertexBagGraph_connected {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) (v : V) :
      (T.vertexBagGraph v).Connected

      Vertex-bag coherence survives joining roots with an empty connector bag.

      source
      noncomputable def SimpleGraph.CliqueTree.toTreeDecomposition {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) [Fintype ι] :
      Utilities.Treewidth.TreeDecomposition G

      Convert a finite rooted clique forest into the existing tree-decomposition interface, preserving original bags and adding only an empty connector bag.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem SimpleGraph.CliqueTree.toTreeDecomposition_bag_none {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) [Fintype ι] :
        T.toTreeDecomposition.bag none = ∅

        The connector contributes no vertices to a bag.

        source
        @[simp]
        theorem SimpleGraph.CliqueTree.toTreeDecomposition_bag_some {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) [Fintype ι] (i : ι) :
        T.toTreeDecomposition.bag (some i) = T.bag i

        Each original bag is unchanged by the adapter.

        source
        theorem SimpleGraph.CliqueTree.toTreeDecomposition_max_bag_card {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) [Fintype ι] :
        (Finset.univ.sup fun (x : T.toTreeDecomposition.Node) => (T.toTreeDecomposition.bag x).card) = Finset.univ.sup fun (i : ι) => (T.bag i).card

        The maximum bag size is unchanged, including the empty-index case.

        source
        theorem SimpleGraph.CliqueTree.toTreeDecomposition_width {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) [Fintype ι] :
        T.toTreeDecomposition.width = (Finset.univ.sup fun (i : ι) => (T.bag i).card) - 1

        The adapter has exactly the original maximum bag size minus one.

        source
        theorem SimpleGraph.CliqueTree.treewidth_le_max_bag_card_sub_one {V : Type u_1} {ι : Type} {G : SimpleGraph V} (T : G.CliqueTree ι) [Fintype ι] :
        Utilities.Treewidth.treewidth G ≤ (Finset.univ.sup fun (i : ι) => (T.bag i).card) - 1

        A clique forest directly supplies a treewidth bound through the existing API.