Maximum adjacency orderings

For a weighted multigraph W : V → V → ℕ (Cslib.WeightedCut.IsMultigraph), the attachment weight w(A, x) = ∑_{a ∈ A} W a x measures how strongly a vertex x is joined to a vertex set A. A maximum adjacency (MA) ordering lists the vertices so that each vertex is attached to the vertices before it at least as strongly as every later vertex is. Maximum adjacency search builds one greedily: starting from the empty set, it repeatedly adds a vertex of largest attachment.

The basic property of these orderings, due to Nagamochi and Ibaraki [NI92] and the key lemma of the Stoer–Wagner minimum cut algorithm [SW97] (the "cut-of-the-phase" lemma), is that the cut {t} of the last vertex t is a minimum cut separating t from the second to last vertex s: it weighs at most every vertex set containing exactly one of s and t. The global minimum cut algorithm built on it is CslibFrontier.Algorithms.Lean.StoerWagner.Basic.

The proof is an induction along the ordering. Fix a cut C. For the set A of vertices listed so far, the weight of C within A is the weight of the edges of A crossing C; whenever the next listed vertex is on the other side of C from the last listed one, its attachment to its own side of A is at most the weight of C within A. The last vertex t is such a vertex for every C separating s and t, and its attachment to A = all other vertices is its degree, the weight of {t}. This is the standard inductive argument for the lemma (as described in secondary accounts of [SW97]), phrased as an invariant of the prefixes.

Main definitions

• Cslib.WeightedCut.attachWeight: the attachment weight w(A, x).
• Cslib.WeightedCut.IsMAOrderingFrom, Cslib.WeightedCut.IsMAOrdering: maximum adjacency orderings after a set of already chosen vertices, and of all the vertices.
• Cslib.WeightedCut.maSearch: maximum adjacency search, ties broken by the order of the candidate list.

Main results

• Cslib.WeightedCut.cutWeight_singleton_le_of_isMAOrdering: the MA-ordering lemma.
• Cslib.WeightedCut.cutWeight_singleton_eq_minCutBetween_of_isMAOrdering: the same, as cutWeight W {t} = minCutBetween W s t.
• Cslib.WeightedCut.maSearch_spec: maximum adjacency search lists its candidates in a maximum adjacency ordering.

References

• H. Nagamochi and T. Ibaraki, Computing Edge-Connectivity in Multigraphs and Capacitated Graphs
• M. Stoer and F. Wagner, A Simple Min-Cut Algorithm

Attachment weights and maximum adjacency orderings

def Cslib.WeightedCut.attachWeight {V : Type u_1} (W : V → V → ℕ) (A : Finset V) (x : V) : ℕ

The attachment weight w(A, x) = ∑_{a ∈ A} W a x of a vertex x to a vertex set A.

theorem Cslib.WeightedCut.attachWeight_mono {V : Type u_1} (W : V → V → ℕ) {A B : Finset V} (h : A ⊆ B) (x : V) : attachWeight W A x ≤ attachWeight W B x

@[simp]

theorem Cslib.WeightedCut.attachWeight_empty {V : Type u_1} (W : V → V → ℕ) (x : V) : attachWeight W ∅ x = 0

theorem Cslib.WeightedCut.attachWeight_insert {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) {A : Finset V} {a : V} (ha : a ∉ A) (x : V) : attachWeight W (insert a A) x = W a x + attachWeight W A x

def Cslib.WeightedCut.IsMAOrderingFrom {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) : Finset V → List V → Prop

IsMAOrderingFrom W A l: listing l after the already chosen vertices A, each vertex is attached to the vertices chosen before it at least as strongly as every later vertex.

@[simp]

theorem Cslib.WeightedCut.isMAOrderingFrom_nil {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (A : Finset V) : IsMAOrderingFrom W A []

@[simp]

theorem Cslib.WeightedCut.isMAOrderingFrom_cons {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (A : Finset V) (x : V) (l : List V) : IsMAOrderingFrom W A (x :: l) ↔ (∀ y ∈ l, attachWeight W A y ≤ attachWeight W A x) ∧ IsMAOrderingFrom W (insert x A) l

@[instance_reducible]

instance Cslib.WeightedCut.decidableIsMAOrderingFrom {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (A : Finset V) (l : List V) : Decidable (IsMAOrderingFrom W A l)

structure Cslib.WeightedCut.IsMAOrdering {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (l : List V) : Prop

A maximum adjacency ordering of the vertices: a list of all the vertices, each once, in which each vertex is attached to the vertices before it at least as strongly as every later vertex is. The first vertex is arbitrary.

• nodup : l.Nodup

  No vertex is listed twice.

• mem (v : V) : v ∈ l

  Every vertex is listed.

• isMAOrderingFrom : IsMAOrderingFrom W ∅ l

  The maximum adjacency property.

theorem Cslib.WeightedCut.isMAOrdering_iff {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (l : List V) : IsMAOrdering W l ↔ l.Nodup ∧ (∀ (v : V), v ∈ l) ∧ IsMAOrderingFrom W ∅ l

@[instance_reducible]

instance Cslib.WeightedCut.instDecidableIsMAOrdering {V : Type u_1} [DecidableEq V] [Fintype V] (W : V → V → ℕ) (l : List V) : Decidable (IsMAOrdering W l)

The MA-ordering lemma

theorem Cslib.WeightedCut.cutWeight_singleton_le_of_isMAOrdering {V : Type u_1} [DecidableEq V] [Fintype V] {W : V → V → ℕ} (hW : IsMultigraph W) {p : List V} {s t : V} (hl : IsMAOrdering W (p ++ [s, t])) {C : Finset V} (hsep : s ∈ C ↔ t ∉ C) : cutWeight W {t} ≤ cutWeight W C

The MA-ordering lemma ([NI92]; the "cut-of-the-phase" lemma of [SW97]): if s, t are the last two vertices of a maximum adjacency ordering, the cut {t} weighs at most every vertex set containing exactly one of s and t.

theorem Cslib.WeightedCut.cutWeight_singleton_eq_minCutBetween_of_isMAOrdering {V : Type u_1} [DecidableEq V] [Fintype V] {W : V → V → ℕ} (hW : IsMultigraph W) {p : List V} {s t : V} (hl : IsMAOrdering W (p ++ [s, t])) : cutWeight W {t} = minCutBetween W s t

The MA-ordering lemma in terms of the minimum s–t cut weight λ(s, t) (Cslib.WeightedCut.minCutBetween): if s, t are the last two vertices of a maximum adjacency ordering, the cut {t} weighs exactly λ(s, t).

Maximum adjacency search

def Cslib.WeightedCut.maSearch {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) : ℕ → (V → ℕ) → List V → List V

Maximum adjacency search. With key y = w(A, y) for the vertices A chosen so far, it lists a candidate of largest key (the first one in the list R of remaining candidates, by List.argmax), adds its edge weights to the keys, and continues with the other candidates. fuel bounds the number of steps, so that the recursion is structural and reduces in the kernel.

theorem Cslib.WeightedCut.maSearch_spec {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (fuel : ℕ) (key : V → ℕ) (A : Finset V) (R : List V) : R.Nodup → R.length ≤ fuel → (∀ (y : V), key y = attachWeight W A y) → (∀ y ∈ R, y ∉ A) → (maSearch W fuel key R).Perm R ∧ IsMAOrderingFrom W A (maSearch W fuel key R)

Maximum adjacency search from the chosen set A, with keys w(A, ·) and enough fuel, lists its candidates in a maximum adjacency ordering after A.