Using Answer-Set Programming to study van der Waerden numbers
Michael R. Dransfield, Lengning Liu, Victor Marek and Mirek Truszczynski

A classical theorem, due to van der Waerden, states that for every positive integers k and l, there is a positive integer m such that every partition of [m] into k blocks has a block containing an arithmetic progression of length l. The least such number is denoted W(k,l). The only five non-trivial numbers are shown below.

 l = 3 l = 4 l = 5 k = 2 9 35 178 k = 3 27 k = 4 76

1. Critical configurations for [75]:
In this research we used SAT solvers to compute all counterexamples to W(4,3)=75 (up to symmetries: permutation of blocks and the flip operation on partitions, that is, a permutation of partitions induced by the following permutation of [75]: f(x) = 76 -x).
We found 30 such counterexamples or critical configurations for 75.

2. Lower bounds on van der Waerden numbers found by SAT solvers:
We also used our program WSAT(CC), a local-search solver for the logic of propositional schemata   extended with cardinality constraints (logic PS+) to compute lower bounds on some van der Waerden numbers [2][3]. For each pair (k,l) of parameters, to show that W(k,l)> m, we found a partition of [m] into k blocks so that no block contains an arithmetic progression of length l. The lower bounds are in the table below (for more details, please check out the info page). Each entry provides a link to an appropriate counterexample partition.

 l = 3 l = 4 l = 5 l = 6 l = 7 l = 8 k = 2 9 35 178 > 341 > 614 > 1322 k = 3 27 > 193 > 676 > 2236 k = 4 76 > 416 k = 5 > 125 > 880 k = 6 > 194

3. Best known lower bounds on van der Waerden numbers (as of 9/10/2004):
Many researchers have been working on this problem. The following table shows the current best known lower bounds on some van der Waerden numbers. Please refer to the references for more information. Our method contributed one lower bound in the table, namely the lower bound for W(5,3).

 l = 3 l = 4 l = 5 l = 6 l = 7 l = 8 k = 2 9 35 178 > 695[4] > 3702[5] > 7483[5] k = 3 27 > 291[6] > 1209[6] > 8885[6] > 43854[6] > 161371[7] k = 4 76 > 1047[6] > 10436[6] > 90306[6] > 262326[7] k = 5 > 125[1] > 2253[6] > 24044[6] > 177955[7] k = 6 > 206[7] > 3693[7] > 56692[7]

Reference

[1] Satisfiability and Computing van der Waerden numbers
M.R. Dransfield, L. Liu, V. Marek, M. Truszczynski. The Electronic Journal of Combinatorics, vol. 11(1), 2004.

[2] Local search with bootstrapping
L. Liu and M. Truszczynski. Proceedings of SAT-2004.

[3] Local-search techniques for propositional logic with cardinality constraints
L. Liu and M. Truszczynski. Proceedings of CP-2003.

[4] Progressions in Every Two-coloration of Z_n
H. Y. Song, H. Taylor and S. W. Golomb. Journal of Combinatorial Theory, Series A, vol. 61, no. 2, pp. 211-221, Nov. 1992

[5] van der Waerden numbers
Mark Cooke

[6] Ramsey Theory on the Integers (Student Mathematical Library, V. 24)
Bruce M. Landman, Aaron Robertson. American Mathematical Society. January 9, 2004

[7] Lower Bounds for Van der Waerden Numbers
Geoffrey Exoo

ACKNOWLEDGEMENT

Activities discussed on this page are partially supported by the National Science Foundation. Any opinions, findings, and conclusions or recommendations expressed here  are those of the author(s) and do not necessarily reflect the views of the National Science Foundation