vertex with $deg(v)={\langle d_1,d_2,d_3 \rangle}$. Then, $d_1+d_2+d_3=n-1$ and $G^1_v$, $G^2_v$, and $G^3_v$ are respectively $(3,3,3;d_1)$, $(4,2,3;d_2)$, and $(4,3,2;d_3)$ colorings.

Note that by definition a $(4,2,3;n)$ coloring is a $(4,3;n)$ Ramsey coloring in colors 1 and 3 and likewise a $(4,3,2;n)$ Ramsey coloring is a $(4,3;n)$ coloring in colors 1 and 2. This is because the “2” specifies that the coloring does not contain a subgraph $K_2$ in the corresponding color and this means that it contains no edge with that color. For $n\in\{14,15,16\}$, the sets ${{\cal R}}(3,3,3;n)$ are known and consist respectively of 115, 2, and 2 colorings. Similarly, for $n\in\{5,6,7,8\}$ the sets ${{\cal R}}(4,3;n)$ are known and consist respectively of 9, 15, 9, and 3 colorings.

In this paper computations are performed using the CryptoMiniSAT [@Crypto] SAT solver. SAT encodings (CNF) are obtained using the finite-domain constraint compiler  [@jair2013]. The use of  facilitates applications to find a single (first) solution, or to find all solutions for a constraint, modulo a specified set of variables. When solving for all solutions, our implementation iterates with the SAT solver, adding so called *blocking clauses* each time another solution is found. This technique, originally due to McMillan [@McMillan2002], is simplistic but suffices for 