3-coloring a graph with propositional formulas I am trying to tackle a specific problem so any help would be greatly appreciated:

Let $G = (V,E)$ be an undirected graph with vertex set $V$ and edge set $E$. A 3-coloring of $G$ is a map $\chi:V\to \{R,G,Y\}$ such that if $\{x,y\}\in E$ then $\chi(x)\neq \chi(y)$. (Let $R,G,Y$ stand for red, blue, and yellow respectively).
Suppose $n &gt; 1$ and let $V_n = \{0,1,\cdots,n-1\}$ and let $G_n = (V_n,E_n)$ be an undirected graph with vertex set $V_n$. For each $i$, $0 \leq i &lt; n$ let $R_i,B_i,Y_i$ be propositional variables. We can think of $i$ being a node so $R_i$ says node $i$ has a color of red.
Give a propositional formula $A_n$ using the variables $\{R_i,B_i,Y_i | 0 \leq i &lt; n\}$ such that $A_n$ is satisfiable iff $G_n$ has a 3-coloring. Do this in such a way that $A_n$ can be computed efficiently from $G_n$ (e.g. don't define $A_n$ to be $R_1$ if $G_n$ has a three coloring and ($R_1 \wedge \neg R_1$) otherwise).

My inclination for a question like this is to set up some sort of CNF formula, that is come up with a set of clauses that set out to take care of different properties. For instance I believe for something like this I need a clause that deals with the case that every node has a color, maybe one that deals with every node cannot have more than one color, and that every node cannot be the same color as an adjacent node? I am not really sure how to illustrate that last one or if there are cases that I am missing.
Hint: Try to formalize the following:


Every node has at least one color.
Every node has at most one color. (This is actually not necessary.)
Any two adjacent nodes cannot have the same color.


Another hint:


   The first can be formalized as $R_i \lor B_i \lor Y_i$ for all $i$.