3.1.12. cnfgen.families.cliquecoloring module

Implementation of the clique-coloring formula

CliqueColoring(n, k, c)

Clique-coloring CNF formula

The formula claims that a graph \(G\) with \(n\) vertices simultaneously contains a clique of size \(k\) and a coloring of size \(c\).

If \(k = c + 1\) then the formula is clearly unsatisfiable, and it is the only known example of a formula hard for cutting planes proof system. [1]

Variables \(e_{u,v}\) to encode the edges of the graph.

Variables \(q_{i,v}\) encode a function from \([k]\) to \([n]\) that represents a clique.

Variables \(r_{v,\ell}\) encode a function from \([n]\) to \([c]\) that represents a coloring.

Parameters:

n : number of vertices in the graph

k : size of the clique

c : size of the coloring

Returns:

A CNF object

References

[1]	Pavel Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic (1997)