  We consider the links between Ramsey theory in the integers, based on van der
Waerden's theorem, and (boolean, CNF) SAT solving. We aim at using the problems
from exact Ramsey theory, concerned with computing Ramsey-type numbers, as a
rich source of test problems, where especially methods for solving hard
problems can be developed. In order to control the growth of the problem
instances, we introduce "transversal extensions" as a natural way of
constructing mixed parameter tuples (k_1, ..., k_m) for van-der-Waerden-like
numbers N(k_1, ..., k_m), such that the growth of these numbers is guaranteed
to be linear. Based on Green-Tao's theorem we introduce the "Green-Tao numbers"
grt(k_1, ..., k_m), which in a sense combine the strict structure of van der
Waerden problems with the (pseudo-)randomness of the distribution of prime
numbers. Using standard SAT solvers (look-ahead, conflict-driven, and local
search) we determine the basic values. It turns out that already for this
single form of Ramsey-type problems, when considering the best-performing
solvers a wide variety of solver types is covered. For m > 2 the problems are
non-boolean, and we introduce the "generic translation scheme", which offers an
infinite variety of translations ("encodings") and covers the known methods. In
most cases the special instance called "nested translation" proved to be far
superior.
