On the van der Waerden numbers w(2;3,t)

In this paper we present results and conjectures on the ordinary van der Waerden numbersw(2;3,t) and on the new palindromic van der Waerden numbers  pdw(2;3,t). We have computed the exact value of the previously unknown number w(2;3,19)=349, and we provide new lower bounds for 20≤t≤3920≤t≤39, where for 20≤t≤3020≤t≤30 we conjecture these bounds to be exact. The lower bounds for w(2;3,t) with 24≤t≤3024≤t≤30 refute the conjecture that w(2;3,t)≤t2 as suggested in Brown et al. (2008). Based on the known values of w(2;3,t), we investigate regularities to better understand the lower bounds of w(2;3,t). Motivated by such regularities, we introduce palindromic van der Waerden numbers pdw(k;t0,…,tk−1), which are defined as the ordinary numbers w(k;t0,…,tk−1), but where only palindromic solutions are considered, reading the same from both ends. Different from the situation for ordinary van der Waerden numbers, these “numbers” need actually to be pairs of numbers. We compute pdw(2;3,t) for 3≤t≤273≤t≤27, and we provide bounds for t≤39t≤39, which we believe to be exact for t≤35t≤35. All computations are based on SAT solving, and we discuss the various relations between SAT solving and Ramsey theory. Especially we introduce a novel (open-source) SAT solver, the tawSolver, which performs best on the SAT instances studied here, and which is actually the original DLL-solver by Davis et al. (1962), but with an efficient implementation and a modern heuristic typical for look-ahead solvers, applying the theory developed by the second author (Kullmann, 2009).