Normal colorings of cubic graphs to SAT
Start with $5|E(G)|$ variables $x_{e,i}$, one for each $e \in E(G)$ and $i \in \{1,2,3,4,5\}$. Intuitively $x_{e,i}$ means that edge $e$ is colored with color $i$.

A CNF formula $\phi$ can be obtained by the logical and of the following sub-formulas.

Each edge must have exactly one color:


At least one color, for each $e \in E(G)$:
$(x_{e,1} \vee x_{e,2} \vee x_{e,3} \vee x_{e,4} \vee x_{e,5})$
At most one color, for each $e \in E$, and $i,j \in \{1,2,3,4,5\}$ with $i&lt;j$:
$(\overline{x_{e,i}} \vee \overline{x_{e,j}})$


The coloring must be proper:


For each pair $e,f \in E(G)$ of adjacent edges and for each $i \in \{1,2,3,4,5\}$:
$(\overline{x_{e,i}} \vee \overline{x_{f,i}} )$


If $e=(u,v)$ is an edge of $G$, let $f^e_1,f^e_2$ be the two edges other than $e$ that are incident to $u$, and $f^e_3,f^e_4$ be the two edges other then $e$ that are incident to $v$.


For each $e \in E(G)$ add a new variable $r_e$. This will encode "if $e$ is not rich, then $r_e$ is true": Notice that if $e$ is rich then $r_e$ can always be set to false.
For every $i \in \{1,2,3,4,5\}$, every $j \in \{1,2\}$, and every $k \in \{3,4\}$:
$(r_e \vee \overline{x_{f^e_j, i}} \vee \overline{x_{f^e_k, i}})$
For each $e \in E(G)$ add a new variable $p_e$. This will encode "if e is not poor, then p_e is true". Notice that if $e$ is poor then $p_e$ can always be set to false.
For every ordered tuple $(j, k, h)$ of $3$ distinct elements from $\{1,2,3,4,5\}$:
$( p_e \vee \overline{x_{f_1,j}} \vee  \overline{x_{f_2,k}} \vee \overline{x_{f_3,h}}) 
\wedge 
( p_e \vee  \overline{x_{f_1,j}} \vee  \overline{x_{f_2,k}} \vee \overline{x_{f_4,h}}) 
\wedge
( p_e \vee  \overline{x_{f_1,j}} \vee  \overline{x_{f_3,k}} \vee \overline{x_{f_4,h}}) 
\wedge
( p_e \vee \overline{x_{f_2,j}} \vee  \overline{x_{f_3,k}} \vee \overline{x_{f_4,h}}) 
$


Finally, this will encode "e is rich or e is poor":


For every $e \in E(G)$: $(\overline{r_e} \vee \overline{p_e})$




If you have a satisfying truth assignment for $\phi$ then you can color edge $e \in E(G)$ with color $i$ iff $x_{e,i}$ is true.

If you have a coloring then let $c(e) \in \{1,2,3,4,5\}$ be the color of edge $e$. You an get a satisfying truth assignment for $\phi$ by setting:


$x_{e,c(e)}= \top$, and $x_{e,j} = \bot$ for $j \in \{1,2,3,4,5\} \setminus \{ c(e) \}$,
$r_e = \bot$ iff edge $e$ is rich,
$p_e = \bot$ iff edge $e$ is poor.