Clique covers and colorings of the complement

The vertices of a finite simple graph are the union of at most l cliques exactly when the complement of the graph is l-colorable: the color classes of a coloring of the complement are cliques of the graph, and conversely each vertex may be colored by the index of a clique covering it. This is the correspondence behind Karp's reduction from CHROMATIC NUMBER to CLIQUE COVER [Kar72].

Main results

• SimpleGraph.exists_cliqueCover_iff_colorable_compl: a cover of the vertices by at most l cliques exists exactly when the complement is l-colorable.

References

• R. M. Karp, Reducibility among combinatorial problems

theorem SimpleGraph.exists_cliqueCover_iff_colorable_compl {V : Type u_1} [Finite V] {G : SimpleGraph V} {l : ℕ} : (∃ (S : Finset (Finset V)), S.card ≤ l ∧ (∀ s ∈ S, G.IsClique ↑s) ∧ ∀ (v : V), ∃ s ∈ S, v ∈ s) ↔ Gᶜ.Colorable l

Clique covers are colorings of the complement. The vertices of a finite graph are the union of at most l cliques exactly when its complement is l-colorable.