our purposes. All computations were performed on a cluster with a total of $228$ Intel E8400 cores clocked at 2 GHz each, able to run a total of $456$ parallel threads. Each of the cores in the cluster has computational power comparable to a core on a standard desktop computer. Each SAT instance is run on a single thread.

Basic SAT Encoding and Embeddings {#sec:embed}
=================================

Throughout the paper we apply a SAT solver to solve CNF encodings of constraints such as those presented in Figure \[fig:gcp\]. In this way it is straightforward to find a Ramsey coloring or prove its non-existence. Ours is a standard encoding to CNF. To this end: nothing new. For an $n$ vertex graph coloring problem in $k$ colors we take an $n\times n$ matrix $A$ where $A_{i,j}$ represents in $k$ bits the edge $(i,j)$ in the graph: exactly one bit is true indicating which color the edge takes, or no bit is true indicating that the edge $(i,j)$ is not in the graph. Already at the representation level, we use the same Boolean variables to represent the color in $A_{i,j}$ and in $A_{j,i}$ for each $1\leq
i<j\leq n$. We further fix the variables corresponding 