Graph coloring

AbbreviationInstances of GRAPH COLORING#✓fully proved

An instance of GRAPH COLORING is a triple \((n, E, K)\) consisting 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 number of colors.

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

Used by 4

Used byGraph of a GRAPH COLORING instance · GRAPH COLORING as a decision problem · Feasible GRAPH COLORING instances · Well-formed GRAPH COLORING instances

DefinitionGraph of a GRAPH COLORING instance#✓fully proved

The graph of an instance \((n, E, K)\) of GRAPH COLORING is 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 : GraphColoringInstance) : 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 GRAPH COLORING

Used byFeasible GRAPH COLORING instances

DefinitionWell-formed GRAPH COLORING instances#✓fully proved

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

def WellFormed (i : GraphColoringInstance) : 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 GRAPH COLORING

Used byGRAPH COLORING as a decision problem

DefinitionFeasible GRAPH COLORING instances#✓fully proved

An instance \((n, E, K)\) of GRAPH COLORING is feasible when its graph is \(K\)-colorable, that is, when its vertices can be assigned colors from \(\{0, \dots, K - 1\}\) so that adjacent vertices receive different colors.

def GraphColoringFeasible
    (i : GraphColoringInstance) : Prop :=
  (Graph i).Colorable i.2.2

Uses 2 · Used by 1

Statement usesGraph of a GRAPH COLORING instance · Instances of GRAPH COLORING

Used byGRAPH COLORING as a decision problem

DefinitionGRAPH COLORING as a decision problem#✓fully proved

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

noncomputable def graphColoringDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := GraphColoringInstance) x with
  | some i => decide (WellFormed i ∧ GraphColoringFeasible 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 GRAPH COLORING instances · Instances of GRAPH COLORING · Well-formed GRAPH COLORING instances · Decision problems

Used byGRAPH COLORING is NP-complete

TheoremGRAPH COLORING is NP-complete#●ready to prove

The decision problem GRAPH COLORING belongs to NP, and every decision problem \(L\) in NP has a polynomial-time many-one reduction to GRAPH COLORING.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), GRAPH COLORING (chromatic number); R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

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