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 Maximalevel related to Ramsey theory
(for example the known numbers).
 In module
ComputerAlgebra/Satisfiability/Lisp/Generators
we provide various SATtranslations.
 In module
ComputerAlgebra/Hypergraphs/Lisp/Generators
we have various hypergraphgenerators related to Ramsey theory.
 There are also various C++ implementations of generators.
 Papers by OK on this subject are found
here
.
GreenTao numbers
Van der Waerden numbers

Van der Waerden numbers
are an important case of Ramseytype 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 vanderWaerden numbers vdw_2(3,k).
 This is a sequence with conjectured quadratic growth,
where the SAT problems seems best solved by lookahead
solvers.
 The known (precise) values are available as sequence
A007783
in the `OnLine Encyclopedia of Integer Sequences'.
 The palindromic vanderWaerden numbers vdw_2^pd(3,k).
 This is a variation on vdw_2(3,k), obtained by imposing
the restriction of selfsymmetry.
 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 `OnLine Encyclopedia of Integer Sequences'.
 Several instances for the
SAT 2011 competition
.
 In this context the CubeandConquer method was
developed; the preprint is available
here .
Oliver Kullmann
Last modified: Thu Aug 9 23:02:23 BST 2012