Independent dominating set

AbbreviationIndependent dominating set instances#✓fully proved

An instance of INDEPENDENT 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 on the size of the set.

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

Used by 4

Used byGraph of an independent dominating set instance · INDEPENDENT DOMINATING SET as a decision problem · Instances with a small independent dominating set · Well-formed independent dominating set instances

DefinitionGraph of an independent dominating set instance#✓fully proved

For an independent dominating set instance with \(n\) vertices and edge list \(E\), the graph of the instance is the simple graph on \(\{0, \dots, n-1\}\) in which distinct vertices \(u\) and \(v\) are adjacent when \((u, v)\) or \((v, u)\) belongs to \(E\).

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

Uses 2 · Used by 1

Statement usesGraph of an edge list · Independent dominating set instances

Used byInstances with a small independent dominating set

DefinitionWell-formed independent dominating set instances#✓fully proved

An independent dominating set instance \((n, E, K)\) is well formed when the list \(E\) has no repeated entries and every pair \((a, b)\) in \(E\) satisfies \(a < n\), \(b < n\), \(a \ne b\), and \((b, a)\) does not belong to \(E\).

def WellFormed (i : IndependentDominatingSetInstance) : 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 usesIndependent dominating set instances

Used byINDEPENDENT DOMINATING SET as a decision problem

DefinitionInstances with a small independent dominating set#✓fully proved

An independent dominating set instance \((n, E, K)\) has a small independent dominating set when there is a set \(S\) of vertices of its graph with at most \(K\) elements such that every vertex lies in \(S\) or is adjacent to a vertex of \(S\), and no two distinct vertices of \(S\) are adjacent.

def IndependentDominatingSetFeasible
    (i : IndependentDominatingSetInstance) : Prop :=
  ∃ S : Finset (Fin i.1), S.card ≤ i.2.2 ∧
    (∀ v : Fin i.1, v ∈ S ∨ ∃ u ∈ S, (Graph i).Adj u v) ∧
    ∀ u ∈ S, ∀ v ∈ S, u ≠ v → ¬ (Graph i).Adj u v

Uses 2 · Used by 1

Statement usesGraph of an independent dominating set instance · Independent dominating set instances

Used byINDEPENDENT DOMINATING SET as a decision problem

DefinitionINDEPENDENT DOMINATING SET as a decision problem#✓fully proved

The decision problem INDEPENDENT DOMINATING SET accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an independent dominating set instance \((n, E, K)\) that is well formed and whose graph has an independent dominating set of at most \(K\) vertices. It rejects every bitstring that does not decode to an instance.

noncomputable def independentDominatingSetDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := IndependentDominatingSetInstance) x with
  | some i => decide (WellFormed i ∧ IndependentDominatingSetFeasible 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 · Instances with a small independent dominating set · Independent dominating set instances · Well-formed independent dominating set instances · Decision problems

Used byINDEPENDENT DOMINATING SET is NP-complete

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

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), INDEPENDENT DOMINATING SET (a small maximal independent set).

Uses 5

Statement usesPolynomial-time many-one reduction · INDEPENDENT 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.