Chromatic number

ChromaticNumber is Karp's problem CHROMATIC NUMBER [Kar72]: given a graph G and a number k, the declared vertices of G can be colored with k colors so that adjacent vertices get different colors. It is KColoring k with the number of colors moved into the instance (Cslib.Complexity.ChromaticNumberInstance, encoded by Cslib.Complexity.encChromaticNumber). The graph of the declared vertices has chromatic number at most k in the sense of SimpleGraph.chromaticNumber (Cslib.Complexity.mem_ChromaticNumber_iff_chromaticNumber_le). Equivalently, by Mathlib's SimpleGraph.partitionable_iff_colorable, that graph is partitioned into at most k independent sets (SimpleGraph.Partitionable).

NP membership uses a list of colors as the witness, the color of a vertex being the entry at its first occurrence among the declared vertices (Cslib.Complexity.colorOf). Since k is written in binary, a coloring of a member is first replaced by one with colors below the number of declared vertices, so that witnesses have length polynomial in the instance: when k exceeds the number of declared vertices, every vertex is colored by its position.

Karp proves hardness by a reduction from SATISFIABILITY WITH AT MOST 3 LITERALS PER CLAUSE. Here ChromaticNumber is NP-hard because the NP-hard ThreeColoring is the instances with three colors (Cslib.Complexity.polyTimeReducible_KColoring_ChromaticNumber).

Main definitions

• Cslib.Complexity.ChromaticNumberInstance: instance (graph, colors) of Chromatic Number.
• Cslib.Complexity.encChromaticNumber: polynomial-time encoding of ChromaticNumberInstance.
• Cslib.Complexity.ChromaticNumber: graphs with a number of colors that suffices.

Main results

• Cslib.Complexity.mem_ChromaticNumber_iff_chromaticNumber_le: membership bounds the chromatic number of the graph of the declared vertices.
• Cslib.Complexity.ChromaticNumber.mem_NP: ChromaticNumber ∈ NP encChromaticNumber.
• Cslib.Complexity.polyTimeReducible_KColoring_ChromaticNumber, Cslib.Complexity.ChromaticNumber_npHard, Cslib.Complexity.ChromaticNumber_npComplete: ChromaticNumber is NP-complete.

References

• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.ChromaticNumberInstance : Type

An instance (graph, colors) of Chromatic Number.

• graph : Graph

  The graph to be colored.

• colors : ℕ

  The maximum number of colors allowed.

theorem Cslib.Complexity.ChromaticNumberInstance.ext_iff {x y : ChromaticNumberInstance} : x = y ↔ x.graph = y.graph ∧ x.colors = y.colors

theorem Cslib.Complexity.ChromaticNumberInstance.ext {x y : ChromaticNumberInstance} (graph : x.graph = y.graph) (colors : x.colors = y.colors) : x = y

def Cslib.Complexity.instDecidableEqChromaticNumberInstance.decEq (x✝ x✝¹ : ChromaticNumberInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqChromaticNumberInstance : DecidableEq ChromaticNumberInstance

@[instance_reducible]

instance Cslib.Complexity.instReprChromaticNumberInstance : Repr ChromaticNumberInstance

def Cslib.Complexity.instReprChromaticNumberInstance.repr : ChromaticNumberInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instInhabitedChromaticNumberInstance : Inhabited ChromaticNumberInstance

theorem Cslib.Complexity.encChromaticNumber_graph_inO : Turing.MultiTapeTM.ComputableInO ChromaticNumberInstance.graph encChromaticNumber encGraph (fun (a : ChromaticNumberInstance) => (encChromaticNumber a).length) fun (a : ChromaticNumberInstance) => (encChromaticNumber a).length

def Cslib.Complexity.encChromaticNumber : ChromaticNumberInstance ↪ List Bool

Encoding of ChromaticNumberInstance as a pair (graph, colors).

theorem Cslib.Complexity.encChromaticNumber_graph_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → ChromaticNumberInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encChromaticNumber S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph S✝

@[simp]

theorem Cslib.Complexity.encChromaticNumber_apply (a : ChromaticNumberInstance) : encChromaticNumber a = encChromaticNumberFields (a.graph, a.colors)

theorem Cslib.Complexity.encChromaticNumber_colors_inO : Turing.MultiTapeTM.ComputableInO ChromaticNumberInstance.colors encChromaticNumber Turing.MultiTapeTM.encNat (fun (a : ChromaticNumberInstance) => (encChromaticNumber a).length) fun (a : ChromaticNumberInstance) => (encChromaticNumber a).length

theorem Cslib.Complexity.encChromaticNumber_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encGraph) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { graph := x0 x, colors := x1 x }) encIn encChromaticNumber

