Computing ${{\cal R}}(r_1,\ldots,r_k;n)$ {#sec:symBreak}
===========================================================

In this section we prepare the ground to apply a SAT solver to find the set of all $(r_1,\ldots,r_k;n)$ Ramsey colorings modulo weak isomorphism. The constraints are those presented in Figure \[fig:gcp\] and their encoding to CNF is as described in Section \[sec:embed\]. Our final aim is to compute the set of all $(3,3,3;13)$ colorings modulo weak isomorphism. Then we can apply the embedding technique of Section \[sec:embed\] to determine the existence of a ${\langle 13,8,8 \rangle}$ regular $(4,3,3;30)$ Ramsey coloring. Given Theorem \[thm:regular\], this will determine the value of $R(4,3,3)$.

Solving hard search problems on graphs, and graph coloring problems in particular, relies heavily on breaking symmetries in the search space. When searching for a graph, the names of the vertices do not matter, and restricting the search modulo graph isomorphism is highly beneficial. When searching for a graph coloring, on top of graph isomorphism, solutions are typically closed under permutations of the colors: the names of the colors do not matter and the term often used is “weak isomorphism” [@PR98] (the equivalence relation is weaker because both node names and edge colors do not matter). When the problem is to compute the set 