Edge coloring

AbbreviationEdge coloring instances#✓fully proved

An instance of EDGE COLORING is a triple \((n, E, K)\) consisting of a natural number \(n\), the number of vertices, a finite list \(E\) of ordered pairs of natural numbers, the edges, and a natural number \(K\), the bound on the number of colors.

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

Used by 3

Used byEDGE COLORING as a decision problem · Feasible edge coloring instances · Well-formed edge coloring instances

DefinitionAdjacency in an edge coloring edge list#✓fully proved

Given a list \(E\) of ordered pairs of natural numbers and natural numbers \(u\) and \(v\), the boolean adjacency of \(u\) and \(v\) in \(E\) is true exactly when \((u, v)\) or \((v, u)\) occurs in \(E\).

def Adj (edges : List (ℕ × ℕ)) (u v : ℕ) : Bool :=
  edges.contains (u, v) || edges.contains (v, u)

DefinitionWell-formed edge coloring instances#✓fully proved

An edge coloring 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\) and \(a \ne b\), and \((b, a)\) does not occur in \(E\).

def WellFormed (i : EdgeColoringInstance) : 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 usesEdge coloring instances

Used byEDGE COLORING as a decision problem

DefinitionFeasible edge coloring instances#✓fully proved

Let \((n, E, K)\) be an edge coloring instance with edge list \(E = (e_0, \dots, e_{m-1})\), where the endpoints of a pair \((x, y)\) are \(x\) and \(y\). The instance is feasible when there is a list \((c_0, \dots, c_{m-1})\) of natural numbers with \(c_j < K\) for every \(j\) such that \(c_a \ne c_b\) for all distinct \(a, b < m\) for which \(e_a\) and \(e_b\) share an endpoint.

def EdgeColoringFeasible
    (i : EdgeColoringInstance) : Prop :=
  ∃ coloring : List ℕ, coloring.length = i.2.1.length ∧ (∀ c ∈ coloring, c < i.2.2) ∧
    ∀ a < i.2.1.length, ∀ b < i.2.1.length, a ≠ b →
      ((i.2.1.getD a (0, 0)).1 = (i.2.1.getD b (0, 0)).1 ∨
        (i.2.1.getD a (0, 0)).1 = (i.2.1.getD b (0, 0)).2 ∨
        (i.2.1.getD a (0, 0)).2 = (i.2.1.getD b (0, 0)).1 ∨
        (i.2.1.getD a (0, 0)).2 = (i.2.1.getD b (0, 0)).2) →
      coloring.getD a 0 ≠ coloring.getD b 0

Uses 1 · Used by 1

Statement usesEdge coloring instances

Used byEDGE COLORING as a decision problem

DefinitionEDGE COLORING as a decision problem#✓fully proved

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

noncomputable def edgeColoringDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := EdgeColoringInstance) x with
  | some i => decide (WellFormed i ∧ EdgeColoringFeasible 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 edge coloring instances · Edge coloring instances · Well-formed edge coloring instances · Decision problems

Used byEDGE COLORING is NP-complete

TheoremEDGE COLORING is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), EDGE COLORING; I. Holyer, "The NP-completeness of edge-coloring" (1981).

Uses 5

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