1: \documentclass{llncs}

2: %\documentclass[runningheads]{llncs}

3: 

4: \usepackage{latexsym}

5: \usepackage{amssymb}

6: \usepackage{amsmath}

7: \usepackage{psfig}

8: \usepackage{url}

9: 

10: \newcommand{\Sup}{\mathit{Sup}}

11: \newcommand{\CC}{\mathit{CC}}

12: \newcommand{\dff}{\mathit{Def}}

13: \newcommand{\pth}{\mathit{path}}

14: \newcommand{\dom}{\mathit{Dom}}

15: \newcommand{\Tr}{\mathbf{t}}

16: \newcommand{\Fa}{\mathbf{f}}

17: \newcommand{\datac}{\mathrm{DC}}

18: \newcommand{\datan}{\mathrm{DATALOG}^{\neg}}

19: \newcommand{\data}{\mathrm{data}}

20: \newcommand{\yes}{\mathrm{YES}}

21: \newcommand{\con}{\mathit{Con}}

22: \newcommand{\cc}{\mathit{cc}}

23: \newcommand{\sol}{\mathit{sol}}

24: \newcommand{\vv}{\mathit{var}}

25: \newcommand{\vp}{\mathit{vpos}}

26: \newcommand{\size}{\mathit{size}}

27: \newcommand{\pred}{\mathit{pred}}

28: \newcommand{\pos}{\mathit{pos}}

29: \newcommand{\indx}{\mathit{index}}

30: \newcommand{\num}{\mathit{num}}

31: \newcommand{\bl}{\mathit{block}}

32: \newcommand{\inb}{\mathit{in\_block}}

33: \newcommand{\cl}{\mathit{cl}}

34: \newcommand{\vpos}{\mathit{vpos}}

35: \newcommand{\var}{\mathit{Var}}

36: \newcommand{\HU}{\mathit{HU}}

37: \newcommand{\pr}{\mathit{Pr}}

38: \newcommand{\gr}{\mathit{gr}}

39: \newcommand{\grnd}{\mbox{\tt{PSgrnd}}}

40: \newcommand{\eps}{\mbox{\tt{ePSs}}}

41: \newcommand{\xgrnd}{\mbox{\tt{ePSgrnd}}}

42: \newcommand{\at}{\mathit{At}}

43: %\newcommand{\plc}{\mathit{PS}^\mathit{cwa}}

44: \newcommand{\plc}{\mathit{PS}}

45: \newcommand{\eplc}{\mathit{PS}+}

46: \newcommand{\HB}{\mathit{HB}}

47: \newcommand{\plcp}{\mathit{PS}+}

48: \newcommand{\epl}{\mathit{ePS}}

49: \newcommand{\col}{\mathit{color}}

50: \newcommand{\gcl}{\mathit{gcl}}

51: \newcommand{\tc}{\mathit{tc}}

52: \newcommand{\vc}{\mathit{vc}}

53: \newcommand{\eq}{\mathit{eq}}

54: \newcommand{\sm}{\mathit{sum}}

55: \newcommand{\df}{\mathit{diff}}

56: \newcommand{\ltq}{\mathit{lteq}}

57: \newcommand{\nq}{\mathit{nq}}

58: \newcommand{\invc}{\mathit{invc}}

59: \newcommand{\hc}{\mathit{hc}}

60: \newcommand{\hcp}{\mathit{hc\_perm}}

61: \newcommand{\hce}{\mathit{hc\_edge}}

62: \newcommand{\start}{\mathit{start}}

63: \newcommand{\visit}{\mathit{visit}}

64: \newcommand{\clr}{\mathit{clrd}}

65: \newcommand{\body}{\mathit{body}}

66: \newcommand{\vtx}{\mathit{vtx}}

67: \newcommand{\edge}{\mathit{edge}}

68: \newcommand{\und}{{\_}}

69: \newcommand{\tr}{{\bf T}}

70: \newcommand{\fa}{{\bf F}}

71: \newcommand{\vph}{\varphi}

72: \newcommand{\rra}{\rightarrow}

73: \newcommand{\Ra}{\Rightarrow}

74: \newcommand{\La}{\Leftarrow}

75: \newcommand{\lla}{\leftarrow}

76: \newcommand{\lra}{\leftrightarrow}

77: \newcommand{\Lra}{\Leftrightarrow}

78: \newcommand{\n}{\mathbf{not}}

79: \newcommand{\impl}{\Leftarrow}

80: \newcommand{\proves}{\vdash}

81: 

