Precoloring extension

AbbreviationInstances of PRECOLORING EXTENSION#✓fully proved

An instance of precoloring extension is a tuple \((n, E, c, K)\) consisting of a natural number \(n\) (the number of vertices), a list \(E\) of pairs of natural numbers (the edges), a list \(c\) of natural numbers (the partial coloring, where an entry \(0\) means uncolored and an entry \(k + 1\) means color \(k\)), and a natural number \(K\) (the number of colors).

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

Used by 3

Used byPRECOLORING EXTENSION as a decision problem · Feasible precoloring extension instances · Well-formed precoloring extension instances

DefinitionWell-formed precoloring extension instances#✓fully proved

An instance \((n, E, c, K)\) of precoloring extension is well formed when the edge list \(E\) has no repeated entries, every edge \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\), and the partial coloring \(c\) has length \(n\).

def WellFormed (i : PrecoloringExtensionInstance) : 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) ∧
    i.2.2.1.length = i.1

Uses 1 · Used by 1

Statement usesInstances of PRECOLORING EXTENSION

Used byPRECOLORING EXTENSION as a decision problem

DefinitionFeasible precoloring extension instances#✓fully proved

An instance \((n, E, c, K)\) of precoloring extension is feasible when there is a list \(\chi = (\chi_0, \dots, \chi_{n-1})\) of \(n\) natural numbers such that \(\chi_v < K\) for every vertex \(v < n\), \(\chi_v = c_v - 1\) for every vertex \(v < n\) with \(c_v \ne 0\), and \(\chi_u \ne \chi_v\) for every edge \((u, v)\) in \(E\). Here \(c_v\) is the entry of \(c\) at position \(v\), and an entry of a list at a position beyond its length is read as \(0\).

def PrecoloringExtensionFeasible
    (i : PrecoloringExtensionInstance) : Prop :=
  ∃ coloring : List ℕ, coloring.length = i.1 ∧ (∀ v < i.1, coloring.getD v 0 < i.2.2.2) ∧
    (∀ v < i.1, i.2.2.1.getD v 0 ≠ 0 → coloring.getD v 0 = i.2.2.1.getD v 0 - 1) ∧
    ∀ e ∈ i.2.1, coloring.getD e.1 0 ≠ coloring.getD e.2 0

Uses 1 · Used by 1

Statement usesInstances of PRECOLORING EXTENSION

Used byPRECOLORING EXTENSION as a decision problem

DefinitionPRECOLORING EXTENSION as a decision problem#✓fully proved

The decision problem PRECOLORING EXTENSION accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a precoloring extension instance that is well formed and feasible; bitstrings that do not decode are rejected.

noncomputable def precoloringExtensionDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := PrecoloringExtensionInstance) x with
  | some i => decide (WellFormed i ∧ PrecoloringExtensionFeasible 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 precoloring extension instances · Instances of PRECOLORING EXTENSION · Well-formed precoloring extension instances · Decision problems

Used byPRECOLORING EXTENSION is NP-complete

TheoremPRECOLORING EXTENSION is NP-complete#●ready to prove

The decision problem PRECOLORING EXTENSION lies in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. Biro, M. Hujter, and Z. Tuza, "Precoloring extension. I. Interval graphs", Discrete Mathematics 100 (1992), 267-279 (NP- completeness on interval graphs, hence on general graphs); hardness also follows directly from Garey-Johnson CHROMATIC NUMBER (GT4) by taking the precoloring to be empty.

Uses 5

Statement usesPolynomial-time many-one reduction · PRECOLORING EXTENSION as a decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.