Graph coloring

KColoring k is the set of graphs, given by a list of vertices and a list of edges, whose declared vertices can be colored with k colors so that adjacent vertices get different colors [Kar72]; ThreeColoring is KColoring 3. Graphs are read through Cslib.Complexity.Graph.toSimpleGraph restricted to the declared vertices (SimpleGraph.induce), and colorings through SimpleGraph.Colorable. Edges with an undeclared endpoint and self-loops are therefore ignored. A graph without declared vertices belongs to every KColoring k, and for k = 0 these are the only members.

A certificate for KColoring k gives each declared vertex k bits, at the position of its first occurrence; the color is the number of set bits, which must be below k.

The reduction SAT.toThreeColoring is the palette, variable and clause gadget construction for 3-colorability, a standard exercise Sipser, Chapter 7. Three palette vertices T, F and B form a triangle; the two literals of each variable form a triangle with B, so they take the colors of T and F in some order. The gadget of a clause is a chain of OR gadgets: its stage 0 is adjacent to T and B, hence colored like F; stage j + 1 is a triangle attached to the output of stage j and to the j-th literal, whose output can take the color of T exactly when one of them does; and the output of the last stage is adjacent to F and B, hence colored like T. Chaining handles clauses of every width, including the empty clause, so the reduction is from SAT; it also reduces ThreeSAT after rejecting clauses with more than three literals.

For k = m + 3 colors, SAT.toKColoring m adds m universal vertices adjacent to every vertex and to each other. They take m colors of their own, and the gadget vertices are colored with the remaining three, so KColoring k is NP-complete for every k ≥ 3.

Main definitions

• Cslib.Complexity.KColoring, Cslib.Complexity.ThreeColoring.
• Cslib.Complexity.KColoring.colorOf, Cslib.Complexity.KColoring.verifier.
• Cslib.Complexity.SAT.toThreeColoring, Cslib.Complexity.SAT.toKColoring.

Main results

• Cslib.Complexity.mem_KColoring_iff: membership as a bounded natural-number coloring.
• Cslib.Complexity.KColoring.isVerifier, Cslib.Complexity.KColoring.mem_NP: KColoring k ∈ NP encGraph for every k.
• Cslib.Complexity.SAT.toThreeColoring_mem_iff: toThreeColoring φ ∈ ThreeColoring ↔ φ ∈ SAT.
• Cslib.Complexity.SAT.computableInPolyTime_toThreeColoring: the reduction is polynomial-time.
• Cslib.Complexity.polyTimeReducible_SAT_ThreeColoring, Cslib.Complexity.polyTimeReducible_ThreeSAT_ThreeColoring, Cslib.Complexity.ThreeColoring_npHard, Cslib.Complexity.ThreeColoring_npComplete: ThreeColoring is NP-complete.
• Cslib.Complexity.SAT.length_toThreeColoring_le: the graph of the 3-coloring reduction has linearly many vertices and edges for clauses of bounded width.
• Cslib.Complexity.SAT.toKColoring_mem_iff: toKColoring m φ ∈ KColoring (m + 3) ↔ φ ∈ SAT.
• Cslib.Complexity.polyTimeReducible_SAT_KColoring, Cslib.Complexity.KColoring_npHard, Cslib.Complexity.KColoring_npComplete: KColoring k is NP-complete for k ≥ 3.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability
• R. M. Karp, Reducibility among combinatorial problems
• M. Sipser, Introduction to the Theory of Computation

def Cslib.Complexity.KColoring (k : ℕ) : Set Graph

The graphs whose declared vertices can be colored with k colors, adjacent vertices getting different colors [Kar72].

@[reducible, inline]

abbrev Cslib.Complexity.ThreeColoring : Set Graph

The graphs whose declared vertices can be colored with three colors, adjacent vertices getting different colors Sipser, Chapter 7.

