to $A_{i,i}$ to ${\mathit{false}}$. The rest of the SAT encoding is straightforward.

Constraint (\[constraint:simple\]) is encoded to CNF by introducing clauses to state that for each $A_{i,j}$ with $1\leq i<j\leq n$ at most one of the $k$ bits representing the color of the edge $(i,j)$ is true. In our setting typically $k=3$. For three colors, if $b_1,b_2,b_3$ are the bits representing the color of an edge, then three clauses suffice: $(\bar b_1\lor \bar b_2),(\bar b_1\lor
\bar b_3),(\bar b_2\lor \bar b_3)$. Constraint (\[constraint:nok\]) is encoded by a single clause per set $I$ of $r$ vertices expressing that at least one of the bits corresponding to an edge between vertices in $I$ does not have color $c$. Finally Constraint (\[constraint:coloring\]) is a conjunction of constraints of the previous two forms.

In Section \[sec:symBreak\] we will improve on this basic encoding by introducing symmetry breaking constraints (encoded to CNF). However, for now we note that, even with symmetry breaking constraints, using the basic encoding, a SAT solver is currently not able to solve any of the open Ramsey coloring problems such as those considered in this paper. In particular, directly applying a SAT solver to search for a $(4,3,3;30)$ Ramsey coloring is hopeless.

