Connected dominating set

AbbreviationInstances of CONNECTED DOMINATING SET#✓fully proved

An instance of CONNECTED 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 ConnectedDominatingSetInstance := ℕ × List (ℕ × ℕ) × ℕ

Used by 4

Used byThe decision problem CONNECTED DOMINATING SET · Feasible CONNECTED DOMINATING SET instances · Graph of a CONNECTED DOMINATING SET instance · Well-formed CONNECTED DOMINATING SET instances

DefinitionGraph of a CONNECTED DOMINATING SET instance#✓fully proved

For an instance \((n, E, K)\) of CONNECTED DOMINATING SET, its graph is the simple graph on the vertex set \(\{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 : ConnectedDominatingSetInstance) : 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 CONNECTED DOMINATING SET

Used byFeasible CONNECTED DOMINATING SET instances

DefinitionWell-formed CONNECTED DOMINATING SET instances#✓fully proved

An instance \((n, E, K)\) of CONNECTED DOMINATING SET is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) has \(u < n\), \(v < n\) and \(u \ne v\), with the reversed pair \((v, u)\) not in \(E\).

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

Used byThe decision problem CONNECTED DOMINATING SET

DefinitionFeasible CONNECTED DOMINATING SET instances#✓fully proved

An instance \((n, E, K)\) of CONNECTED DOMINATING SET is feasible when there is a set \(S\) of vertices of its graph \(G\) with at most \(K\) elements such that every vertex of \(G\) lies in \(S\) or is adjacent in \(G\) to a vertex of \(S\), and the subgraph of \(G\) induced by \(S\) is connected (in particular, \(S\) is nonempty).

def ConnectedDominatingSetFeasible
    (i : ConnectedDominatingSetInstance) : Prop :=
  ∃ S : Finset (Fin i.1), S.card ≤ i.2.2 ∧
    (∀ v : Fin i.1, v ∈ S ∨ ∃ u ∈ S, (Graph i).Adj u v) ∧
    ((Graph i).induce (↑S : Set (Fin i.1))).Connected

Uses 2 · Used by 1

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

Used byThe decision problem CONNECTED DOMINATING SET

DefinitionThe decision problem CONNECTED DOMINATING SET#✓fully proved

CONNECTED DOMINATING SET accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance of CONNECTED DOMINATING SET that is well formed and feasible. Bitstrings that do not decode to an instance are rejected.

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

Used byCONNECTED DOMINATING SET is NP-complete

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

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

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

Sources

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

Uses 5

Statement usesPolynomial-time many-one reduction · The decision problem CONNECTED 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.