TITLE: The Method in the Madness: New lower bounds for Van der Waerden numbers

PRESENTER: Marijn Heule, http://www.st.ewi.tudelft.nl/~marijn, marijn@heule.nl

AFFILIATION:Delft University of Technology, The Netherlands, http://www.st.ewi.tudelft.nl

DATE: Friday 9th October 2009

TIME: 12:00:00

PLACE: CSE Seminar Room, L1 K17_113

ABSTRACT:

Chaos does not exist. It is impossible to avoid certain patterns ad
infinitum. The Ramsey theory offers several of these patterns. A very
hard combinatorial problem within this theory is computing Van der
Waerden numbers W(r,k). These numbers represent the smallest n such
that partitioning {1,2,...,n} into r sets, at least one set contains
an arithmetic progression of length k. Visualization of Van der
Waerden numbers and the best known lower bounds reveal some symmetries.
We propose to translate the problem into satisfiability (SAT),
add constraints forcing symmetry to it - as observed in the
visualizations - and solve the resulting problem with a SAT solver.
The additional (symmetry) constraints reduce the search-space
significantly, yielding improved lower bounds to some Van der Waerden
numbers.

BIOGRAPHY OF SPEAKER:

Marijn Heule is a postdoc within the Algorithmics Group of the TU Delft,
Faculty of Engineering, Mathematics and Computer Science (EWI),
Department of Software Technology.
His research focuses on development of algorithms to solve instances of
the satisfiability problem (SAT). One of the results of this research
is his SAT solver march which won several awards during the SAT
competitions. Recently, he started developing a local search solver
called UnitMarch and a cardinality solver.
Besides SAT, he is interested in other hard combinatorial problems
such as the Van der Waerden numbers. For these numbers, he discovered
various improved lower bounds. Some of them where obtained using SAT
solvers. Recently, he became fascinated by the Eternity 2 puzzle.
His research is currently supported by the Dutch Organisation of
Scientific Research (NWO), at the TU Delft.

In addition to his research, Marijn helped set up the Journal on
Satisfiability, Boolean Modeling and Computation (JSAT) and now
contributes to this journal as a production editor. At Delft University,
he gives courses in Satisfiability, supervises several graduate students
and advises them on their masters' theses.

Host:

Toby Walsh

Seminar Convenor:

Van Hai Ho