Gonzalez's farthest-first traversal for k-center

Gonzalez's algorithm picks a first center and then, k - 1 times, adds a point farthest from the centers chosen so far ([Gon85]; [WS11], Algorithm 2.1). On a symmetric distance with the triangle inequality its radius is at most twice the optimal k-center radius ([WS11], Theorem 2.3). The factor 2 cannot be improved in polynomial time unless P = NP: the combinatorial core of that hardness result is CslibFrontier.Algorithms.Lean.KCenter.DominatingSet, and the statement on encoded instances is Cslib.Complexity.P_eq_NP_of_kCenter_approx.

Algorithm and source mapping

gonzalez d P k runs k rounds of farthestStep d P from no centers. A round appends a point of the list P maximizing the distance centerDist to the current centers, the first such point in the order of P (List.argmax). In the first round every point is at distance ⊤ from no centers, so the first center is the first point of P; Algorithm 2.1 picks it arbitrarily. The algorithm is total: it returns k centers whenever P is nonempty (length_gonzalez), and the loop "while |S| < k" of Algorithm 2.1 becomes a fixed number of rounds. Under a distance that vanishes exactly on the diagonal the centers are distinct (nodup_gonzalez).

The analysis is stated for every farthest-first traversal (IsFarthestFirst), whatever its first center and tie-breaking. It follows the pigeonhole form of the argument of Theorem 2.3: if a point v were farther than 2 r from all k centers, then the centers followed by v would be k + 1 points pairwise farther than 2 r apart (IsFarthestFirst.pairwise_lt), because each center was at least as far from the earlier centers as v is; but at most k centers covering within r cannot cover such points (length_le_card_of_pairwise_lt). Williamson and Shmoys phrase the same argument through the clusters of an optimal solution.

Limitations

The algorithm is a pure Lean function; no machine-level running time is certified. The competing centers C in centerDist_gonzalez_le_two_mul are arbitrary points of the space, not only points of P. The alternative threshold 2-approximation of [HS85] (see the chapter notes of [WS11], Chapter 2) is not formalized.

Main definitions

• Cslib.Algorithms.Lean.KCenter.IsFarthestFirst: a farthest-first traversal of a list of points.
• Cslib.Algorithms.Lean.KCenter.farthestStep: add a farthest point to the centers.
• Cslib.Algorithms.Lean.KCenter.gonzalez: Gonzalez's algorithm with k centers.

Main results

• isFarthestFirst_gonzalez, mem_of_mem_gonzalez, length_gonzalez, length_gonzalez_le, card_toFinset_gonzalez_le: Gonzalez's algorithm is a farthest-first traversal of at most k points of P, exactly k when P is nonempty.
• nodup_gonzalez, card_toFinset_gonzalez: under a distance vanishing exactly on the diagonal the centers are k distinct points when P has at least k distinct points.
• IsFarthestFirst.pairwise_lt: separation of a farthest-first traversal.
• IsFarthestFirst.centerDist_le_two_mul, centerDist_gonzalez_le_two_mul: every point of P is within 2 r of the centers when some k centers cover P within r.
• radius_gonzalez_le_two_mul, radius_gonzalez_le_two_mul_radius, radius_gonzalez_le_two_mul_optRadius: on a finite space the radius is at most twice the optimum, and at most twice the radius of every set of at most k centers.

References

• T. F. Gonzalez, Clustering to minimize the maximum intercluster distance
• D. S. Hochbaum and D. B. Shmoys, A best possible heuristic for the k-center problem
• D. P. Williamson and D. B. Shmoys, The Design of Approximation Algorithms, Section 2.2.

The algorithm

inductive Cslib.Algorithms.Lean.KCenter.IsFarthestFirst {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P : List V) : List V → Prop

IsFarthestFirst d P L says that the list L of centers is a farthest-first traversal of the points P: every center is a point of P that, among the points of P, is farthest from the centers before it. The first center is therefore an arbitrary point of P.

• nil {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} : IsFarthestFirst d P []

  No centers.

• snoc {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P L : List V} {x : V} : IsFarthestFirst d P L → x ∈ P → (∀ y ∈ P, centerDist d L.toFinset y ≤ centerDist d L.toFinset x) → IsFarthestFirst d P (L ++ [x])

  Append a point of P farthest from the current centers.

