Dominating sets and the hardness gap for k-center

The hardness of approximating k-center within a factor below 2 comes from the dominating set problem ([WS11], Section 2.2 and Theorem 2.4, attributed there to [HN79]). Give a graph G the distance domDist G: 1 between adjacent vertices, 2 between distinct nonadjacent vertices and 0 from a vertex to itself. This is a metric, and a set of centers has radius at most 1 exactly when it dominates G; otherwise its radius is 2. So G has a dominating set of at most k vertices exactly when the optimal k-center radius is at most 1, and otherwise the optimum is 2. A set of centers whose radius is within a factor ρ < 2 of the optimum has radius less than 2 when the optimum is 1, so it is dominating: a polynomial-time ρ-approximation algorithm with ρ < 2 would decide the NP-complete dominating set problem.

Model

Graphs are Mathlib simple graphs on a finite nonempty vertex type with decidable equality and adjacency; dominating sets are SimpleGraph.IsDominatingSet. Distances take values in a linearly ordered strict semiring α such as ℕ or ℝ. A ρ-approximate set of centers is stated as "radius at most ρ * r for every bound r on the optimum", which avoids multiplication in WithTop α and agrees with radius ≤ ρ * optimum whenever the optimum is finite.

Limitations

This module proves the combinatorial reduction and the gap only, on Mathlib simple graphs. The NP-hardness statement of Theorem 2.4 on encoded instances, with the polynomial-time map from encoded graphs to distance matrices, is Cslib.Complexity.P_eq_NP_of_kCenter_approx (CslibFrontier.Computability.PCP.Approximation.KCenter).

Main definitions

• Cslib.Algorithms.Lean.KCenter.domDist: the {1, 2} distance of a graph.

Main results

• domDist_symm, domDist_triangle: domDist G is symmetric and satisfies the triangle inequality.
• radius_domDist_le_one_iff, radius_domDist_lt_two_iff: a set of centers has radius at most 1, equivalently less than 2, exactly when it is dominating.
• optRadius_domDist_le_one_iff: a dominating set of at most k vertices exists exactly when the optimal radius is at most 1.
• optRadius_domDist_eq_two: otherwise, for k ≥ 1, the optimal radius is 2.
• isDominatingSet_of_radius_le_mul: the gap: when a dominating set of at most k vertices exists, every ρ-approximate set of centers with ρ < 2 is dominating.
• exists_isDominatingSet_iff_of_radius_le_mul: so a ρ-approximate set of at most k centers with ρ < 2 is dominating exactly when some dominating set of at most k vertices exists.

References

• W.-L. Hsu and G. L. Nemhauser, Easy and hard bottleneck location problems
• D. P. Williamson and D. B. Shmoys, The Design of Approximation Algorithms, Section 2.2.

def Cslib.Algorithms.Lean.KCenter.domDist {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableEq V] [DecidableRel G.Adj] [Semiring α] (u v : V) : α

The {1, 2} distance of a graph ([WS11], Section 2.2): 0 from a vertex to itself, 1 between adjacent vertices and 2 between distinct nonadjacent vertices.

theorem Cslib.Algorithms.Lean.KCenter.domDist_symm {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] (u v : V) : domDist G u v = domDist G v u

theorem Cslib.Algorithms.Lean.KCenter.domDist_triangle {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (u v w : V) : domDist G u w ≤ domDist G u v + domDist G v w

theorem Cslib.Algorithms.Lean.KCenter.domDist_le_one_iff {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {u v : V} : domDist G u v ≤ 1 ↔ u = v ∨ G.Adj u v

theorem Cslib.Algorithms.Lean.KCenter.domDist_lt_two_iff {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {u v : V} : domDist G u v < 2 ↔ u = v ∨ G.Adj u v

theorem Cslib.Algorithms.Lean.KCenter.domDist_le_two {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (u v : V) : domDist G u v ≤ 2

theorem Cslib.Algorithms.Lean.KCenter.radius_domDist_le_one_iff {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Fintype V] [Nonempty V] {S : Finset V} : radius (domDist G) S ≤ ↑1 ↔ G.IsDominatingSet ↑S

A set of centers has radius at most 1 in the {1, 2} distance exactly when it dominates the graph.

theorem Cslib.Algorithms.Lean.KCenter.radius_domDist_lt_two_iff {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Fintype V] [Nonempty V] {S : Finset V} : radius (domDist G) S < ↑2 ↔ G.IsDominatingSet ↑S

Distances in the {1, 2} distance are integers, so radius less than 2 means radius at most 1: domination again.

theorem Cslib.Algorithms.Lean.KCenter.radius_domDist_le_two {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Fintype V] [Nonempty V] {S : Finset V} (hS : S.Nonempty) : radius (domDist G) S ≤ ↑2

A nonempty set of centers has radius at most 2 in the {1, 2} distance.

theorem Cslib.Algorithms.Lean.KCenter.optRadius_domDist_le_one_iff {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Fintype V] [Nonempty V] {k : ℕ} : optRadius (domDist G) k ≤ ↑1 ↔ ∃ (S : Finset V), S.card ≤ k ∧ G.IsDominatingSet ↑S

Dominating sets are k-center solutions of radius 1 ([WS11], Section 2.2): a graph has a dominating set of at most k vertices exactly when the optimal k-center radius of its {1, 2} distance is at most 1.

theorem Cslib.Algorithms.Lean.KCenter.optRadius_domDist_eq_two {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Fintype V] [Nonempty V] {k : ℕ} (hk : 0 < k) (h : ¬∃ (S : Finset V), S.card ≤ k ∧ G.IsDominatingSet ↑S) : optRadius (domDist G) k = ↑2

Without a dominating set of at most k ≥ 1 vertices, the optimal k-center radius of the {1, 2} distance is exactly 2.

theorem Cslib.Algorithms.Lean.KCenter.isDominatingSet_of_radius_le_mul {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Fintype V] [Nonempty V] {S : Finset V} {k : ℕ} {ρ : α} (hρ : ρ < 2) (happrox : ∀ (r : α), optRadius (domDist G) k ≤ ↑r → radius (domDist G) S ≤ ↑(ρ * r)) (hdom : ∃ (S : Finset V), S.card ≤ k ∧ G.IsDominatingSet ↑S) : G.IsDominatingSet ↑S

The gap behind the hardness of k-center ([WS11], Theorem 2.4; [HN79]): if a graph has a dominating set of at most k vertices, then every set S of centers that is ρ-approximate for the {1, 2} distance with ρ < 2 is dominating. So a ρ-approximation algorithm for k-center with ρ < 2 decides whether a dominating set of at most k vertices exists: check whether its output dominates the graph and has at most k vertices. This is the combinatorial core of Theorem 2.4; the NP-hardness statement is Cslib.Complexity.P_eq_NP_of_kCenter_approx.

theorem Cslib.Algorithms.Lean.KCenter.exists_isDominatingSet_iff_of_radius_le_mul {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Fintype V] [Nonempty V] {S : Finset V} {k : ℕ} {ρ : α} (hρ : ρ < 2) (hS : S.card ≤ k) (happrox : ∀ (r : α), optRadius (domDist G) k ≤ ↑r → radius (domDist G) S ≤ ↑(ρ * r)) : (∃ (T : Finset V), T.card ≤ k ∧ G.IsDominatingSet ↑T) ↔ G.IsDominatingSet ↑S

A ρ-approximation with ρ < 2 decides dominating set ([WS11], Theorem 2.4): if S has at most k vertices and is ρ-approximate for the {1, 2} distance with ρ < 2, then the graph has a dominating set of at most k vertices exactly when S is dominating.