theorem Cslib.Complexity.encChromaticNumber_graph_deg : Turing.MultiTapeTM.ComputableInDegree ChromaticNumberInstance.graph encChromaticNumber encGraph 1 1

theorem Cslib.Complexity.encChromaticNumber_colors_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → ChromaticNumberInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encChromaticNumber → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).colors) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encChromaticNumber_colors_deg : Turing.MultiTapeTM.ComputableInDegree ChromaticNumberInstance.colors encChromaticNumber Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encChromaticNumber_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : ChromaticNumberInstance) => (a.graph, a.colors)) encChromaticNumber encChromaticNumberFields 1 1

theorem Cslib.Complexity.encChromaticNumber_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encGraph T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { graph := x0 x, colors := x1 x }) encIn encChromaticNumber (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encChromaticNumber_colors_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → ChromaticNumberInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encChromaticNumber S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).colors) encIn✝ Turing.MultiTapeTM.encNat S✝

@[reducible, inline]

abbrev Cslib.Complexity.encChromaticNumberFields : Graph × ℕ ↪ List Bool

The tuple of the fields of encChromaticNumber.

theorem Cslib.Complexity.encChromaticNumber_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ) => { graph := p.1, colors := p.2 }) encChromaticNumberFields encChromaticNumber 1 1

theorem Cslib.Complexity.encChromaticNumber_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encGraph budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { graph := x0 x, colors := x1 x }) encIn encChromaticNumber budget

theorem Cslib.Complexity.encChromaticNumber_graph_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → ChromaticNumberInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encChromaticNumber → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph

def Cslib.Complexity.ChromaticNumber : Set ChromaticNumberInstance

Chromatic number [Kar72]: the graphs whose declared vertices can be colored with the given number of colors so that adjacent vertices get different colors. Unlike KColoring k, the number of colors is part of the instance.

@[simp]

theorem Cslib.Complexity.mem_ChromaticNumber_iff {G : Graph} {k : ℕ} : { graph := G, colors := k } ∈ ChromaticNumber ↔ G ∈ KColoring k

Membership in ChromaticNumber is membership in KColoring with the given number of colors.

theorem Cslib.Complexity.mem_ChromaticNumber_iff_chromaticNumber_le {G : Graph} {k : ℕ} : { graph := G, colors := k } ∈ ChromaticNumber ↔ G.induced.chromaticNumber ≤ ↑k

Membership in ChromaticNumber bounds the chromatic number of the graph induced on the declared vertices (SimpleGraph.chromaticNumber).

theorem Cslib.Complexity.ChromaticNumber.mem_NP : ChromaticNumber ∈ NP encChromaticNumber

ChromaticNumber belongs to NP, with a list of colors as the witness. Colors are taken below the number of declared vertices, so witnesses stay polynomial although the number of colors is written in binary.

theorem Cslib.Complexity.polyTimeReducible_KColoring_ChromaticNumber (k : ℕ) : PolyTimeReducible encGraph encChromaticNumber (KColoring k) ChromaticNumber

KColoring k reduces to ChromaticNumber in polynomial time, by attaching the number of colors k to the graph.

theorem Cslib.Complexity.ChromaticNumber_npHard : NPHard encChromaticNumber ChromaticNumber

ChromaticNumber is NP-hard, already for three colors.

theorem Cslib.Complexity.ChromaticNumber_npComplete : NPComplete encChromaticNumber ChromaticNumber

Chromatic number is NP-complete, with the number of colors in binary [Kar72].