We have verified that the van der Waerden number $W(2, 6)$ is 1132, that is, 1132 is the
smallest integer n = W(2, 6) such that whenever the set of integers {1, 2, . . . , $n$} is
2-colored, there exists a monochromatic arithmetic progression of length 6. This was
accomplished by applying special preprocessing techniques that drastically reduced the
required search space. The exhaustive search showing that $W(2, 6)$ = 1132 was carried out
by formulating the problem as a satisfiability (SAT) question for a Boolean formula in
conjunctive normal form (CNF), and then using a SAT solver specifically designed for the
problem. The parallel backtracking computation was run over multiple Beowulf clusters, and
in the last phase, field programmable gate arrays (FPGAs) were used to speed up the
search. The fact that $W(2, 6)$ > 1131 was shown previously by the first author.