number $R(r_1,\ldots,r_k)$ is the least $n>0$ such that no $(r_1,\ldots,r_k;n)$ coloring exists. In particular, the number $R(4,3,3)$ is often presented as the unknown Ramsey number with the best chances of being found “soon”. Yet, its precise value has remained unknown for more than 50 years. It is currently known that $30\leq R(4,3,3)\leq 31$. Kalbfleisch [@kalb66] proved in 1966 that $R(4,3,3)\geq 30$, Piwakowski [@Piwakowski97] proved in 1997 that $R(4,3,3)\leq 32$, and one year later Piwakowski and Radziszowski [@PR98] proved that $R(4,3,3)\leq 31$. We demonstrate how our methodology applies to computationally prove that $R(4,3,3)=30$.

Our strategy to compute $R(4,3,3)$ is based on the search for a $(4,3,3;30)$ Ramsey coloring. If one exists, then because $R(4,3,3)\leq 31$, it follows that $R(4,3,3) = 31$. Otherwise, because $R(4,3,3)\geq 30$, it follows that $R(4,3,3) = 30$.

In recent years, Boolean SAT solving techniques have improved dramatically. Today’s SAT solvers are considerably faster and able to manage larger instances than were previously possible. Moreover, encoding and modeling techniques are better understood and increasingly innovative. SAT is currently applied to solve a wide variety of hard and practical combinatorial problems, often outperforming dedicated algorithms. The general idea is to encode a (typically, NP) hard problem instance, $\mu$, to 