Efficient domination

AbbreviationEfficient Domination instances#✓fully proved

An instance of EFFICIENT DOMINATION is a pair \((n, E)\) of a natural number \(n\), the number of vertices, and a list \(E\) of pairs of natural numbers, the edges.

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

Used by 4

Used byEFFICIENT DOMINATION (PERFECT CODE) as a decision problem · Instances with an efficient dominating set · Graph of an Efficient Domination instance · Well-formed Efficient Domination instances

DefinitionGraph of an Efficient Domination instance#✓fully proved

For an instance \((n, E)\), its graph is the simple graph on the vertex set \(\{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 : EfficientDominationInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2

Uses 2 · Used by 1

Statement usesGraph of an edge list · Efficient Domination instances

Used byInstances with an efficient dominating set

DefinitionWell-formed Efficient Domination instances#✓fully proved

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

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

Uses 1 · Used by 1

Statement usesEfficient Domination instances

Used byEFFICIENT DOMINATION (PERFECT CODE) as a decision problem

DefinitionInstances with an efficient dominating set#✓fully proved

An instance \((n, E)\) of EFFICIENT DOMINATION is feasible when its graph has an efficient dominating set (a perfect code): a set \(S\) of vertices such that every vertex \(v\) has exactly one vertex \(u \in S\) with \(u = v\) or \(u\) adjacent to \(v\).

def EfficientDominationFeasible
    (i : EfficientDominationInstance) : Prop :=
  ∃ S : Finset (Fin i.1),
    ∀ v : Fin i.1, ∃! u ∈ S, u = v ∨ (Graph i).Adj u v

Uses 2 · Used by 1

Statement usesEfficient Domination instances · Graph of an Efficient Domination instance

Used byEFFICIENT DOMINATION (PERFECT CODE) as a decision problem

DefinitionEFFICIENT DOMINATION (PERFECT CODE) as a decision problem#✓fully proved

The decision problem EFFICIENT DOMINATION accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of instances, to an instance \((n, E)\) that is well formed and whose graph has an efficient dominating set. Bitstrings that do not decode to an instance are rejected.

noncomputable def efficientDominationDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := EfficientDominationInstance) x with
  | some i => decide (WellFormed i ∧ EfficientDominationFeasible 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 an efficient dominating set · Efficient Domination instances · Well-formed Efficient Domination instances · Decision problems

Used byEFFICIENT DOMINATION (PERFECT CODE) is NP-complete

TheoremEFFICIENT DOMINATION (PERFECT CODE) is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), EFFICIENT DOMINATION; D. G. Corneil and Y. Perl, "Clustering and domination in perfect graphs" (1984) and the perfect-code literature.

Uses 5

Statement usesPolynomial-time many-one reduction · EFFICIENT DOMINATION (PERFECT CODE) 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.