The optimized numbers of variables and clauses to encode a graph coloring problem in CNF
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.