# Ramsey Theory and SAT

• This page gives an overview on the exploration of the connections between Ramsey theory and SAT in the context of the OKlibrary .
• Relevant modules within the OKlibrary:
• In module Experimentation/Investigations/RamseyTheory we document our investigations.
• In module ComputerAlgebra/RamseyTheory/Lisp we provide functions at Maxima-level related to Ramsey theory (for example the known numbers).
• In module ComputerAlgebra/Satisfiability/Lisp/Generators we provide various SAT-translations.
• In module ComputerAlgebra/Hypergraphs/Lisp/Generators we have various hypergraph-generators related to Ramsey theory.
• There are also various C++ implementations of generators.
• Papers by OK on this subject are found here .

## Van der Waerden numbers

• Van der Waerden numbers are an important case of Ramsey-type numbers.
• The first technical report is On the van der Waerden numbers w(2;3,t) .
• The two main topics of this report are:
• The van-der-Waerden numbers vdw_2(3,k).
• This is a sequence with conjectured quadratic growth, where the SAT problems seems best solved by look-ahead solvers.
• The known (precise) values are available as sequence A007783 in the `On-Line Encyclopedia of Integer Sequences'.
• The palindromic van-der-Waerden numbers vdw_2^pd(3,k).
• This is a variation on vdw_2(3,k), obtained by imposing the restriction of self-symmetry.
• We have two numbers p < q here: until p everything is satisfiable, from q on everything is unsatisfiable.
• While inbetween we have alternation.
• q is a lower bound on vdw_2(3,k).
• The known (precise) values are available as sequences A198684 , A198685 , in the `On-Line Encyclopedia of Integer Sequences'.
• Several instances for the SAT 2011 competition .
• In this context the Cube-and-Conquer method was developed; the preprint is available here .

Oliver Kullmann