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

Question

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?