Dominating sets

A set S of vertices of a simple graph is dominating when every vertex lies in S or is adjacent to a vertex of S. Deciding whether a graph has a dominating set of at most k vertices is the NP-complete dominating set problem (Cslib.Complexity.DominatingSet_npComplete on the library's encoded graphs), the source problem of the hardness of approximating metric k-center ([WS11], Section 2.2; Cslib.Algorithms.Lean.KCenter.isDominatingSet_of_radius_le_mul). Mathlib has no notion of domination for simple graphs.

Main definitions

• SimpleGraph.IsDominatingSet: S dominates G.

Main results

• SimpleGraph.isDominatingSet_iff: the defining property.
• SimpleGraph.isDominatingSet_univ, SimpleGraph.IsDominatingSet.mono: the vertex set is dominating, and supersets of dominating sets are dominating.
• SimpleGraph.IsDominatingSet.nonempty: a dominating set of a nonempty graph is nonempty.

References

• D. P. Williamson and D. B. Shmoys, The Design of Approximation Algorithms, Section 2.2.

def SimpleGraph.IsDominatingSet {V : Type u_1} (G : SimpleGraph V) (S : Set V) : Prop

A set S of vertices dominates G when every vertex lies in S or is adjacent to a vertex of S.

theorem SimpleGraph.isDominatingSet_iff {V : Type u_1} {G : SimpleGraph V} {S : Set V} : G.IsDominatingSet S ↔ ∀ (v : V), v ∈ S ∨ ∃ s ∈ S, G.Adj v s

@[instance_reducible]

instance SimpleGraph.instDecidableIsDominatingSetCoeFinsetOfFintypeOfDecidableEqOfDecidableRelAdj {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (S : Finset V) : Decidable (G.IsDominatingSet ↑S)

theorem SimpleGraph.isDominatingSet_univ {V : Type u_1} (G : SimpleGraph V) : G.IsDominatingSet Set.univ

The set of all vertices dominates every graph.

theorem SimpleGraph.IsDominatingSet.mono {V : Type u_1} {G : SimpleGraph V} {S T : Set V} (h : G.IsDominatingSet S) (hST : S ⊆ T) : G.IsDominatingSet T

A superset of a dominating set is dominating.

theorem SimpleGraph.IsDominatingSet.nonempty {V : Type u_1} {G : SimpleGraph V} {S : Set V} [Nonempty V] (h : G.IsDominatingSet S) : S.Nonempty

A dominating set of a graph with a vertex is nonempty.