Dominating set

AbbreviationInstances of DOMINATING SET#✓fully proved

An instance of DOMINATING SET is a triple \((n, E, K)\) 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 DominatingSetInstance := ℕ × List (ℕ × ℕ) × ℕ

Used by 4

Used byDOMINATING SET as a decision problem · Feasibility of a DOMINATING SET instance · Graph of a DOMINATING SET instance · Well-formed DOMINATING SET instances

DefinitionGraph of a DOMINATING SET instance#✓fully proved

For an instance \((n, E, K)\) of DOMINATING SET, its graph 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\).

def Graph (i : DominatingSetInstance) : 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 DOMINATING SET

Used byFeasibility of a DOMINATING SET instance

DefinitionWell-formed DOMINATING SET instances#✓fully proved

An instance \((n, E, K)\) of 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\), \(u \ne v\) and \((v, u) \notin E\).

def WellFormed (i : DominatingSetInstance) : 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 DOMINATING SET

Used byDOMINATING SET as a decision problem

DefinitionFeasibility of a DOMINATING SET instance#✓fully proved

An instance \((n, E, K)\) of DOMINATING SET is feasible when there is a set \(S\) of at most \(K\) vertices of its graph such that every vertex lies in \(S\) or is adjacent to a vertex of \(S\), where the graph has vertex set \(\{0, \dots, n - 1\}\) and distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E\).

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

Uses 2 · Used by 1

Statement usesInstances of DOMINATING SET · Graph of a DOMINATING SET instance

Used byDOMINATING SET as a decision problem

DefinitionDOMINATING SET as a decision problem#✓fully proved

The decision problem DOMINATING SET accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a triple \((n, E, K)\) of a natural number \(n\), a list \(E\) of pairs of natural numbers and a natural number \(K\) such that \(E\) has no repeated entries, every pair \((u, v) \in E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\), and there is a set \(S\) of at most \(K\) vertices with every vertex in \(S\) or adjacent to a vertex of \(S\), in the graph on \(\{0, \dots, n - 1\}\) where distinct \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E\). Bitstrings that do not decode are rejected.

noncomputable def dominatingSetDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := DominatingSetInstance) x with
  | some i => decide (WellFormed i ∧ DominatingSetFeasible 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 DOMINATING SET instance · Instances of DOMINATING SET · Well-formed DOMINATING SET instances · Decision problems

Used byDOMINATING SET is NP-complete

TheoremDOMINATING SET is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), DOMINATING SET.

Uses 5

Statement usesPolynomial-time many-one reduction · DOMINATING SET as a decision problem · 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.