Dominating sets

DominatingSet is problem GT2 of Garey and Johnson. Its instances (Cslib.Complexity.DominatingSetInstance, encoded by Cslib.Complexity.encDominatingSet) pair a graph, given by a list of vertices and a list of edges, with a number k. An instance is in the problem when some k declared vertices dominate the graph: every declared vertex is chosen or is adjacent to a chosen one. Graphs are read on their declared vertices through Cslib.Complexity.Graph.induced, and domination through SimpleGraph.IsDominatingSet, as for VertexCover. Edges with an undeclared endpoint and self-loops are therefore ignored, and repeated vertex entries count once.

The dominating set has exactly k distinct vertices, matching VertexCover and IndependentSet. A set of declared vertices containing a dominating set is dominating, so this agrees with the textbook formulation "a dominating set of at most k vertices" for every k up to the number n of distinct declared vertices. DominatingSet rejects every k > n (mem_DominatingSet_iff_exists_card_le).

NP membership uses a subset witness (Cslib.Complexity.mem_NP_of_subsetWitness): the certificate selects declared vertices, and DominatingSet.isDominating checks domination.

The reduction from vertex cover

VertexCover.toDominatingSet maps (G, k) to ⟨VertexCover.dominationGraph G, k + 1⟩. The graph dominationGraph G has:

• a copy 2v of every declared vertex v of G;
• a hub 1 adjacent to every copy, and a pendant 3 adjacent only to the hub;
• for every edge e of G between distinct declared vertices (VertexCover.properEdges), a vertex VertexCover.edgeVertex e = 2 * Nat.pair e.1 e.2 + 5 adjacent to the copies of the two endpoints of e.

The hub dominates every copy, and either the hub or the pendant must be chosen to dominate the pendant. Choosing the hub costs one vertex. The vertex of an edge is then dominated exactly when an endpoint's copy, or the edge's own vertex, is chosen. Replacing the vertex of an edge by an endpoint reads a dominating set of k + 1 vertices back as a vertex cover of at most k vertices, and a vertex cover of k vertices with the hub is a dominating set of k + 1 vertices. Since VertexCover asks for exactly k vertices, instances with k > n are sent to the target 0. No dominating set of 0 vertices dominates the hub.

Garey and Johnson cite a transformation from VERTEX COVER for GT2 (locator from secondary sources). The common textbook version keeps the edges of G, adds a vertex for every edge and keeps k, but it must account separately for isolated vertices of G: they impose nothing on a cover and must be chosen in a dominating set. The hub and pendant used here dominate every copy, including isolated ones, at a fixed cost of one vertex. So the reduction needs neither the number of isolated vertices nor the edges of G between copies.

Main definitions

• Cslib.Complexity.DominatingSetInstance, Cslib.Complexity.encDominatingSet.
• Cslib.Complexity.DominatingSet.
• Cslib.Complexity.DominatingSet.isDominating: the executable domination test.
• Cslib.Complexity.VertexCover.properEdges, Cslib.Complexity.VertexCover.edgeVertex, Cslib.Complexity.VertexCover.dominationGraph, Cslib.Complexity.VertexCover.toDominatingSet: the reduction from VertexCover.

Main results

• Cslib.Complexity.mem_DominatingSet_iff, Cslib.Complexity.mem_DominatingSet_iff_exists_card_le: dominating sets of exactly k vertices versus dominating sets of at most k vertices.
• Cslib.Complexity.DominatingSet.isDominating_eq_true_iff, Cslib.Complexity.DominatingSet.computableInPolyTime_isDominating, Cslib.Complexity.DominatingSet.mem_NP: DominatingSet ∈ NP encDominatingSet.
• Cslib.Complexity.VertexCover.toDominatingSet_mem_iff, Cslib.Complexity.VertexCover.computableInPolyTime_toDominatingSet, Cslib.Complexity.polyTimeReducible_VertexCover_DominatingSet: the reduction.
• Cslib.Complexity.DominatingSet_npHard, Cslib.Complexity.DominatingSet_npComplete: DominatingSet is NP-complete.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability, Problem GT2.

structure Cslib.Complexity.DominatingSetInstance : Type

An instance (graph, bound) of Dominating Set.

• graph : Graph

  The undirected graph to dominate.

• bound : ℕ

  The number of vertices in the dominating set.

theorem Cslib.Complexity.DominatingSetInstance.ext {x y : DominatingSetInstance} (graph : x.graph = y.graph) (bound : x.bound = y.bound) : x = y

theorem Cslib.Complexity.DominatingSetInstance.ext_iff {x y : DominatingSetInstance} : x = y ↔ x.graph = y.graph ∧ x.bound = y.bound

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqDominatingSetInstance : DecidableEq DominatingSetInstance

