pub fn clique_coloring(n: usize, k: usize) -> (DimacsCnf, ExpectedVerdict)Expand description
Graph k-coloring of the complete graph K_n — the canonical color-permutation symmetry
family (the color group S_k acts, on top of the vertex group S_n). It is unsatisfiable
exactly when k < n (a clique of size n needs n colors). The variable “vertex v takes
color c” lives at index v*k + c.