a circulant $(3,4,4;29)$ coloring. Encoding instance $\varphi_{(4,3,3;29)}(A)$ of Constraint (\[constraint:coloring\]) together with a constraint that states that the adjacency matrix $A$ is circulant, results in a CNF with 146[,]{}506 clauses and 8[,]{}394 variables. Using a SAT solver, we obtain a corresponding $(4,3,3;29)$ coloring in less than two seconds of computation time. The solution is ${\langle 12,8,8 \rangle}$ regular and isomorphic to the adjacency matrix depicted as Figure \[embed\_12\_8\_8\]. Now we apply the embedding approach. We take the partial solution (the boldface elements) corresponding to the three subgraphs: $G^1_{v_1}$, $G^2_{v_1}$ and $G^3_{v_1}$ which are respectively $(3,3,3;12)$, $(4,2,3;8)$ and $(4,3,2;8)$ Ramsey colorings. Applying a SAT solver to complete this partial solution to a $(4,3,3;29)$ coloring satisfying Constraint (\[constraint:coloring\]) involves a CNF with 30[,]{}944 clauses and 4[,]{}736 variables and requires under two hours of computation time. Figure \[embed\_12\_8\_8\] portrays the solution (the gray elements).

To apply the embedding approach described in this section to determine if there exists a $(4,3,3;30)$ Ramsey coloring which is ${\langle 13,8,8 \rangle}$ regular would require access to the set ${{\cal R}}(3,3,3;13)$. We defer this discussion until after Section \[sec:33313b\] where we describe how we compute the set of all 78[,]{}892 $(3,3,3;13)$ Ramsey colorings modulo weak isomorphism.

Symmetry Breaking: 