3-colorability: definition

A (directed) graph is a FirstOrder.Language.graph-structure (already in Mathlib); DescriptiveComplexity.ThreeColorable is properness of some 3-coloring, and DescriptiveComplexity.ThreeCol the bundled decision problem. On structures arising from Mathlib's SimpleGraph this agrees with SimpleGraph.Colorable (DescriptiveComplexity.threeColorable_iff_colorable).

The reductions to and from SAT, and NP-completeness, are in DescriptiveComplexity.Problems.ThreeColorability.

def DescriptiveComplexity.ThreeColorable (V : Type) [FirstOrder.Language.graph.Structure V] : Prop

A Language.graph-structure is 3-colorable if the vertices can be colored with 3 colors so that adjacent vertices get distinct colors. (On structures with self-loops this is never satisfiable, matching the usual convention.)

Equations

• DescriptiveComplexity.ThreeColorable V = ∃ (c : V → Fin 3), ∀ (x y : V), FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] → c x ≠ c y

theorem DescriptiveComplexity.threeColorable_iso {A B : Type} [FirstOrder.Language.graph.Structure A] [FirstOrder.Language.graph.Structure B] (e : FirstOrder.Language.graph.Equiv A B) : ThreeColorable A ↔ ThreeColorable B

3-colorability is isomorphism-invariant.

def DescriptiveComplexity.ThreeCol : DecisionProblem FirstOrder.Language.graph

3-colorability, as a problem on Language.graph-structures.

Equations

• DescriptiveComplexity.ThreeCol = { Holds := fun (V : Type) (inst : FirstOrder.Language.graph.Structure V) => DescriptiveComplexity.ThreeColorable V, iso_invariant := ⋯ }

theorem DescriptiveComplexity.threeColorable_iff_colorable {V : Type} (G : SimpleGraph V) : ThreeColorable V ↔ G.Colorable 3

On the first-order structure associated to a simple graph, ThreeColorable coincides with Mathlib's SimpleGraph.Colorable 3.