Clique coloring problems

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 $n+1$ nodes (where every node in the clique is connected to every other), and that the graph must be colored in $n$ 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 $e_{ij}$ to describe the edges of the graph, $c_{ij}$ to describe the coloring of the graph, and $q_{ij}$ to describe the embedding of the cliQue into the graph. The graph has $m$ nodes, the clique is of size $n+1$, and there are $n$ colors available. So the axiomatization is:

$$\neg e_{ij} \vee \neg c_{il} \vee \neg c_{jl} \mbox{for $1\leq i<j\leq m$, $l=1,\dots,n$}$$ (13)

$$c_{i1} \vee \cdots \vee c_{in} \mbox{for $i=1,\dots,m$}$$ (14)

$$q_{i1} \vee \cdots \vee q_{im} \mbox{for $i=1,\dots,n+1$}$$ (15)

$$\neg q_{ij} \vee \neg q_{kj} \mbox{for $1\leq i<k\leq n+1$, $j=1,\dots,m$}$$ (16)

$$e_{ij} \vee \neg q_{ki} \vee \neg q_{lj} \mbox{for $1\leq i<j\leq m$, $1\leq k \neq l \leq n+1$}$$ (17)

Here $e_{ij}$ means that there is an edge between graph nodes $i$ and $j$, $c_{ij}$ means that graph node $i$ is colored with the $j$th color, and $q_{ij}$ means that the $i$th element of the clique is mapped to graph node $j$. Thus the first axiom (13) says that two of the $m$ nodes in the graph cannot be the same color (of the $n$ colors available) if they are connected by an edge. (14) says that every graph node has a color. (15) says that every element of the clique appears in the graph, and (16) says that no two elements of the clique map to the same node in the graph. Finally, (17) says that the clique is indeed a clique - no two clique elements can map to disconnected nodes in the graph.

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.