def Cslib.Complexity.instDecidableEqDominatingSetInstance.decEq (x✝ x✝¹ : DominatingSetInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instReprDominatingSetInstance : Repr DominatingSetInstance

def Cslib.Complexity.instReprDominatingSetInstance.repr : DominatingSetInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instInhabitedDominatingSetInstance : Inhabited DominatingSetInstance

theorem Cslib.Complexity.encDominatingSet_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : DominatingSetInstance) => (a.graph, a.bound)) encDominatingSet encDominatingSetFields 1 1

theorem Cslib.Complexity.encDominatingSet_bound_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → DominatingSetInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDominatingSet → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encDominatingSet_bound_deg : Turing.MultiTapeTM.ComputableInDegree DominatingSetInstance.bound encDominatingSet Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encDominatingSet_graph_deg : Turing.MultiTapeTM.ComputableInDegree DominatingSetInstance.graph encDominatingSet encGraph 1 1

@[reducible, inline]

abbrev Cslib.Complexity.encDominatingSetFields : Graph × ℕ ↪ List Bool

The tuple of the fields of encDominatingSet.

theorem Cslib.Complexity.encDominatingSet_graph_inO : Turing.MultiTapeTM.ComputableInO DominatingSetInstance.graph encDominatingSet encGraph (fun (a : DominatingSetInstance) => (encDominatingSet a).length) fun (a : DominatingSetInstance) => (encDominatingSet a).length

def Cslib.Complexity.encDominatingSet : DominatingSetInstance ↪ List Bool

Encoding of DominatingSetInstance as a pair (graph, bound).

theorem Cslib.Complexity.encDominatingSet_graph_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → DominatingSetInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDominatingSet → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph

theorem Cslib.Complexity.encDominatingSet_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encGraph) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { graph := x0 x, bound := x1 x }) encIn encDominatingSet

theorem Cslib.Complexity.encDominatingSet_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ) => { graph := p.1, bound := p.2 }) encDominatingSetFields encDominatingSet 1 1

@[simp]

theorem Cslib.Complexity.encDominatingSet_apply (a : DominatingSetInstance) : encDominatingSet a = encDominatingSetFields (a.graph, a.bound)

theorem Cslib.Complexity.encDominatingSet_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encGraph T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { graph := x0 x, bound := x1 x }) encIn encDominatingSet (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encDominatingSet_bound_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → DominatingSetInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDominatingSet S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encDominatingSet_graph_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → DominatingSetInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDominatingSet S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph S✝

theorem Cslib.Complexity.encDominatingSet_bound_inO : Turing.MultiTapeTM.ComputableInO DominatingSetInstance.bound encDominatingSet Turing.MultiTapeTM.encNat (fun (a : DominatingSetInstance) => (encDominatingSet a).length) fun (a : DominatingSetInstance) => (encDominatingSet a).length

theorem Cslib.Complexity.encDominatingSet_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encGraph budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { graph := x0 x, bound := x1 x }) encIn encDominatingSet budget

def Cslib.Complexity.DominatingSet : Set DominatingSetInstance

The graphs with a dominating set of k of their vertices Garey and Johnson, Problem GT2: k declared vertices such that every declared vertex is chosen or adjacent to a chosen one.

@[simp]

theorem Cslib.Complexity.mem_DominatingSet_iff {G : Graph} {k : ℕ} : { graph := G, bound := k } ∈ DominatingSet ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ G.vertices) ∧ (∀ v ∈ G.vertices, v ∈ S ∨ ∃ s ∈ S, G.toSimpleGraph.Adj v s) ∧ S.card = k

Membership in DominatingSet as a finite set of k declared vertices such that every declared vertex is chosen or adjacent to a chosen one.

theorem Cslib.Complexity.mem_DominatingSet_iff_exists_card_le {G : Graph} {k : ℕ} : { graph := G, bound := k } ∈ DominatingSet ↔ k ≤ G.vertices.toFinset.card ∧ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ G.vertices) ∧ (∀ v ∈ G.vertices, v ∈ S ∨ ∃ s ∈ S, G.toSimpleGraph.Adj v s) ∧ S.card ≤ k

DominatingSet through dominating sets of at most k vertices: (G, k) ∈ DominatingSet exactly when k is at most the number of distinct declared vertices and some dominating set has at most k vertices.

Membership in NP

def Cslib.Complexity.DominatingSet.isDominating (G : Graph) (C : List ℕ) : Bool

Whether every declared vertex of G is in C or adjacent to a vertex of C.

