Roman domination

AbbreviationRoman domination instances#✓fully proved

An instance of ROMAN DOMINATION 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 weight bound.

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

Used by 4

Used byGraph of a Roman domination instance · ROMAN DOMINATION as a decision problem · Feasible Roman domination instances · Well-formed Roman domination instances

DefinitionGraph of a Roman domination instance#✓fully proved

For an instance \((n, E, K)\) of ROMAN DOMINATION, its graph is the graph of the edge list \(E\) on \(n\) vertices: 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 : RomanDominationInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2.1

Uses 2 · Used by 1

Statement usesGraph of an edge list · Roman domination instances

Used byFeasible Roman domination instances

DefinitionWell-formed Roman domination instances#✓fully proved

An instance \((n, E, K)\) of ROMAN DOMINATION is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) has \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\).

def WellFormed (i : RomanDominationInstance) : 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 usesRoman domination instances

Used byROMAN DOMINATION as a decision problem

DefinitionFeasible Roman domination instances#✓fully proved

An instance \((n, E, K)\) of ROMAN DOMINATION is feasible when there is a function \(f\) from the vertices \(\{0, \dots, n - 1\}\) of its graph to \(\{0, 1, 2\}\) such that every vertex \(v\) with \(f(v) = 0\) is adjacent to some vertex \(u\) with \(f(u) = 2\), and the total weight \(\sum_v f(v)\) is at most \(K\).

def RomanDominationFeasible
    (i : RomanDominationInstance) : Prop :=
  ∃ labeling : Fin i.1 → ℕ, (∀ v, labeling v ≤ 2) ∧
    (∀ v, labeling v = 0 → ∃ u, (Graph i).Adj u v ∧ labeling u = 2) ∧
    (Finset.univ.sum labeling) ≤ i.2.2

Uses 2 · Used by 1

Statement usesGraph of a Roman domination instance · Roman domination instances

Used byROMAN DOMINATION as a decision problem

DefinitionROMAN DOMINATION as a decision problem#✓fully proved

The decision problem ROMAN DOMINATION accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance \((n, E, K)\) of ROMAN DOMINATION that is well formed and feasible; it rejects every other bitstring.

noncomputable def romanDominationDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := RomanDominationInstance) x with
  | some i => decide (WellFormed i ∧ RomanDominationFeasible 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 Roman domination instances · Roman domination instances · Well-formed Roman domination instances · Decision problems

Used byROMAN DOMINATION is NP-complete

TheoremROMAN DOMINATION is NP-complete#●ready to prove

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

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

Sources

• E. J. Cockayne, P. A. Dreyer Jr., S. M. Hedetniemi, and S. T. Hedetniemi, "Roman domination in graphs", Discrete Mathematics 278 (2004), 11-22.

Uses 5

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