theorem Cslib.Complexity.mem_KColoring_iff {k : ℕ} {G : Graph} : G ∈ KColoring k ↔ ∃ (c : ℕ → ℕ), (∀ v ∈ G.vertices, c v < k) ∧ ∀ u ∈ G.vertices, ∀ v ∈ G.vertices, G.toSimpleGraph.Adj u v → c u ≠ c v

Membership in KColoring k as a coloring by natural numbers below k.

The verifier

def Cslib.Complexity.KColoring.colorOf (k : ℕ) (V : List ℕ) (w : List Bool) (v : ℕ) : ℕ

The color of v described by the certificate w: the number of set bits among the k bits of w from position k * i on, where i is the first occurrence of v in V.

def Cslib.Complexity.KColoring.verifier (k : ℕ) (x : Graph × List Bool) : Bool

The verifier for KColoring k: every declared vertex gets a color below k from the certificate, and no two adjacent declared vertices get the same color.

theorem Cslib.Complexity.KColoring.isVerifier (k : ℕ) : IsVerifier encGraph (Polynomial.C k * Polynomial.X) (verifier k) (KColoring k)

KColoring.verifier k verifies KColoring k with certificates of k bits per symbol of the encoded graph.

theorem Cslib.Complexity.KColoring.computableInPolyTime_colorOf (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (List ℕ × List Bool) × ℕ) => colorOf k p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encUnary

Reading a color from a certificate is polynomial-time, with the color in unary.