theorem Cslib.Complexity.DominatingSet.isDominating_eq_true_iff {G : Graph} {C : List ℕ} : isDominating G C = true ↔ ∀ v ∈ G.vertices, v ∈ C ∨ ∃ s ∈ C, G.toSimpleGraph.Adj v s

isDominating G C holds exactly when C dominates the declared vertices of G.

theorem Cslib.Complexity.DominatingSet.computableInPolyTime_isDominating : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × List ℕ) => isDominating p.1 p.2) (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBool

The domination test is polynomial-time.

theorem Cslib.Complexity.DominatingSet.mem_NP : DominatingSet ∈ NP encDominatingSet

DominatingSet belongs to NP: the certificate selects distinct declared vertices, and the verifier checks their number and isDominating.

Reduction from vertex covers

def Cslib.Complexity.VertexCover.properEdges (G : Graph) : List (ℕ × ℕ)

The listed edges of G between two distinct declared vertices.

theorem Cslib.Complexity.VertexCover.mem_properEdges {G : Graph} {e : ℕ × ℕ} : e ∈ properEdges G ↔ e ∈ G.edges ∧ e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices ∧ e.1 ≠ e.2

An edge is proper when it is listed and joins two distinct declared vertices.

def Cslib.Complexity.VertexCover.edgeVertex (e : ℕ × ℕ) : ℕ

The vertex of the edge e in dominationGraph: an odd number at least 5.

theorem Cslib.Complexity.VertexCover.edgeVertex_injective : Function.Injective edgeVertex

Distinct edges have distinct vertices.

def Cslib.Complexity.VertexCover.dominationGraph (G : Graph) : Graph

The graph of the reduction from VertexCover to DominatingSet: a copy 2v of every declared vertex v, a hub 1 adjacent to every copy, a pendant 3 adjacent to the hub, and for every proper edge e a vertex edgeVertex e adjacent to the copies of the endpoints of e.

theorem Cslib.Complexity.VertexCover.mem_dominationGraph_fst {G : Graph} {w : ℕ} : w ∈ (dominationGraph G).vertices ↔ w = 1 ∨ w = 3 ∨ (∃ v ∈ G.vertices, 2 * v = w) ∨ ∃ e ∈ properEdges G, edgeVertex e = w

The vertices of dominationGraph G.

theorem Cslib.Complexity.VertexCover.mem_dominationGraph_snd {G : Graph} {a b : ℕ} : (a, b) ∈ (dominationGraph G).edges ↔ a = 1 ∧ b = 3 ∨ (a = 1 ∧ ∃ v ∈ G.vertices, b = 2 * v) ∨ ∃ e ∈ properEdges G, a = edgeVertex e ∧ (b = 2 * e.1 ∨ b = 2 * e.2)

The edges of dominationGraph G.

def Cslib.Complexity.VertexCover.toDominatingSet : VertexCoverInstance → DominatingSetInstance

The reduction from VertexCover to DominatingSet: the graph dominationGraph G with the target k + 1, or the unsatisfiable target 0 when k exceeds the number of distinct declared vertices.

theorem Cslib.Complexity.VertexCover.toDominatingSet_mem_iff (x : VertexCoverInstance) : toDominatingSet x ∈ DominatingSet ↔ x ∈ VertexCover

Vertex covers of G are dominating sets of dominationGraph G with the hub.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_properEdges : Turing.MultiTapeTM.ComputableInPolyTime properEdges encGraph (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

Listing the proper edges is polynomial-time.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_edgeVertex : Turing.MultiTapeTM.ComputableInPolyTime edgeVertex (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat

The vertex of an edge is computable in polynomial time from the binary endpoints.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_dominationGraph : Turing.MultiTapeTM.ComputableInPolyTime dominationGraph encGraph encGraph

The graph of the reduction is computable in polynomial time. The four lists are certified separately: fun_prop alone times out on the whole graph.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_toDominatingSet : Turing.MultiTapeTM.ComputableInPolyTime toDominatingSet encVertexCoverInstance encDominatingSet

The reduction toDominatingSet is polynomial-time: the binary target is compared with the number of distinct declared vertices, computed in unary.

theorem Cslib.Complexity.polyTimeReducible_VertexCover_DominatingSet : PolyTimeReducible encVertexCoverInstance encDominatingSet VertexCover DominatingSet

VertexCover reduces to DominatingSet in polynomial time via VertexCover.toDominatingSet.

theorem Cslib.Complexity.DominatingSet_npHard : NPHard encDominatingSet DominatingSet

DominatingSet is NP-hard.

theorem Cslib.Complexity.DominatingSet_npComplete : NPComplete encDominatingSet DominatingSet

DominatingSet is NP-complete Garey and Johnson, Problem GT2, with the target in binary.