theorem Cslib.Algorithms.Lean.KCenter.IsFarthestFirst.subset {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P L : List V} (h : IsFarthestFirst d P L) (x : V) : x ∈ L → x ∈ P

The centers of a farthest-first traversal are points of P.

def Cslib.Algorithms.Lean.KCenter.farthestStep {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P L : List V) : List V

One round of the farthest-first traversal: append a point of P farthest from the current centers, the first such point in the order of P. Nothing is appended when P is empty.

def Cslib.Algorithms.Lean.KCenter.gonzalez {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P : List V) (k : ℕ) : List V

Gonzalez's algorithm ([Gon85]; [WS11], Algorithm 2.1): k rounds of the farthest-first traversal from no centers. The first round picks the first point of P.

theorem Cslib.Algorithms.Lean.KCenter.gonzalez_zero {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P : List V) : gonzalez d P 0 = []

theorem Cslib.Algorithms.Lean.KCenter.gonzalez_succ {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P : List V) (k : ℕ) : gonzalez d P (k + 1) = farthestStep d P (gonzalez d P k)

theorem Cslib.Algorithms.Lean.KCenter.IsFarthestFirst.farthestStep {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P L : List V} (h : IsFarthestFirst d P L) : IsFarthestFirst d P (KCenter.farthestStep d P L)

theorem Cslib.Algorithms.Lean.KCenter.isFarthestFirst_gonzalez {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P : List V) (k : ℕ) : IsFarthestFirst d P (gonzalez d P k)

Gonzalez's algorithm computes a farthest-first traversal.

theorem Cslib.Algorithms.Lean.KCenter.length_farthestStep {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} (hP : P ≠ []) (L : List V) : (farthestStep d P L).length = L.length + 1

theorem Cslib.Algorithms.Lean.KCenter.length_gonzalez {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} (hP : P ≠ []) (k : ℕ) : (gonzalez d P k).length = k

On a nonempty list of points, Gonzalez's algorithm chooses exactly k centers. Repetitions occur only when the distance vanishes between distinct points or k exceeds the number of distinct points of P; see nodup_gonzalez.

@[simp]