82: \newcommand{\mc}[1]{\marginpar{\scriptsize{#1}}}

83: \newcommand{\vd}[1]{\text{vdW}_{#1}}

84: %\newcommand{\victor}[1]{{\bf Victor: #1}} 

85: %Celowo zaslonilem by NIE pozostalo przez omylke

86: 

87: 

88: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

89: \begin{document}

90: 

91: %\pagestyle{headings}

92: \pagestyle{empty}

93: 

94: \title{Satisfiability and computing van der Waerden numbers}

95: 

96: \titlerunning{SAT and van der Waerden numbers}

97: 

98: \author{Michael R. Dransfield\inst{1} \and Victor W. Marek\inst{2} \and

99: Miros\l aw Truszczy\'nski\inst{2}}

100: %

101: \authorrunning{Michael Dransfield et al.}

102: %

103: %

104: \institute{National Security Agency, Information Assurance Directorate,

105: Ft. Meade, MD 20755\\

106: \and

107: Department of Computer Science, University

108: of Kentucky, Lexington,\\

109: KY 40506-0046, USA}

110: 

111: %\begin{document}

112: 

113: \maketitle

114: 

115: \begin{abstract}

116: In this paper we bring together the areas of combinatorics and

117: propositional satisfiability. Many combinatorial theorems establish,

118: often constructively, the existence of positive integer functions,

119: without actually providing their closed algebraic form or tight lower

120: and upper bounds. The area of Ramsey theory is especially rich in such 

121: results. Using the problem of computing van der Waerden numbers as an

122: example, we show that these problems can be represented by parameterized 

123: propositional theories in such a way that decisions concerning their

124: satisfiability determine the numbers (function) in question. We show

125: that by using general-purpose complete and local-search techniques for testing 

126: propositional satisfiability, this approach becomes effective ---

127: competitive with specialized approaches. By following it, we were able 

128: to obtain several new results pertaining to the problem of computing 

129: van der Waerden numbers. We also note that due to their properties,

130: especially their structural simplicity and computational hardness, 

131: propositional theories that arise in this research can be of use in 

132: development, testing and benchmarking of SAT solvers.

133: \end{abstract}

134: 

135: 

136: \section{Introduction}\label{intro}

137: 

138: In this paper we discuss how the areas of propositional satisfiability

139: and combinatorics can help advance each other. On one hand, we show 

140: that recent dramatic improvements in the efficiency of SAT solvers 

141: and their extensions make it possible to obtain new results in 

142: combinatorics simply by encoding problems as propositional theories, 

143: and then computing their models (or deciding that none exist) using 

144: off-the-shelf general-purpose SAT solvers. On the other hand, we argue 

145: that combinatorics is a rich source of structured, parameterized 

146: families of hard propositional theories, and can provide useful sets 

147: of benchmarks for developing and testing new generations of SAT 

148: solvers.

149: 

150: In our paper we focus on the problem of computing van der Waerden 

151: numbers. The celebrated van der Waerden theorem \cite{vdw27} asserts 

152: that for every positive integers $k$ and $l$ there is a positive 

153: integer $m$ such that every partition of $\{1,\ldots,m\}$ into $k$ 

154: blocks (parts) has at least one block with an arithmetic progression 

155: of length $l$. The problem is to find the least such number $m$. This

156: number is called the {\em van der Waerden number} $W(k,l)$. Exact 

157: values of $W(k,l)$ are known only for five pairs $(k,l)$. For other

158: combinations of $k$ and $l$ there are some general lower and upper

159: bounds but they are very coarse and do not give any good idea about 

160: the actual value of $W(k,l)$. In the paper we show that SAT solvers 

161: such as POSIT \cite{posit}, and SATO \cite{sato}, 

162: as well as recently 

163: developed local-search solver {\em walkaspps} \cite{lt03}, designed 

164: to compute models for propositional theories  extended by cardinality 

165: atoms \cite{et01a}, can improve lower bounds for van der Waerden numbers 

166: for several combinations of parameters $k$ and $l$.

167: 

168: Theories that arise in these investigations are determined by the two

169: parameters $k$ and $l$. Therefore, they show a substantial degree of

170: structure and similarity. Moreover, as $k$ and $l$ grow, these theories

171: quickly become very hard. This hardness is only to some degree an

172: effect of the growing size of the theories. For the most part, it is

173: the result of the inherent difficulty of the combinatorial problem in

174: question. All this suggests that theories resulting from hard

175: combinatorial problems defined in terms of tuples of integers may serve

176: as benchmark theories in experiments with SAT solvers.

177: 

178: There are other results similar in spirit to the van der Waerden

179: theorem. The Schur theorem states that for every positive integer 

180: $k$ there is an integer $m$ such that every partition of $\{1,

181: \ldots, m\}$ into $k$ blocks contains a block that is not sum-free. 

182: Similarly, the Ramsey theorem (which gave name to this whole area 

183: in combinatorics) \cite{ra28} concerns the existence of monochromatic 

184: cliques in edge-colored graphs, and the Hales-Jewett theorem 

185: \cite{hj63} concerns the existence of monochromatic lines in colored 

186: cubes. 

187: %\footnote{Hales-Jewett theorem implies the van der Waerden theorem 

188: %and the bound on Hales-Jewett numbers found by Shelah \cite{sh88} 

189: %entails an upper bound on van der Waerden numbers.}. 

190: Each of these results gives rise to a particular function defined on 

191: pairs or triples of integers and determining the values of these 

192: functions is a major challenge for combinatorialists. In all cases, 

193: only few exact values are known and lower and upper estimates are very 

194: far apart. Many of these results were obtained by means of specialized 

195: search algorithms highly depending on the combinatorial properties of the

196: problem. Our paper shows that generic SAT solvers are maturing to the

197: point where they are competitive and sometimes more effective than

198: existing advanced specialized approaches.

199: 

200: \section{van der Waerden numbers}

201: \label{vdw-sub}

202: 

203: In the paper we use the following terminology. By $\mathbb{Z}^+$

204: we denote the set of positive integers and, for $m \in \mathbb{Z}^+$,

205: $[m]$ is the set $\{1,\ldots,m\}$. A {\em partition} of a set

206: $X$ is a collection ${\cal A}$ of nonempty and mutually disjoint 

207: subsets of $X$ such that $\bigcup {\cal A} = X$. Elements of ${\cal A}$

208: are commonly called {\em blocks}.

209: 

210: Informally, the van der Waerden theorem \cite{vdw27} states that 

211: if a sufficiently long initial segment of positive integers is 

212: partitioned into a few blocks, then one of these blocks has to 

213: contain an arithmetic progression of a desired length. Formally, the

214: theorem is usually stated as follows.

215: 

216: \begin{theorem}[van der Waerden theorem] \label{vdw27}

217: For every $k, l \in \mathbb{Z}^+$, there is $m \in \mathbb{Z}^+$ 

218: such that for every partition $\{A_1,\ldots,A_k\}$ of $[m]$,

219: there is $i$, $1 \leq i \leq k$, such that block $A_i$ contains 

220: an arithmetic progression of length at least $l$.

221: \end{theorem}

222: 

223: We define the {\em van der Waerden number} $W(k,l)$ to be the least 

224: number $m$ for which the assertion of Theorem \ref{vdw27} holds. 

225: Theorem \ref{vdw27} states that van der Waerden numbers are well 

226: defined.

227: 

228: One can show that for every $k$ and $l$, where $l\geq 2$, $W(k,l) > k$.

229: In particular, it is easy to see that $W(k,2) = k+1$. From now on, we

230: focus on the non-trivial case when $l\geq 3$.

231: 

232: Little is known about the numbers $W(k,l)$. In particular, no closed

233: formula has been identified so far and only five exact values are 

234: known. They are shown in Table \ref{tab1} \cite{bn79,grs90}.

235: 

236: \begin{table} \label{table.vdw}

237: \begin{center}

238: \begin{tabular}{ || l  r | r | r | r ||}

239: \hline

240:      & $l$  & $3$ & $4$  & $5$ \\ 

241: $k$  &      &     &      &     \\ 

242: \hline

243: $2$  &      & $9$ & $35$ & $178$ \\

244: $3$  &      & $27$&      &       \\

245: $4$  &      & $76$&      &       \\

246: \hline

247: \end{tabular}

248: \end{center}

249: \caption{Known non-trivial values of van der Waerden numbers}

250: \label{tab1}

251: \end{table}

252: 

253: Since we know few exact values for van der Waerden numbers, it is

254: important to establish good estimates. One can show that the Hales-Jewett

255: theorem entails the van der Waerden theorem, and some upper bounds for the

256: numbers $W(k,l)$ can be derived from the Shelah's proof of the former

257: \cite{sh88}. Recently, Gowers \cite{go01} presented stronger upper

258: bounds, which he derived from his proof of the Szemer\'edi theorem

259: \cite{sz75} on arithmetic progressions.

260: 

261: In our work, we focus on lower bounds. Several general results are

262: known. For instance, Erd\"os and Rado \cite{er52} provided a

263: non-constructive proof for the inequality

264: \[

265: W(k,l) > (2(l-1) k^{l-1})^{1/2}.

266: \]

267: For some special values of parameters $k$ and $l$, Berlekamp obtained

268: better bounds by using properties of finite fields \cite{be68}. These

269: bounds are still rather weak. His strongest result concerns the case

270: when $k=2$ and $l-1$ is a prime number. Namely, he proved that when

271: $l-1$ is a prime number,

272: \[

273: W(2,l) > (l-1) 2^{l-1} .

274: \]

275: In particular, $W(2,6) > 160$ and $W(2,8) > 896$.

276: 

277: Our goal in this paper is to employ propositional satisfiability solvers 

278: to find lower bounds for several small van der Waerden numbers. The

279: bounds we find significantly improve on the ones implied by the results

280: of Erd\"os and Rado, and Berlekamp. 

281: 

282: We proceed as follows. For each triple of positive integers 

283: $\langle k,l,m\rangle$, we define a propositional CNF theory 

284: $\text{vdW}_{k,l,m}$ and then show that $\text{vdW}_{k,l,m}$ is 

285: satisfiable if and only if $W(k,l) > m$. With such encodings, one can 

286: use SAT solvers (at least in principle) to determine the satisfiability 

287: of $\vd{k,l,m}$ and, consequently, find $W(k,l)$. Since $W(k,l) > k$, 

288: without loss of generality we can restrict our attention to $m > k$.

289: We also show that more concise encodings are possible, leading

290: ultimately to better bounds, if we use an extension of propositional

291: logic by {\em cardinality atoms} and apply to them solvers capable of 

292: handling such atoms directly.

293: 

294: To describe $\vd{k,l,m}$ we will use a standard first-order language, 

295: without function symbols, but containing a predicate symbol $\inb$ 

296: and constants $1,\ldots,m$. An intuitive reading of a ground atom

297: $\inb(i,b)$ is that an integer $i$ is in block $b$. 

298: 

299: We now define the theory $\vd{k,l,m}$ by including in it the following

300: clauses:

301: \newcounter{ct1}

302: \begin{list}{vdW\arabic{ct1}:\ }{\usecounter{ct1}\topsep 0.1in

303: \parsep 0in\itemsep 0.05in\itemindent 0in\leftmargin 0.65in\labelwidth

304: 0.5in \labelsep 0.1in}

305: \item $\neg \inb(i,b_1) \lor \neg \inb(i,b_2)$, \ for every $i\in[m]$ and

306: every $b_1,b_2\in[k]$ such that $b_1<b_2$,

307: \item $\inb(i,1) \vee \ldots \vee \inb(i,k)$, \ for every $i\in [m]$,

308: \item $\neg \inb(i,b) \vee \neg \inb(i+d,b) \vee \ldots \vee \neg

309: \inb(i+(l-1)d, b)$, \ for every $i,d \in [m]$ such that $i+(l-1)d\leq m$,

310: and for every $b$ such that $1\leq b\leq k$.

311: \end{list}

312: 

313: As an aside, we note that we could design $\vd{k,l,m}$ strictly as a 

314: theory in propositional language using propositional atoms of the form

315: $\mathit{in\_block}_{i,b}$ instead of ground atoms $\inb(i,b)$. However, 

316: our approach

317: opens a possibility to specify this theory as finite (and independent of

318: data) collections of {\em propositional schemata}, that is, open clauses

319: in the language of first-order logic without function symbols. Given a

320: set of appropriate constants (to denote integers and blocks) such

321: theory, after grounding, coincides with $\vd{k,l,m}$. In fact, we have

322: defined an appropriate syntax that allows us to specify both data and

323: schemata and implemented a grounding program {\em psgrnd} \cite{et01a}

324: that generates their equivalent ground (propositional) representation.

325: This grounder accepts arithmetic expressions as well as simple regular

326: expressions, and evaluates and eliminates them according to their 

327: standard interpretation. Such approach significantly simplifies the

328: task of developing propositional theories that encode problems, as well as

329: the use of SAT solvers \cite{et01a}.

330: 

331: Propositional interpretations of the theory $\vd{k,l,m}$ can be

332: identified with subsets of the set of atoms $\{\inb(i,b)\colon i

333: \in [m],\ b\in [k]\}$. Namely, a set $M \subseteq \{\inb(i,b)\colon

334: i\in [m],\ b\in[k]\}$ determines an interpretation in which all atoms

335: in $M$ are true and all other atoms are false. In the paper we always

336: assume that interpretations are represented as sets.

337: 

338: It is easy to see that clauses (vdW1) ensure that if $M$ is a model of 

339: $\vd{k,l,m}$ (that is, is an interpretation satisfying all clauses of 

340: $\vd{k,l,m}$), then for every $i\in [m]$, $M$ contains at most one atom 

341: of the form $\inb(i,b)$. Clauses (vdW2) ensure that for every $i\in 

342: [m]$ there is at least one $b\in [k]$ such that $\inb(i,b)\in M$. In 

343: other words, clauses (vdW1) and (vdW2) together ensure that if $M$ is 

344: a model of $\vd{k,l,m}$, then $M$ determines a partition of $[m]$ into 

345: $k$ blocks. 

346: 

347: The last group of constraints, clauses (vdW3), guarantee that elements

348: from $[m]$ forming an arithmetic progression of length $l$ do not all

349: belong to the same block. All these observations imply the following 

350: result.

351: 

352: \begin{proposition}\label{vdw3}

353: There is a one-to-one correspondence between models of the formula

354: $\vd{k,l,m}$ 

355: and partitions of $[m]$ into $k$ blocks so that no block contains

356: an arithmetic progression of length $l$. Specifically, an

357: interpretation $M$ is a model of $\vd{k,l,m}$ if and only if

358: $\{\{i\in [m] \colon \inb(i,b) \in M\}\colon b\in [k]\}$ is a 

359: partition of $[m]$ into $k$ blocks such that no block contains an 

360: arithmetic progression of length $l$.

361: \end{proposition}

362: 

363: Proposition \ref{vdw3} has the following direct corollary.

364: 

365: \begin{corollary}\label{c.vdw}

366: For every positive integers $k, l$, and $m$, with $l \geq 2$ and $m > k$,

367: $m < W(k,l)$ if and only if the formula $\vd{k,l,m}$ is

368: satisfiable.

369: \end{corollary}

370: 

371: It is evident that if $m$ has the property that $\vd{k,l,m}$ is

372: unsatisfiable then for every $m' > m$, $\vd{k,l,m'}$ is also 

373: unsatisfiable. Thus, Corollary \ref{c.vdw} suggests the following 

374: algorithm that, given $k$ and $l$, computes the van der Waerden number 

375: $W(k,l)$: for consecutive integers $m=k+1, k+2,\ldots$ we test whether 

376: the theory $\vd{k,l,m}$ is satisfiable. If so, we continue. If not, we 

377: return $m$ and terminate the algorithm. By the van der Waerden theorem, 

378: this algorithm terminates. 

379: 

380: It is also clear that there are simple symmetries involved in

381: the van der Waerden problem. If a set $M$ of atoms of the form 

382: $\inb(i,b)$ is a model of the theory $\vd{k,l,m}$, and $\pi$ is 

383: a permutation of $[k]$, then the corresponding set of atoms 

384: $\{\inb(i,\pi(b))\colon \inb(i,b)\in M\}$ is also a model of

385: $\vd{k,l,m}$, and so is the set of atoms $\{\inb(m+1-i,b)\colon 

386: \inb(i,b)\in M\}$. 

387: %In our computational experiments we used additional clauses 

388: %breaking these symmetries.

389: 

390: Following the approach outlined above, adding clauses to break these

391: symmetries, and applying POSIT  \cite{posit} and SATO \cite{sato}

392: as a SAT solvers we were able to establish that 

393: $W(4,3) = 76$ and compute a ``library'' of counterexamples (partitions

394: with no block containing arithmetic progressions of a specified length)

395: for $m = 75$. We were also able to find several lower bounds on 

396: van der Waerden numbers for larger values of $k$ and $m$. 

397: 

398: However, a major limitation of our first approach is that the size of 

399: theories $\vd{k,l,m}$ grows quickly and makes complete SAT 

400: solvers ineffective. Let us estimate the size of the theory

401: $\vd{k,l,m}$. The total size of clauses (vdW1) (measured as the 

402: number of atom occurrences) is $\Theta(mk^2)$. The size of clauses 

403: (vdW2) is $\Theta(mk)$. Finally, the size of clauses (vdW3) is 

404: $\Theta(m^2)$ (indeed, there are $\Theta(m^2/l)$ arithmetic 

405: progressions of length $l$ in $[m])$\footnote{Goldstein \cite{dg02}

406: provided a 

407: precise formula. When $r = rm(m-1,l-1)$ and $q = q(m-1,l-1)$ then 

408: there are $q\cdot r + \binom{q-1}{2}\cdot (l-1)$ arithmetic 

409: progressions of length $l$ in $[m]$.}. Thus, the total size of the 

410: theory $\vd{k,l,m}$ is $\Theta(mk^2+m^2)$.

411: 

412: To overcome this obstacle, we used a two-pronged 

413: approach. First, as a modeling language we used PS+ logic \cite{et01a},

414: which is an extension of propositional logic by cardinality atoms. 

415: Cardinality atoms support concise representations of constraints of the

416: form ``at least $p$ and at most $r$ elements in a set are true'' and

417: result in theories of smaller size.

418: Second, we used a local-search algorithm, {\em walkaspps}, for finding 

419: models of theories in logic PS+ that we have designed and implemented

420: recently \cite{lt03}. Using encodings as theories in logic PS+ and {\em

421: walkaspps} as a solver, we were able to obtain substantially stronger 

422: lower bounds for van der Waerden numbers than those know to date.

423: 

424: We will now describe this alternative approach. 

425: For a detailed treatment of the PS+

426: logic we refer the reader to \cite{et01a}. In this paper, we will

427: only review most basic ideas underlying the logic PS+ (in its

428: propositional form). By a {\em propositional cardinality atom} ({\em

429: c-atom} for short), we mean any expression of the form $m\{p_1,\ldots,

430: p_k\}n$ (one of $m$ and $n$, but not both, may be missing), where $m$ 

431: and $n$ are non-negative integers and $p_1 ,\ldots,p_k$ are 

432: propositional atoms from $\at$. The notion of a clause generalizes in 

433: an obvious way to the language with cardinality atoms. Namely, a {\em 

434: c-clause} is an expression of the form

435: \begin{equation}\label{eq.cl}

436: %\[

437: C=\ \ A_1\vee \ldots \vee A_s\vee \neg B_1\vee\ldots\vee \neg B_t,

438: %\]

439: \end{equation}

440: where all $A_i$ and $B_i$ are (propositional) atoms or cardinality

441: atoms.

442: 

443: Let $M\subseteq \at$ be a set of atoms. We say that $M$ {\em satisfies}

444: a cardinality atom $m\{p_1,\ldots,p_k\}n$ if

445: \[

446: m \leq |M\cap \{p_1,\ldots,p_k\}|\leq n.

447: \]

448: If $m$ is missing, we only require that $|M\cap \{p_1,\ldots,p_k\}|\leq

449: n$. Similarly, when $n$ is missing, we only require that $m \leq |M\cap

450: \{p_1,\ldots,p_k\}|$. A set of atoms $M$ {\em satisfies} a c-clause $C$

451: of the form (\ref{eq.cl})

452: if $M$ satisfies at least one atom $A_i$ or does not satisfy at least

453: one atom $B_j$. W note that the expression $1\{p_1,\ldots ,p_k\}1$

454: expresses the quantifier ``There exists exactly one ...'' - commonly

455: used in mathematical statements.

456: 

457: It is now clear that all clauses (vdW1) and (vdW2) from $\vd{k,l,m}$ 

458: can be represented in a more concise way by the following

459: collection of c-clauses:

460: \newcounter{ct2}

461: \begin{list}{vdW$'$\arabic{ct2}:\ }{\usecounter{ct2}\topsep 0.03in

462: \parsep 0in\itemsep 0in}

463: \item $1\{\inb(i,1),\ldots,\inb(i,k)\}1$, for every $i\in [m]$.

464: \end{list}

465: 

466: Indeed, c-clauses (vdW$'$1) enforce that their models, for every

467: $i\in[m]$ contain exactly one atom of the form $\inb(i,b)$ ---

468: precisely the same effect as that of clauses (vdW1) and (vdW2).

469: Let $\vd{k,l,m}'$ be a PS+ theory consisting of clauses (vdW$'$1)

470: and (vdW3). It follows that Proposition \ref{vdw3} and Corollary 

471: \ref{c.vdw} can be reformulated by replacing $\vd{k,l,m}$ with

472: $\vd{k,l,m}'$ in their statements. Consequently, any algorithm

473: for finding models of PS+ theories can be used to compute van der

474: Waerden numbers (or, at least, some bounds for them) in the way we

475: described above.

476: 

477: The adoption of cardinality atoms leads to a more concise 

478: representation of the problem. While, as we discussed above,  

479: the size of all clauses (vdW1) and (vdW2) is $\Theta (mk^2 + mk)$, 

480: the size of clauses (vdW$'$1) is $\Theta(mk)$.

481: 

482: In our experiments, for various lower bound results,

483: we used the local-search algorithm {\em walkaspps}

484: \cite{lt03}. This algorithm is based on the same ideas as {\em

485: walksat} \cite{skc94}. A major difference is that due to the presence of

486: c-atoms in c-clauses {\em walkaspps} uses different formulas to 

487: calculate the breakcount and proposes several other heuristics designed

488: specifically to handle c-atoms.

489: 

490: \section{Results} \label{results}

491: 

492: Our goal is to establish lower bounds for small van der Waerden numbers

493: by exploiting propositional satisfiability solvers.  Here is a summary

494: of our results.

495: 

496: \begin{enumerate}

497: \item Using complete SAT solvers POSIT and SATO and the encoding of the

498: problem as $\vd{k,l,m}$, we found a ``library'' of all (up to obvious

499: symmetries) counterexamples to the fact that $W(4,3) > 75$. There are

500: 30 of them. We list two of them in the appendix. A complete list can be

501: found at \url{http://www.cs.uky.edu/ai/vdw/}. Since there 

502: are $48$ symmetries, 

503: of the types discussed above,

504: the full library of counterexamples consists of 

505: $1440$  partitions.

506: \item We found that the formula $\vd{4,3,76}$ is unsatisfiable. Hence,

507: we found that a ``generic'' SAT solver is capable of finding that 

508: $W(4,3) = 76$.

509: \item We established several new lower bounds for the numbers $W(k,l)$. 

510: They are presented in Table \ref{table.vdw1}. Partitions demonstrating 

511: that $W(2,8) > 1295$, $W(3,5) > 650$, and $W(4,4) > 408$ are included 

512: in the appendix. Counterexample partitions for all other inequalities 

513: are available at

514: \url{http://www.cs.uky.edu/ai/vdw/}.

515: We note that our bounds for $W(2,6)$ and $W(2,8)$ are much stronger

516: than those implied by the results of Berlekamp \cite{be68}, which we 

517: stated earlier.

518: \end{enumerate}

519: 

520: \begin{table} \label{table.vdw1}

521: \caption{Extended results on van der Waerden numbers}

522: \begin{center}

523: \begin{tabular}{ || l  r | r | r | r | r | r | r ||}

524: \hline

525:      & $l$  & $3$    & $4$    & $5$    & $6$    & $7$    & $8$     \\

526: $k$  &      &        &        &        &        &        &         \\

527: \hline

528: $2$  &      & $9$    & $35$   & $178$  & $>341$ & $>604$ & $>1295$ \\

529: $3$  &      & $27$   & $>193$ & $>650$ &        &        &         \\

530: $4$  &      & $76$   & $>408$ &        &        &        &         \\

531: $5$  &      & $>125$ &        &        &        &        &         \\

532: $6$  &      & $>180$ &        &        &        &        &         \\

533: \hline

534: \end{tabular}

535: \end{center}

536: \end{table}

537: 

538: To provide some insight into the complexity of the satisfiability 

539: problems involved, in Table \ref{table.vdw2} we list the number of

540: atoms and the number of clauses in the theories $\vd{k,l,m}'$.

541: Specifically, the entry $k,l$ in this table contains the number of

542: atoms and the number of clauses in the theories $\vd{k,l,m}'$, where

543: $m$ is the value given in the entry $k,l$ in Table \ref{table.vdw1}. 

544: 

545: %\vspace*{-0.2in}

546: \begin{table} \label{table.vdw2}

547: \caption{Numbers of atoms and clauses in theories $\vd{k,l,m}'$, used

548: to establish the results presented in Table \ref{table.vdw1}.}

549: \begin{center}

550: \begin{tabular}{ || l  r | r | r | r | r | r | r ||}

551: \hline

552:     & $l$  & $3$    & $4$    & $5$    & $6$    & $7$    & $8$    \\

553: $k$ &   &        &        &        &        &        &        \\

554: \hline

555: $2$ &   & 18, 41  & 70, 409 & 356, 7922 & 682, 23257 & 1208, 60804 & 2590, 239575\\

556: $3$ &   & 108, 534 & 579, 18529 & 1950, 158114 &        &        &        \\

557: $4$ &   & 304, 5700 & 1632, 110568 &        &        &        &        \\

558: $5$ &   & 625, 19345 &        &        &        &        &        \\

559: $6$ &   & 1080, 48240 &        &        &        &        &        \\

560: \hline

561: \end{tabular}

562: \end{center}

563: \end{table}

564: 

565: \section{Discussion}\label{conclude}

566: 

567: Recent progress in the development of SAT solvers provides an important

568: tool for researchers looking for both the existence and non-existence

569: of various combinatorial objects. We have demonstrated that several 

570: classical questions related to van der Waerden numbers can be naturally 

571: cast as questions on the existence of satisfying valuations for some 

572: propositional CNF-formulas. 

573: 

574: Computing combinatorial objects such as van der Waerden numbers is

575: hard. They are structured but as we pointed out few values are known, 

576: and new results are hard to obtain. Thus, the computation of those 

577: numbers can serve as a benchmark (`can we find the configuration 

578: such that...') for complete and local-search methods, and as a 

579: challenge (`can we show that a configuration such that ...' does not 

580: exist) for complete SAT solvers. Moreover, with powerful SAT solvers 

581: it is likely that the bounds obtained by computation of counterexamples 

582: are ``sharp'' in the sense that when a configuration is not found then 

583: none exist. For instance it is likely that $W(5,3)$ is close to 126 

584: (possibly, it is 126), because 125 was the last integer where we were 

585: able to find a counterexample despite significant computational effort. 

586: This claim is further supported by the fact that in all examples where 

587: exact values are known, our local-search algorithm was able to find 

588: counterexample partitions for the last possible value of $m$. The 

589: lower-bounds results of this sort may constitute an important clue for 

590: %researchers looking for nonexistence arguments.

591: researchers looking for nonexistence arguments and, ultimately, for the

592: closed form of van der Waerden numbers.

593: 

594: A major impetus for the recent progress of SAT solvers comes from 

595: applications in computer engineering. In fact, several leading SAT 

596: solvers such as zCHAFF \cite{mmzzm01} and {\em berkmin} \cite{berkmin}

597: have been developed with the express goal of aiding engineers in 

598: correctly designing and implementing digital circuits. Yet, the fact 

599: that these solvers are able to deal with hard optimization problems 

600: in one area (hardware design and verification) carries the promise 

601: that they will be of use in another area --- combinatorial 

602: optimization. Our results indicate that it is likely to be the 

603: case.

604: 

605: The current capabilities of SAT solvers has allowed us to handle

606: large instances of these problems. Better heuristics and other

607: techniques for pruning the search space will undoubtedly further expand

608: the scope of applicability of generic SAT solvers to problems that,

609: until recently, could only be solved using specialized software.

610: 

611: \section*{Acknowledgments}

612: The authors thank Lengning Liu for developing software facilitating

613: our experimental work. This research has been supported by the Center 

614: for Communication Research, La Jolla. During the research reported in 

615: this paper the second and third authors have been partially supported 

616: by an NSF grant  IIS-0097278.

617: 

618: \begin{thebibliography}{10}

619: 

620: %\bibitem{arms02}

621: %F.A. Aloul, A.~Ramani, I.L. Markov, and K.A. Sakallah.

622: %\newblock {Solving Difficult SAT Instances in the Presence of

623:   %Symmetry}, in {\em {SAT}-2002}, pages 338--345, 2002.

624: 

625: \bibitem{bn79}

626: M.D. Beeler and P.E. O'Neil.

627: \newblock  {Some new van der Waerden numbers}, {\em Discrete

628:   Mathematics}, 28:135--146, 1979.

629: 

630: \bibitem{be68} E. Berlekamp. A construction for partitions which avoid

631: long arithmetic progressions. {\em Canadian Mathematical Bulletin} 

632: 11:409--414, 1968.

633: 

634: %\bibitem{cglr96}

635: %J.~Crawford, M.~Ginsberg, E.~Luks, and A.~Roy.

636: %\newblock  {Symmetry-Breaking Predicates for Search Problems}, in

637:   %{\em KR-96, Proceedings of the Fifth International Conference on Knowledge

638:   %Representation and Reasoning}, pages 148--159, Morgan-Kaufmann, 2002.

639: 

640: %\bibitem{dll62}

641: %M.~Davis, G.~Logemann, and D.~Loveland.

642: %\newblock  A machine program for theorem-proving, {\em

643:   %Communications of the Association for Computing Machinery}, 7:394--397, 1962.

644: 

645: \bibitem{dp60}

646: M.~Davis and H.~Putnam.

647: \newblock  A computing procedure for quantification theory, {\em

648:   Journal of the Association for Computing Machinery}, 7:201--215, 1960.

649: 

650: \bibitem{et01a}

651: D. East and M. Truszczy\'nski. Propositional satisfiability in answer-set

652: programming. Proceedings of Joint German/Austrian Conference on

653: Artificial Intelligence, KI'2001. Lecture Notes in Artificial

654: Intelligence, Springer Verlag 2174, pages 138--153. (Full version

655: available at \url{http://xxx.lanl.gov/ps/cs.LO/0211033}). 2001.

656: 

657: \bibitem{er52}

658: P.~{Erd\"os} and R.~Rado.

659: \newblock  Combinatorial theorems on classifications of subsets of

660: a given set, {\em Proceedings of London Mathematical Society}, 2:417--439,

661: 1952.

662: 

663: \bibitem{posit}

664: J.W. Freeman.

665: \newblock  {\em {Improvements to propositional satisfiability

666:   search algorithms}}, PhD thesis, Department of Computer Science, University

667:   of Pennsylvania, 1995.

668: 

669: %\bibitem{ex94}

670: %{G. Exoo}.

671: %\newblock  {A Lower Bound for Schur Numbers and Multicolor Ramsey

672:   %Numbers of $K_3$}, {\em Electronic International Journal of Combinatorics},

673:   %1:1--3, 1995.

674: %

675: %\bibitem{gj79}

676: %M.R. Garey and D.S. Johnson.

677: %\newblock  {\em Computers and Intractability}, Freeman, 1979.

678: 

679: \bibitem{berkmin}  

680: E. Goldberg, Y. Novikov. 

681: BerkMin: a Fast and Robust SAT-Solver. DATE-2002, pages 142--149, 2002.

682: 

683: \bibitem{dg02}

684: D. Goldstein.

685: \newblock Personal communication, 2002.

686: 

687: \bibitem{go01} T. Gowers. A new proof of Szemer\'edi theorem. {\em

688: Geometric and Functional Analysis}, 11:465-588, 2001.

689: 

690: \bibitem{grs90}

691: R.L. Graham, B.L. Rotschild, and J.H. Spencer.

692: \newblock  {\em Ramsey Theory}, Wiley, 1990.

693: 

694: \bibitem{hj63}

695: A.~Hales and R.I. Jewett.

696: \newblock  Regularity and positional games, {\em Transactions of

697:   American Mathematical Society}, 106:222--229, 1963.

698: 

699: \bibitem{jw90}

700: R.E. Jeroslaw and J.~Wang.

701: \newblock  solving propositional satisfiability problems, {\em

702:   Annals of Mathematics and Artificial Intelligence}, 1:167--187, 1990.

703: 

704: \bibitem{lt03}

705: L. Liu and M. Truszczy\'nski. Local-search techniques in propositional

706: logic extended with cardinality atoms. In preparation.

707: 

708: %\bibitem{kim95}

709: %J.H. Kim.

710: %\newblock  The {R}amsey number $r(3,t)$ has order of magnitude

711: %$t^2/\log t$, {\em Random Structures and Algorithms}, 7:173--207, 1995.

712: 

713: %

714: \bibitem{ss99}

715: J.P. Marques-Silva and K.A. Sakallah.

716: \newblock  {GRASP}: {A} new search algorithm for satisfiability,

717:   {\em {IEEE Transactions on Computers}}, 48:506--521, 1999.

718: 

719: %\bibitem{mr95}

720: %B.D. McKay and S.P. Radziszowski.

721: %\newblock  {$R(4,5) = 25$}, {\em Journal of Graph Theory},

722: %19:309--322, 1995.

723: 

724: %

725: \bibitem{mmzzm01}

726: M.W. Moskewicz, C.F. Magidan, Y.~Zhao, L.~Zhang, and S.~Malik.

727: \newblock  Chaff: engineering an efficient {SAT} solver, in {\em

728:   SAT 2001}, 2001.

729: 

730: %\bibitem{ra01}

731: %S.P. Radziszowski.

732: %\newblock  {Small Ramsey Numbers}, {\em Electronic International

733: %Journal of Combinatorics}, 8:1--38, 2001.

734: %\newblock Annual review of results in Computational Ramsey Theory, Revision 8.

735: %

736: \bibitem{ra28}

737: F.P. Ramsey.

738: \newblock  On a problem of formal logic, {\em Proceedings of London

739: Mathematical Society}, 30:264--286, 1928.

740: 

741: \bibitem{skc94}

742: B. Selman, H.A. Kautz, and B. Cohen.

743: \newblock Noise Strategies for Improving Local Search. {\em Proceedings

744: of AAAI'94}, pp. 337-343. MIT Press 1994.

745: 

746: \bibitem{sh88}

747: S.~Shelah.

748: \newblock  {Primitive recursive bounds for van der Waerden

749:   numbers}, {\em Journal of American Mathematical Society}, 1:683--697, 1988.

750: 

751: \bibitem{sz75}

752: E. Szemer{\'e}di.

753: \newblock {On sets of integers containing no $k$ elements in arithmetic

754: progression}, {\em Acta Arithmetica}, 27:199--243, 1975.

755: 

756: \bibitem{vdw27}

757: B.L. van~der Waerden.

758: \newblock  {Beweis einer Baudetschen Vermutung}, {\em Nieuwe

759:   Archief voor Wiskunde}, 15:212--216, 1927.

760: 

761: \bibitem{sato}

762: H.~Zhang.

763: \newblock  {SATO: An efficient propositional prover}, in {\em

764:   Proceedings of CADE-17}, pages 308--312, 1997.

765: \newblock Springer Lecture Notes in Artificial Intelligence 1104.

766: 

767: \def\BibNewMarkings{2}

768: \end{thebibliography}

769: 

770: %\newpage

771: \section*{Appendix}

772: 

773: Using a complete SAT solver we computed

774: the library of all partitions (up to isomorphism) of $[75]$ showing 

775: that $75 < W(4,3)$. Two of these 30 partitions are shown below:\\

776: \\

777: \noindent

778: Solution 1:\\

779: {\small

780: Block 1: 6 7 9 14 18 20 23 24 36 38 43 44 46 51 55 57 60 61 73 75\\

781: Block 2: 4 5 12 22 26 28 29 31 37 41 42 49 59 63 65 66 68 74 \\

782: Block 3: 1 2 8 10 11 13 17 27 34 35 39 45 47 48 50 54 64 71 72 \\    

783: Block 4: 3 15 16 19 21 25 30 32 33 40 52 53 56 58 62 67 69 70} \\

784: \ \\ 

785: Solution 2:\\ 

786: {\small

787: Block 1: 6 7 9 14 18 20 23 24 36 38 43 44 46 51 55 57 60 61 73 \\

788: Block 2: 4 5 12 22 26 28 29 31 37 41 42 49 59 63 65 66 68 74\\ 

789: Block 3: 1 2 8 10 11 13 17 27 34 35 39 45 47 48 50 54 64 71 72\\

790: Block 4: 3 15 16 19 21 25 30 32 33 40 52 53 56 58 62 67 69 70 75}\\ 

791: \ \\

792: These two and the remaining 28 partitions can be found at

793: \url{http://www.cs.uky.edu/ai/vdw/} \\

794: \ \\ 

795: \noindent

796: Next, we exhibit a partition of $[1295]$ into two blocks demonstrating

797: that $W(2,8)$ \\

798: $> 1295$.\\

799: \ \\

800: {\small

801: \noindent

802: Block 1:\\

803: 1 3 4 5 7 8 10 11 13 14 15 16 17 18 21 26 27 29 31 35 38 40 42 43 45 46 51 53 56 62 63 64 67 68 69 71 73 74 75 77 79 80 83 85 86 88 90 94 96 97 98 101 102 103 104 107 110 112 114 116 118 120 123 124 125 130 131 132 135 138 139 142 145 149 152 153 155 157 159 160 161 163 165 166 169 170 171 174 178 179 181 187 188 189 190 192 193 195 198 200 202 205 207 208 209 210 211 212 213 215 216 221 222 224 225 226 228 229 231 232 236 241 247 249 252 253 254 255 259 260 261 262 264 267 268 269 270 272 274 277 278 279 286 288 290 292 293 294 295 296 297 298 301 306 308 309 311 312 313 317 319 320 321 322 323 326 327 328 334 335 336 338 342 346 349 356 358 359 360 367 368 369 370 373 374 377 378 379 382 383 384 385 386 388 395 396 398 399 400 401 402 404 405 408 410 413 414 416 417 420 423 424 426 429 430 433 434 436 437 443 445 446 447 448 449 451 452 453 456 459 463 464 467 469 470 473 475 476 477 478 479 481 485 486 487 488 490 491 494 495 497 499 502 503 504 505 507 508 510 513 515 518 521 522 528 529 530 533 534 539 540 542 546 547 550 555 558 559 560 561 564 571 577 578 579 580 581 583 584 587 589 590 591 594 595 596 597 601 609 611 612 613 614 615 616 618 619 623 624 625 626 627 628 632 634 636 637 639 640 642 643 647 648 651 652 653 660 661 662 663 665 666 668 670 674 675 676 677 678 680 681 683 684 687 688 690 694 695 696 697 698 700 701 702 703 704 706 709 710 715 717 718 722 725 726 727 728 734 739 742 743 744 746 748 752 753 755 756 757 759 763 766 768 770 771 774 775 776 779 781 788 792 795 796 799 801 802 806 807 809 812 816 817 818 819 821 825 826 832 833 835 836 840 841 843 844 845 846 847 848 852 853 855 856 859 862 863 864 867 868 871 872 874 875 876 877 879 881 882 885 886 893 897 898 899 901 902 903 904 905 906 908 909 910 913 915 917 922 923 925 927 928 929 930 931 932 936 937 939 940 941 944 946 947 948 951 952 954 957 960 961 963 964 965 966 967 974 977 982 983 984 986 989 990 993 994 1001 1003 1004 1008 1009 1010 1012 1013 1016 1017 1020 1022 1023 1025 1026 1028 1029 1033 1034 1036 1037 1038 1040 1045 1047 1050 1051 1052 1053 1058 1060 1065 1070 1073 1074 1075 1076 1077 1079 1083 1085 1087 1088 1089 1090 1091 1092 1094 1095 1096 1097 1098 1102 1103 1105 1106 1109 1111 1113 1116 1117 1118 1119 1121 1123 1124 1126 1129 1130 1133 1135 1139 1140 1141 1144 1150 1151 1152 1154 1155 1156 1157 1159 1161 1168 1170 1171 1174 1175 1179 1180 1184 1185 1186 1188 1189 1190 1191 1194 1196 1197 1200 1202 1205 1206 1213 1216 1217 1218 1219 1220 1221 1222 1224 1226 1227 1229 1234 1236 1237 1238 1239 1246 1247 1249 1251 1253 1257 1260 1261 1262 1263 1264 1268 1269 1272 1274 1275 1276 1278 1279 1283 1285 1286 1287 1288 1289 1290 1291 1294 1295\\

804: Block 2:\\

805: 2 6 9 12 19 20 22 23 24 25 28 30 32 33 34 36 37 39 41 44 47 48 49 50 52 54 55 57 58 59 60 61 65 66 70 72 76 78 81 82 84 87 89 91 92 93 95 99 100 105 106 108 109 111 113 115 117 119 121 122 126 127 128 129 133 134 136 137 140 141 143 144 146 147 148 150 151 154 156 158 162 164 167 168 172 173 175 176 177 180 182 183 184 185 186 191 194 196 197 199 201 203 204 206 214 217 218 219 220 223 227 230 233 234 235 237 238 239 240 242 243 244 245 246 248 250 251 256 257 258 263 265 266 271 273 275 276 280 281 282 283 284 285 287 289 291 299 300 302 303 304 305 307 310 314 315 316 318 324 325 329 330 331 332 333 337 339 340 341 343 344 345 347 348 350 351 352 353 354 355 357 361 362 363 364 365 366 371 372 375 376 380 381 387 389 390 391 392 393 394 397 403 406 407 409 411 412 415 418 419 421 422 425 427 428 431 432 435 438 439 440 441 442 444 450 454 455 457 458 460 461 462 465 466 468 471 472 474 480 482 483 484 489 492 493 496 498 500 501 506 509 511 512 514 516 517 519 520 523 524 525 526 527 531 532 535 536 537 538 541 543 544 545 548 549 551 552 553 554 556 557 562 563 565 566 567 568 569 570 572 573 574 575 576 582 585 586 588 592 593 598 599 600 602 603 604 605 606 607 608 610 617 620 621 622 629 630 631 633 635 638 641 644 645 646 649 650 654 655 656 657 658 659 664 667 669 671 672 673 679 682 685 686 689 691 692 693 699 705 707 708 711 712 713 714 716 719 720 721 723 724 729 730 731 732 733 735 736 737 738 740 741 745 747 749 750 751 754 758 760 761 762 764 765 767 769 772 773 777 778 780 782 783 784 785 786 787 789 790 791 793 794 797 798 800 803 804 805 808 810 811 813 814 815 820 822 823 824 827 828 829 830 831 834 837 838 839 842 849 850 851 854 857 858 860 861 865 866 869 870 873 878 880 883 884 887 888 889 890 891 892 894 895 896 900 907 911 912 914 916 918 919 920 921 924 926 933 934 935 938 942 943 945 949 950 953 955 956 958 959 962 968 969 970 971 972 973 975 976 978 979 980 981 985 987 988 991 992 995 996 997 998 999 1000 1002 1005 1006 1007 1011 1014 1015 1018 1019 1021 1024 1027 1030 1031 1032 1035 1039 1041 1042 1043 1044 1046 1048 1049 1054 1055 1056 1057 1059 1061 1062 1063 1064 1066 1067 1068 1069 1071 1072 1078 1080 1081 1082 1084 1086 1093 1099 1100 1101 1104 1107 1108 1110 1112 1114 1115 1120 1122 1125 1127 1128 1131 1132 1134 1136 1137 1138 1142 1143 1145 1146 1147 1148 1149 1153 1158 1160 1162 1163 1164 1165 1166 1167 1169 1172 1173 1176 1177 1178 1181 1182 1183 1187 1192 1193 1195 1198 1199 1201 1203 1204 1207 1208 1209 1210 1211 1212 1214 1215 1223 1225 1228 1230 1231 1232 1233 1235 1240 1241 1242 1243 1244 1245 1248 1250 1252 1254 1255 1256 1258 1259 1265 1266 1267 1270 1271 1273 1277 1280 1281 1282 1284 1292 1293

806: \ \\

807: }

808: \ \\

809: \noindent

810: Next, we exhibit a partition of $[650]$ into three blocks demonstrating

811: that $W(3,5)$ \\

812: $> 650$.\\

813: \ \\

814: {\small

815: \noindent

816: Block 1:\\

817: 1 2 5 6 10 16 18 21 22 23 27 28 31 35 40 44 45 46 55 56 58 59 67 69 73 75 81 82 84 85 86 95 96 97 100 102 103 105 107 110 111 117 121 122 127 130 131 132 133 136 138 141 142 147 148 152 155 156 157 158 163 165 168 171 175 180 181 183 185 186 189 203 207 210 211 212 215 216 218 221 223 225 227 236 238 240 241 242 247 250 252 254 256 259 260 261 262 266 271 277 280 282 287 288 290 291 292 296 300 302 306 310 328 330 331 334 340 345 346 347 348 350 355 362 365 366 367 371 374 375 378 380 383 384 386 390 392 393 395 396 397 399 400 405 407 408 411 412 413 422 433 435 436 439 443 448 449 453 455 456 457 460 463 472 481 485 486 491 493 500 503 505 506 508 509 511 515 517 521 524 525 528 530 532 535 543 548 550 551 552 560 561 565 566 568 569 571 575 583 585 587 596 597 598 607 608 610 616 620 624 625 626 629 630 640 641 642 646\\

818: \noindent

819: Block 2:\\

820: 3 4 7 8 9 12 15 24 26 29 32 34 37 39 42 43 49 51 60 61 63 65 68 70 71 74 76 78 79 80 83 87 89 90 91 94 109 112 113 115 118 120 129 134 135 139 140 143 145 149 153 159 160 162 164 167 172 173 176 177 178 179 188 190 195 197 200 205 209 213 214 217 219 220 222 224 230 232 233 234 235 239 244 245 248 249 253 255 270 273 275 279 281 284 285 286 297 299 301 305 308 315 318 323 324 325 327 332 333 335 336 338 339 342 343 344 349 354 356 357 358 360 361 364 368 369 370 377 379 382 385 387 389 394 398 410 415 418 424 425 426 430 432 437 440 445 446 450 452 458 461 465 468 471 474 475 476 480 482 483 487 488 490 492 495 496 499 504 514 519 520 523 526 527 529 534 537 539 540 545 549 555 558 567 570 572 574 577 579 580 581 582 584 588 590 593 599 600 602 604 605 611 612 614 615 618 619 633 636 637 639 644 645 648\\

821: \noindent

822: Block 3:\\

823: 11 13 14 17 19 20 25 30 33 36 38 41 47 48 50 52 53 54 57 62 64 66 72 77 88 92 93 98 99 101 104 106 108 114 116 119 123 124 125 126 128 137 144 146 150 151 154 161 166 169 170 174 182 184 187 191 192 193 194 196 198 199 201 202 204 206 208 226 228 229 231 237 243 246 251 257 258 263 264 265 267 268 269 272 274 276 278 283 289 293 294 295 298 303 304 307 309 311 312 313 314 316 317 319 320 321 322 326 329 337 341 351 352 353 359 363 372 373 376 381 388 391 401 402 403 404 406 409 414 416 417 419 420 421 423 427 428 429 431 434 438 441 442 444 447 451 454 459 462 464 466 467 469 470 473 477 478 479 484 489 494 497 498 501 502 507 510 512 513 516 518 522 531 533 536 538 541 542 544 546 547 553 554 556 557 559 562 563 564 573 576 578 586 589 591 592 594 595 601 603 606 609 613 617 621 622 623 627 628 631 632 634 635 638 643 647 649 650

824: \ \\

825: }

826: \ \\

827: \noindent

828: Finally, we exhibit a partition of $[408]$ into four blocks demonstrating

829: that $W(4,4) > 408$.\\

830: \ \\

831: {\small

832: \noindent

833: Block 1:\\

834: 2 8 11 17 19 20 23 30 38 42 48 50 52 59 61 65 67 71 78 82 83 85 89 90 98 104 107 108 113 119 120 124 127 129 140 143 144 147 150 152 157 158 163 166 181 183 184 198 199 204 214 220 223 226 231 237 240 241 244 250 251 253 259 264 266 270 271 273 278 282 286 287 289 306 312 314 317 318 321 327 329 331 348 351 354 359 361 362 363 366 373 377 378 382 383 386 399 401 402 403 406

835: 

836: \noindent

837: Block 2:\\

838: 1 3 7 13 15 16 24 26 28 37 39 47 49 57 58 66 73 76 77 81 84 86 87 92 93 94 103 110 111 117 118 121 122 123 125 133 135 151 153 154 155 161 162 167 170 172 176 182 190 194 195 196 207 210 216 228 232 233 234 242 243 245 246 248 249 254 255 256 258 262 275 280 283 284 290 293 297 298 299 305 307 309 328 333 336 341 346 352 353 355 356 358 368 370 371 372 381 385 391 393 404

839: 

840: \noindent

841: Block 3:\\

842: 4 6 21 22 27 29 31 32 34 35 40 41 44 56 62 63 69 70 72 74 75 79 95 96 99 101 105 109 114 115 116 126 132 134 136 141 145 159 160 165 169 171 174 175 179 180 187 188 191 192 197 200 201 208 209 212 217 219 221 227 229 235 236 247 257 263 267 269 272 274 276 281 291 292 294 300 302 304 310 311 322 324 325 330 332 334 339 340 342 344 345 350 365 367 376 379 388 390 394 397 398 400 407

843: 

844: \noindent

845: Block 4:\\

846: 5 9 10 12 14 18 25 33 36 43 45 46 51 53 54 55 60 64 68 80 88 91 97 100 102 106 112 128 130 131 137 138 139 142 146 148 149 156 164 168 173 177 178 185 186 189 193 202 203 205 206 211 213 215 218 222 224 225 230 238 239 252 260 261 265 268 277 279 285 288 295 296 301 303 308 313 315 316 319 320 323 326 335 337 338 343 347 349 357 360 364 369 374 375 380 384 387 389 392 395 396 405 408

847: }\\

848: \ \\

849: \noindent

850: Configurations showing the validity of other lower bounds listed in 

851: Table \ref{table.vdw1} are available at 

852: \url{http://www.cs.uky.edu/ai/vdw/}.

853: \end{document}

854: 

855: 

856: 138--153", NOTE = "Full version available at \url{http://xxx.lanl.gov/ps/cs.LO/0211033}", YEAR=2001,}

857: 

858: