# The optimized numbers of variables and clauses to encode a graph coloring problem in CNF

## Problem Statement

Given a finite graph $$G = \langle V, E\rangle$$, consisting of vertice set $$V$$ and edge set $$E$$, and a finite set of colors $$C$$, a problem instance of graph coloring is to assign each vertex $$v \in V$$ a $$\text{color} (v) \in C$$ such that $$\forall \langle v, w\rangle \in E, \text{color}(v) \not= \text{color}(w)$$. Now we encode an instance of graph coloring problem into a CNF (conjunctive normal formula) $$F$$.

Note: The word "encode" means that we'll know a graph coloring problem if a CNF is given, and also will know a CNF if a graph coloring problem is given.

• What is the minimal number of propositional variables in $$F$$?
• What is the minimal number of clauses in $$F$$?

## Original Version

A solution to a graph coloring problem is an assignment of colors to vertices such that no two adjacent vertices have the same color. Formally, a finite graph $$G = \langle V, E\rangle$$ consists of vertices $$V = \{v_1, \cdots, v_n\}$$ and edges $$E = \{ \langle v_{i_1} , w_{i_1} \rangle , \cdots , \langle v_{i_k} , w_{i_k} \rangle \}$$. The finite set of colors is given by $$C = \{c_1, \cdots , c_m \}$$. A problem instance is given by a graph and a set of colors: the problem is to assign each vertex $$v \in V$$ a $$\text{color}(v) \in C$$ such that for every edge $$\langle v, w\rangle \in E$$, $$\text{color}(v) \not= \text{color}(w)$$. Clearly, not all instances have solutions.

Show how to encode an instance of a graph coloring problem into a PL formula $$F$$. $$F$$ should be satisfiable iff a graph coloring exists.

1. Describe a set of constraints in PL asserting that every vertex is colored. Since the sets of vertices, edges, and colors are all finite, use notation such as “$$\text{color}(v) = c$$” to indicate that vertex $$v$$ has color $$c$$. Realize that such an assertion is encodeable as a single propositional variable $$P^c_v$$.
2. Describe a set of constraints in PL asserting that every vertex has at most one color.
3. Describe a set of constraints in PL asserting that no two connected vertices have the same color.
4. Identify a significant optimization in this encoding. Hint: Can any constraints be dropped? Why?
5. If the constraints are not already in CNF, specify them in CNF now. For $$N$$ vertices, $$K$$ edges, and $$M$$ colors, how many variables does the optimized encoding require? How many clauses?

As suggested by @D.W.♦, I copy the original problem here (above is the version simplified by me). This original version is Exercise 1.6 from:

Bradley, A. and Manna, Z. (2007). The Calculus of Computation. Dordrecht: Springer, p.34.

## My Analysis

The optimized CNF within my ability is to use propositional variable $$P_v^c$$ to indicate that $$\text{color}(v) = c$$. Here we can only use at most $$|V|$$ colors of all colors, i.e., the number of colors in our design of propositional variables is $$|V|\min (|V|, |C|)$$. Then we can build a CNF: $$F_0 = \bigwedge_{v \in V} (\bigvee_{c \in C} P_v^c) \wedge \bigwedge_{v \in V} (\bigvee_{c_1 \not= c_2 \in C} (\neg P_v^{c_1} \vee \neg P_v^{c_2})) \land \bigwedge_{c \in C \\ \langle v, w\rangle \in E} (\neg P_v^c \vee \neg P_w^c)$$

In this variable, there're $$|V| \min (|V|, |C|)$$ propositional variables and $$2|V| + |C||E|$$ clauses.

I failed to prove $$F_0$$ is the CNF with neither the least propositional variables nor the least clauses. Is there an another CNF $$F'$$ with less propostional variables or less clauses? How to find the minimal number of propositional variables and clauses of legal CNFs?

• If the 2nd group of terms in $F_0$ is supposed to rule out that a vertex has 2 or more colors, shouldn't the term be $(\bigwedge_{c_1 \not= c_2 \in C} (\neg P_v^{c_1} \vee \neg P_v^{c_2}))$ ( instead of $(\bigvee_{c_1 \not= c_2 \in C} (\neg P_v^{c_1} \wedge \neg P_v^{c_2}))$ ) ? As it stands the duplicity check passes iff for a given vertex there exist 2 [amongst all] colors that are not assigned to that vertex. What you want is that for each triple of vertex and 2 different colors, [at least] one color is not assigned to the vertex. – collapsar Sep 27 at 15:40

If I'm being pedantic, I would say that the minimum number of propositional variables is zero: you can solve the graph coloring problem (taking exponential time if necessary), then either use the formula $$\text{True}$$ or $$\text{False}$$ according to whether the graph is $$C$$-colorable or not. I suspect this isn't what you're looking for, so you probably need to define the problem statement more carefully to be able to answer the question in a useful way. For instance, perhaps you need to specify exactly what properties you want $$F$$ to have.
• And, appologize for my typo of the number propositional variables. In fact, I use $|V| \min (|V|, |C|)$ propositional variables in designed CNF. – namasikanam Sep 28 at 2:56
• @namasikanam, good idea. One can encode a graph coloring problem using $2 |E| \lg |V| + \lg |C|$ bits, so if we don't need the CNF to have any properties (e.g., its satisfiability must be related to the colorability of the graph), then you could encode from there to any family of at least $2^{2 |E| \lg |V| + \lg |C|}$ formulas. For instance, there are $\ge 2^{2^n}$ CNF formulas on $n$ variables, so $\lg (2 |E| \lg |V| + \lg |C|)$ variables should suffice. I question whether this is useful or what is intended, though. – D.W. Sep 29 at 4:05