The last examples we will consider are known as ``clique coloring problems.'' These are derivatives of pigeonhole problems where the exact nature of the pigeonhole problem is obscured. Somewhat more specifically, the problems indicate that a graph includes a clique of nodes (where every node in the clique is connected to every other), and that the graph must be colored in colors. If the graph itself is known to be a clique, the problem is equivalent to the pigeonhole problem. But if we know only that the clique can be embedded into the graph, the problem is more difficult.
In the axiomatization, we use to describe the edges of the
graph, to describe the coloring of the graph, and to
describe the embedding of the cliQue into the graph. The
graph has nodes, the clique is of size , and there are
colors available. So the axiomatization is:
Since there is no polynomially sized resolution proof of the pigeonhole problem in Boolean satisfiability, there is obviously no polynomially sized proof of the clique coloring problems, either. But as we shall see, clique coloring problems can in some cases be used to distinguish among elements of the proof complexity hierarchy.