theorem Cslib.Algorithms.Lean.KCenter.gonzalez_nil {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (k : ℕ) : gonzalez d [] k = []

theorem Cslib.Algorithms.Lean.KCenter.mem_of_mem_gonzalez {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} {k : ℕ} {x : V} (hx : x ∈ gonzalez d P k) : x ∈ P

The centers are points of P.

theorem Cslib.Algorithms.Lean.KCenter.length_gonzalez_le {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P : List V) (k : ℕ) : (gonzalez d P k).length ≤ k

theorem Cslib.Algorithms.Lean.KCenter.card_toFinset_gonzalez_le {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] (d : V → V → α) (P : List V) (k : ℕ) : (gonzalez d P k).toFinset.card ≤ k

Feasibility: Gonzalez's algorithm chooses at most k centers.

theorem Cslib.Algorithms.Lean.KCenter.nodup_gonzalez {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} [Zero α] (hself : ∀ (x : V), d x x = 0) (hpos : ∀ (x y : V), x ≠ y → 0 < d x y) {k : ℕ} (hk : k ≤ P.toFinset.card) : (gonzalez d P k).Nodup

The centers are distinct under a distance that vanishes exactly on the diagonal, as long as P has at least k distinct points: when a round would repeat a center, every point of P is at distance 0 from the centers, hence is one of them.

theorem Cslib.Algorithms.Lean.KCenter.card_toFinset_gonzalez {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} [Zero α] (hself : ∀ (x : V), d x x = 0) (hpos : ∀ (x y : V), x ≠ y → 0 < d x y) {k : ℕ} (hk : k ≤ P.toFinset.card) : (gonzalez d P k).toFinset.card = k

Under a distance that vanishes exactly on the diagonal, Gonzalez's algorithm chooses exactly k distinct centers when P has at least k distinct points.

The 2-approximation

theorem Cslib.Algorithms.Lean.KCenter.IsFarthestFirst.pairwise_lt {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P L : List V} (h : IsFarthestFirst d P L) (hsymm : ∀ (x y : V), d x y = d y x) {v : V} {r : α} (hv : v ∈ P) (hr : ↑r < centerDist d L.toFinset v) : List.Pairwise (fun (a b : V) => r < d a b) (L ++ [v])

Separation of a farthest-first traversal. If a point v of P is farther than r from every center of a farthest-first traversal L, then the centers of L followed by v are pairwise farther than r apart: each center was at least as far from the earlier centers as v is from them.

theorem Cslib.Algorithms.Lean.KCenter.IsFarthestFirst.centerDist_le_two_mul {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} [Semiring α] [IsOrderedAddMonoid α] {L : List V} (h : IsFarthestFirst d P L) (hsymm : ∀ (x y : V), d x y = d y x) (htri : ∀ (x y z : V), d x z ≤ d x y + d y z) {C : Finset V} (hC : C.card ≤ L.length) {r : α} (hr : ∀ v ∈ P, ∃ c ∈ C, d v c ≤ r) {v : V} (hv : v ∈ P) : centerDist d L.toFinset v ≤ ↑(2 * r)

The 2-approximation for farthest-first traversals ([WS11], Theorem 2.3): if some set C of at most |L| centers covers every point of P within r, then every point of P is within 2 r of a center of the farthest-first traversal L.

theorem Cslib.Algorithms.Lean.KCenter.centerDist_gonzalez_le_two_mul {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} [Semiring α] [IsOrderedAddMonoid α] (hsymm : ∀ (x y : V), d x y = d y x) (htri : ∀ (x y z : V), d x z ≤ d x y + d y z) {k : ℕ} {C : Finset V} (hC : C.card ≤ k) {r : α} (hr : ∀ v ∈ P, ∃ c ∈ C, d v c ≤ r) {v : V} (hv : v ∈ P) : centerDist d (gonzalez d P k).toFinset v ≤ ↑(2 * r)

Gonzalez's algorithm is a 2-approximation ([WS11], Theorem 2.3; [Gon85]): for a symmetric distance with the triangle inequality, if some set C of at most k points of the space covers every point of P within r, then every point of P is within 2 r of the k centers chosen by gonzalez d P k.

theorem Cslib.Algorithms.Lean.KCenter.radius_gonzalez_le_two_mul {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} [Semiring α] [IsOrderedAddMonoid α] [Fintype V] [Nonempty V] (hsymm : ∀ (x y : V), d x y = d y x) (htri : ∀ (x y z : V), d x z ≤ d x y + d y z) (hP : ∀ (v : V), v ∈ P) {k : ℕ} {r : α} (hr : optRadius d k ≤ ↑r) : radius d (gonzalez d P k).toFinset ≤ ↑(2 * r)

Gonzalez's algorithm is a 2-approximation for k-center ([WS11], Theorem 2.3; [Gon85]): on a finite space with a symmetric distance satisfying the triangle inequality, run on a list P of all the points, the k chosen centers have radius at most 2 r for every bound r on the optimal radius.

theorem Cslib.Algorithms.Lean.KCenter.radius_gonzalez_le_two_mul_radius {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} [Semiring α] [IsOrderedAddMonoid α] [Fintype V] [Nonempty V] (hsymm : ∀ (x y : V), d x y = d y x) (htri : ∀ (x y z : V), d x z ≤ d x y + d y z) (hP : ∀ (v : V), v ∈ P) {k : ℕ} {S : Finset V} (hS : S.card ≤ k) {r : α} (hr : radius d S ≤ ↑r) : radius d (gonzalez d P k).toFinset ≤ ↑(2 * r)

The 2-approximation against every feasible solution: the radius of Gonzalez's centers is at most twice the radius of every set of at most k centers.

theorem Cslib.Algorithms.Lean.KCenter.radius_gonzalez_le_two_mul_optRadius {V : Type u_1} {α : Type u_2} [LinearOrder α] [DecidableEq V] {d : V → V → α} {P : List V} [Semiring α] [IsOrderedAddMonoid α] [Fintype V] [Nonempty V] (hsymm : ∀ (x y : V), d x y = d y x) (htri : ∀ (x y z : V), d x z ≤ d x y + d y z) (hP : ∀ (v : V), v ∈ P) {k : ℕ} (hk : 0 < k) : radius d (gonzalez d P k).toFinset ≤ ↑(2 * (optRadius d k).untop ⋯)

The 2-approximation against the optimum value: with k ≥ 1 centers the optimal radius is finite, and Gonzalez's radius is at most twice it.