a Boolean formula, $\varphi_\mu$, such that the satisfying assignments of $\varphi_\mu$ correspond to the solutions of $\mu$. Given such an encoding, a SAT solver can be applied to solve $\mu$.

Our methodology in this paper combines SAT solving with two additional concepts: *abstraction* and *symmetry breaking*. The paper is structured to let the application drive the presentation of the methodology in three steps. Section \[sec:prelim\] presents: preliminaries on graph coloring problems, some general notation on graphs, and a simple constraint model for Ramsey coloring problems. Section \[sec:embed\] presents the first step in our quest to compute $R(4,3,3)$. We introduce a basic SAT encoding and detail how a SAT solver is applied to search for Ramsey colorings. Then we describe and apply a well known embedding technique, which allows to determine a set of partial solutions in the search for a $(4,3,3;30)$ Ramsey coloring such that if a coloring exists then it is an extension of one of these partial solutions. This may be viewed as a preprocessing step for a SAT solver which then starts from a partial solution. Applying this technique we conclude that if a $(4,3,3;30)$ Ramsey coloring exists then it must be ${\langle 13,8,8 \rangle}$ regular. Namely, 