theorem Cslib.Complexity.KColoring.computableInPolyTime_verifier (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (verifier k) (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The KColoring k verifier is polynomial-time.

theorem Cslib.Complexity.KColoring.mem_NP (k : ℕ) : KColoring k ∈ NP encGraph

KColoring k belongs to NP.

The gadget graph

def Cslib.Complexity.SAT.paletteVertex (c : ℕ) : ℕ

The palette vertex of color c: color 0 reads true, 1 reads false and 2 is the base color.

def Cslib.Complexity.SAT.literalVertex (φ : Logic.PL.CNF ℕ) (l : Logic.PL.Literal ℕ) : ℕ

The vertex of a literal of φ, numbered by the first occurrence of its variable in φ.

def Cslib.Complexity.SAT.gadgetVertex (i j r : ℕ) : ℕ

Vertex r of stage j of the gadget of clause i; vertex 2 is the output of the stage.

def Cslib.Complexity.SAT.variableEdges (φ : Logic.PL.CNF ℕ) (x : ℕ) : List (ℕ × ℕ)

The edges between the two literals of the variable x and the base palette vertex.

def Cslib.Complexity.SAT.stageEdges (φ : Logic.PL.CNF ℕ) (i j : ℕ) (l : Logic.PL.Literal ℕ) : List (ℕ × ℕ)

Stage j + 1 of the gadget of clause i: a triangle attached to the output of stage j and to the literal l.

def Cslib.Complexity.SAT.clauseEdges (φ : Logic.PL.CNF ℕ) (i : ℕ) (c : Logic.PL.Clause ℕ) : List (ℕ × ℕ)

The gadget of the clause c with index i: the output of stage 0 is adjacent to the true and base palette vertices, one stage follows for each literal, and the output of the last stage is adjacent to the false and base palette vertices.

def Cslib.Complexity.SAT.coloringEdges (φ : Logic.PL.CNF ℕ) : List (ℕ × ℕ)

The edges of the gadget graph of φ: the palette triangle, the variable triangles and the clause gadgets.

def Cslib.Complexity.SAT.toThreeColoring (φ : Logic.PL.CNF ℕ) : Graph

The reduction from SAT to ThreeColoring: the gadget graph of φ, whose declared vertices are the endpoints of its edges.

Correctness of the reduction

theorem Cslib.Complexity.SAT.toThreeColoring_mem_iff (φ : Logic.PL.CNF ℕ) : toThreeColoring φ ∈ ThreeColoring ↔ φ ∈ SAT

Correctness of the 3-coloring reduction. A formula is satisfiable exactly when its gadget graph is 3-colorable.

Polynomial-time reduction

theorem Cslib.Complexity.SAT.computableInPolyTime_toThreeColoring : Turing.MultiTapeTM.ComputableInPolyTime toThreeColoring encCNF encGraph

The reduction toThreeColoring is computable in polynomial time: vertex labels are computed in unary from clause, position and first-occurrence indices, then converted to binary.

Size

theorem Cslib.Complexity.SAT.length_toThreeColoring_le {k : ℕ} {φ : Logic.PL.CNF ℕ} (hφ : ∀ c ∈ φ, List.length c ≤ k) : (toThreeColoring φ).vertices.length + (toThreeColoring φ).edges.length ≤ (24 * k + 12) * List.length φ + 9

The 3-coloring reduction has linear size. On formulas with m clauses of at most k literals, the graph of SAT.toThreeColoring has at most (24 k + 12) m + 9 vertices and edges in total, counted as listed.

More colors

def Cslib.Complexity.SAT.universalVertex (r : ℕ) : ℕ

The r-th universal vertex of the reduction to KColoring (m + 3).

def Cslib.Complexity.SAT.kColoringEdges (m : ℕ) (φ : Logic.PL.CNF ℕ) : List (ℕ × ℕ)

The edges of the gadget graph of φ together with m universal vertices, each adjacent to every vertex of the gadget graph and to the other universal vertices.

def Cslib.Complexity.SAT.toKColoring (m : ℕ) (φ : Logic.PL.CNF ℕ) : Graph

The reduction from SAT to KColoring (m + 3): the gadget graph of φ with m universal vertices, which take m colors of their own.

theorem Cslib.Complexity.SAT.toKColoring_mem_iff (m : ℕ) (φ : Logic.PL.CNF ℕ) : toKColoring m φ ∈ KColoring (m + 3) ↔ φ ∈ SAT

Correctness of the (m + 3)-coloring reduction. A formula is satisfiable exactly when its gadget graph with m universal vertices is (m + 3)-colorable.

theorem Cslib.Complexity.SAT.computableInPolyTime_toKColoring (m : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (toKColoring m) encCNF encGraph

The reduction toKColoring m is computable in polynomial time for every fixed m.

theorem Cslib.Complexity.polyTimeReducible_SAT_ThreeColoring : PolyTimeReducible encCNF encGraph SAT ThreeColoring

SAT reduces to ThreeColoring in polynomial time via SAT.toThreeColoring.

theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_ThreeColoring : PolyTimeReducible encCNF encGraph ThreeSAT ThreeColoring

ThreeSAT reduces to ThreeColoring in polynomial time: a formula with a clause of more than three literals is mapped to the gadget graph of the empty clause, which is not 3-colorable.

theorem Cslib.Complexity.ThreeColoring_npHard : NPHard encGraph ThreeColoring

ThreeColoring is NP-hard.

theorem Cslib.Complexity.ThreeColoring_npComplete : NPComplete encGraph ThreeColoring

ThreeColoring is NP-complete Garey and Johnson.

theorem Cslib.Complexity.polyTimeReducible_SAT_KColoring {k : ℕ} (hk : 3 ≤ k) : PolyTimeReducible encCNF encGraph SAT (KColoring k)

For k ≥ 3, SAT reduces to KColoring k in polynomial time via SAT.toKColoring (k - 3).

theorem Cslib.Complexity.KColoring_npHard {k : ℕ} (hk : 3 ≤ k) : NPHard encGraph (KColoring k)

For k ≥ 3, KColoring k is NP-hard.

theorem Cslib.Complexity.KColoring_npComplete {k : ℕ} (hk : 3 ≤ k) : NPComplete encGraph (KColoring k)

For k ≥ 3, KColoring k is NP-complete Garey and Johnson.