Total dominating set

AbbreviationInstances of TOTAL DOMINATING SET#✓fully proved

An instance of TOTAL DOMINATING SET is a triple \((n, E, K)\) consisting of a natural number \(n\), the number of vertices, a list \(E\) of pairs of natural numbers, the edges, and a natural number \(K\), the bound.

abbrev TotalDominatingSetInstance := ℕ × List (ℕ × ℕ) × ℕ

Used by 4

Used byGraph of a total dominating set instance · The decision problem TOTAL DOMINATING SET · Feasibility of a total dominating set instance · Well-formed total dominating set instances

DefinitionGraph of a total dominating set instance#✓fully proved

The graph of an instance \((n, E, K)\) of TOTAL DOMINATING SET is the simple graph on \(\{0, \dots, n-1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E\). Loops are dropped, and pairs with an endpoint at least \(n\) contribute no edge.

def Graph (i : TotalDominatingSetInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2.1

Uses 2 · Used by 1

Statement usesGraph of an edge list · Instances of TOTAL DOMINATING SET

Used byFeasibility of a total dominating set instance

DefinitionWell-formed total dominating set instances#✓fully proved

An instance \((n, E, K)\) of TOTAL DOMINATING SET is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and its reversal \((v, u)\) does not belong to \(E\).

def WellFormed (i : TotalDominatingSetInstance) : Prop :=
  i.2.1.Nodup ∧ ∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.1

Uses 1 · Used by 1

Statement usesInstances of TOTAL DOMINATING SET

Used byThe decision problem TOTAL DOMINATING SET

DefinitionFeasibility of a total dominating set instance#✓fully proved

An instance \((n, E, K)\) of TOTAL DOMINATING SET is feasible when there is a set \(S\) of at most \(K\) vertices of its graph such that every vertex \(v\) of the graph, including the vertices of \(S\), is adjacent to some vertex \(u \in S\).

def TotalDominatingSetFeasible
    (i : TotalDominatingSetInstance) : Prop :=
  ∃ S : Finset (Fin i.1), S.card ≤ i.2.2 ∧
    ∀ v : Fin i.1, ∃ u ∈ S, (Graph i).Adj u v

Uses 2 · Used by 1

Statement usesGraph of a total dominating set instance · Instances of TOTAL DOMINATING SET

Used byThe decision problem TOTAL DOMINATING SET

DefinitionThe decision problem TOTAL DOMINATING SET#✓fully proved

TOTAL DOMINATING SET accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of triples of a natural number, a list of pairs of natural numbers and a natural number, to an instance \((n, E, K)\) that is well formed and feasible: some set of at most \(K\) vertices of the graph of the instance contains a neighbor of every vertex. Bitstrings that do not decode to an instance are rejected.

noncomputable def totalDominatingSetDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := TotalDominatingSetInstance) x with
  | some i => decide (WellFormed i ∧ TotalDominatingSetFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasibility of a total dominating set instance · Instances of TOTAL DOMINATING SET · Well-formed total dominating set instances · Decision problems

Used byTOTAL DOMINATING SET is NP-complete

TheoremTOTAL DOMINATING SET is NP-complete#●ready to prove

The decision problem TOTAL DOMINATING SET belongs to NP, and every decision problem in NP reduces to TOTAL DOMINATING SET by a polynomial-time many-one reduction.

public theorem_wanted totalDominatingSet_npComplete :
    totalDominatingSetDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L totalDominatingSetDec

Sources

• E. J. Cockayne, R. M. Dawes, and S. T. Hedetniemi, "Total domination in graphs", Networks 10 (1980), 211-219; R. Laskar, J. Pfaff, S. M. Hedetniemi, and S. T. Hedetniemi, "On the algorithmic complexity of total domination", SIAM Journal on Algebraic and Discrete Methods 5 (1984), 420-425.

Uses 5

Statement usesPolynomial-time many-one reduction · The decision problem TOTAL DOMINATING SET · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.