This problem is related to ”Normal coloring of cubic graphs (part 1) - a previous post. We repeat the definitions, slightly modified so as to get to the point (we define normal edge 5 colorability, rather than the more general normal edge $k$ colorability).
Definition A normal edge 5 coloring (or normal 5 coloring) of a cubic graph $G$ is a proper coloring of the edges with 5 colors, so that for any edge $e\in E(G)$, the four edges adjacent to $e$ are colored with two colors, or with four colors.
Thus, an edge $e$ and its four adjacent edges might utilize three colors, or five colors.
If three colors are used, $e$ is called poor, and if five colors are used, $e$ is called rich.
Question I would like to know how to transform an instance of this problem to a CNF formula. That is, given a graph $G$, produce a CNF formula, such that a satisfying assignment can be translated back to a normal 5 coloring of the graph.
Note that working with the line graph of the cubic graph, as one would in dealing with a typical edge coloring problem, is a bit tricky (and that is all I dare to say).
Please advise if this question would be better off if posted in the theoretical computer science pages. Thanks in advance.