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.


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$.
Describe a set of constraints in PL asserting that every vertex has at most
one color.
Describe a set of constraints in PL asserting that no two connected vertices
have the same color.
Identify a significant optimization in this encoding. Hint: Can any constraints be dropped? Why?
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?
The problem statement needs to be specified more precisely to be meaningful.

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.