To facilitate the search for $(4,3,3;30)$ Ramsey coloring using a SAT encoding, we apply a general approach where, when seeking a $(r_1,\ldots,r_k;n)$ Ramsey coloring one selects a “preferred” vertex, call it $v_1$, and based on its degrees in each of the $k$ colors, embeds $k$ subgraphs which are corresponding smaller colorings. Using this approach, we apply Corollary \[cor:degrees\] and Observation \[obs:embed\] to establish that a $(4,3,3;30)$ coloring, if one exists, must be ${\langle 13,8,8 \rangle}$ regular. Specifically, all vertices must have 13 edges in the first color and 8 each, in the second and third colors. This result is considered significant progress in the research on Ramsey numbers [@XuRad2015]. This “embedding” approach is often applied in the Ramsey number literature where the process of completing (or trying to complete) a partial solution (an embedding) to a Ramsey coloring is called *gluing*. See for example the presentations in [@PiwRad2001; @FKRad2004; @PR98].

\[thm:regular\] Any $(4,3,3;30)$ coloring, if one exists, is ${\langle 13,8,8 \rangle}$ regular.

By computation as described in the rest of this section.

[r]{}[.460]{}

We seek a $(4,3,3;30)$ coloring of $K_{30}$, represented as a $30\times 30$ adjacency matrix $A$. Let $v_1$ correspond to the the first row in $A$ with $deg(v_1)={\langle 