Modelling colorability in propositional logic

Colorability of a graph can be easily modelled in propositional logic.

Let $G$ denote an undirected graph and $V$ and $E$ its sets of vertices and edges, respectively. A coloring with $k$ colors is a function $V \to \{0, \dots, k-1\}$. Such a function assigns to each vertex exactly one out of $k$ colors, named $0, \dots, k-1$.

Such a coloring is a $k$-coloring if adjacent vertices are assigned distinct colors. Formally, if $c$ is a coloring with $k$ colors, then it is a $k$-coloring if $c(u) \neq c(v)$ for all $\{u,v\} \in E$.

In the following, we only deal with finite graphs.

Example The illustration below shows a graph with four vertices and a coloring with two colors. Formally, the coloring is $\{0 \mapsto 0, 1 \mapsto 1, 2 \mapsto 0, 3 \mapsto 1\}$. Obviously, this is a 2-coloring.

There is no 1-coloring of this graph.

Example The illustration below shows a triangle and a coloring with two colors. Formally, the coloring is $\{0 \mapsto 0, 1 \mapsto 1, 2 \mapsto 0\}$. Obviously, this is not a 2-coloring, because the graph has the edge $\{0, 2\}$ and both vertices incident with this edge have the same color.

There is no 2-coloring of this graph.

Two colors

A coloring of a graph with vertex set $\{0, \dots, n-1\}$ is a function $\{0, \dots, n-1\} \to \{0,1\}$. Such a function can be thought of as a partial variable assignment $\{X_0, \dots, X_{n-1}\} \to \{0,1\}$. In other words, a coloring with two colors is represented by a variable assignment on $\{X_0, \dots, X_{n-1}\}$, and vice versa.

Example The partial assignment representing the coloring in the first example is $\{X_0 \mapsto 0, X_1 \mapsto 1, X_2 \mapsto 0, X_3 \mapsto 1\}$, the one for the second example is $\{X_0 \mapsto 0, X_1 \mapsto 1, X_2 \mapsto 0\}$.

The condition that vertices $i$ and $j$ are colored with distinct colors can be expressed as $X_i \not\leftrightarrow X_j$. So when we assume that the edge of a graph is given as $\{\{i_0,j_0\}, \dots, \{i_{m-1}, j_{m-1}\}\}$, then the 1-assignments on $\{X_0, \dots, X_{n-1}\}$ of the formula $\varphi_G$ defined by \begin{align} \varphi_G = \bigwedge_{k<m} (X_{i_k} \not\leftrightarrow X_{j_k}) \end{align} represent exactly the 2-colorings of the given graph.

Example The following is a formula for the first example: $$(X_0 \not\leftrightarrow X_1) \wedge (X_1 \not\leftrightarrow X_2) \wedge (X_2 \not\leftrightarrow X_3) \wedge (X_3 \not\leftrightarrow X_0) \enspace.$$ And $$(X_0 \not\leftrightarrow X_1) \wedge (X_1 \not\leftrightarrow X_2) \wedge (X_2 \not\leftrightarrow X_0)$$ is a formula for the second example.

Here is one more example:

Example Consider the graph depicted below. We obtain the following formula: $$(X_0 \not\leftrightarrow X_1) \wedge (X_0 \not\leftrightarrow X_2) \wedge (X_1 \not\leftrightarrow X_4) \wedge (X_2 \not\leftrightarrow X_4) \wedge (X_1 \not\leftrightarrow X_3) \wedge (X_1 \not\leftrightarrow X_5) \wedge (X_3 \not\leftrightarrow X_5) \enspace.$$

Four colors

Modelling 4-colorability is somewhat more complicated.

Again, assume a graph with vertex set $\{0, \dots, n-1\}$ is given. Then a coloring with four colors is a function $\{0, \dots, n-1\} \to \{0,1,2,3\}$. Since the numbers from the latter set correspond to two-bit numbers, such a coloring can be represented by a partial assignment $\{X_0, \dots, X_{2n-1}\} \to \{0,1\}$. More precisely, a coloring $c$ can be represented by the assignment $\beta_c \colon \{X_0, \dots, X_{2n-1}\} \to \{0,1\}$ defined by $\beta(X_{2i}) = c(i) \text{ div } 2$ and $\beta(X_{2i+1}) = c(i) \text{ rem } 2$, for every $i<n$. Conversely, a variable assignment $\beta \colon \{X_0, \dots, X_{2n-1}\} \to \{0,1\}$ represents the coloring $c_\beta$ defined by $c(i) = 2 \beta(X_{2i}) + \beta(X_{2i+1})$.

Example When we have $\beta(X_6) = 1$ and $\beta(X_7) = 0$, then this means that vertex $3$ is colored with $1 \cdot 2 + 0 = 2$. When we have $\beta(X_8) = 1$ and $\beta(X_9) = 1$, then this means vertex $4$ is colored with $1 \cdot 2 + 1 = 3$.

That a coloring with four colors is a 4-coloring now translates into a formula which, for every edge, expresses that the vertices incident to it are colored with distinct colors. Since these colors are each respresented by two bits, the formula expresses that there is at least one bit which is different in the representation of the two colors. For instance, if $i$ and $j$ are adjacent, then the formula $$(X_{2i} \not\leftrightarrow X_{2j}) \vee (X_{2i+1} \not\leftrightarrow X_{2j+1})$$ can be used.

In complete analogy to above, a formula for the entire graph is $\varphi_G$ defined by $$\varphi_G = \bigwedge_{k < m} ((X_{2i_k} \not\leftrightarrow X_{2j_k}) \vee (X_{2i_k+1} \not\leftrightarrow X_{2j_k+1})) \enspace.$$

Three colors

The case of three colors is more complicated than the one of two or the one of four colors, because there is no straightforward way of respresenting colorings as variable assignments: with $n$ vertices there are $3^n$ colorings, but there are $2^m$ partial assignments on $m$ variables; equality only holds for $m=n=0$.

The idea for the modelling of 3-colorability is to proceed as with four colors but to disallow one of the colors. Clearly, we want to disallow the number 3. So we simply rule out corresponding assignments. This is accomplished by the formula $\chi$ defined by $$\chi = \bigwedge_{i<n} \neg (X_{2i} \wedge X_{2i+1}) \enspace.$$ We can state that a 1-assignment on $\{X_0, \dots, X_{2n-1}\}$ of $\chi$ represents a coloring with 3 colors, and vice versa.

Overall, we can use $$\chi \wedge \varphi\enspace,$$ with $\varphi$ from above, for representing all 3-colorings of the given graph.

More than four colors and an infinite number of vertices

When there are more than four colors, the ideas from above can be used to model colorability in propositional logic. There are two standard ways to do this: for each vertex one uses as many variables as there are colors; for each vertex one uses $\lceil \log_2 k \rceil$ variables when $k$ denotes the number of colors.

When the number of vertices is infinite (and the number of colors is still finite), one can replace the formulas $\varphi$ and $\chi$ by sets of formulas, because these formulas are infinite conjunctions of finite formulas.