  Ramsey Theory deals with avoiding certain patterns. When constructing an
instance that avoids one pattern, it is observed that other patterns emerge.
For example, repetition emerges when avoiding arithmetic progression (Van der
Waerden numbers), while reflection emerges when avoiding monochromatic
solutions of $a+b=c$ (Schur numbers). We exploit observed patterns when
coloring a grid while avoiding monochromatic rectangles. Like many problems in
Ramsey Theory, this problem has a rapidly growing search space that makes
computer search difficult. Steinbach et al. obtained a solution of an 18 by 18
grid with 4 colors by enforcing a rotation symmetry. However, that symmetry is
not suitable for 5 colors.
  In this article, we will encode this problem into propositional logic and
enforce so-called internal symmetries, which preserves satisfiability, to guide
SAT-solving. We first observe patterns with 2 and 3 colors, among which the
"shift pattern" can be easily generalized and efficiently encoded. Using this
pattern, we obtain a new solution of the 18 by 18 grid that is non-isomorphic
to the known solution. We further analyze the pattern and obtain necessary
conditions to further trim down the search space. We conclude with our attempts
on finding a 5-coloring of a 26 by 26 grid, as well as further open problems on
the shift pattern.
