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.

Green-Tao numbers

• Green-Tao numbers are a refinement of van-der-Waerden numbers based on the Green-Tao theorem .
• See slides for a talk OK gave in the PCV seminar (Swansea, Computer Science) May 2010 on the initial phase of investigations into the connection between Ramsey theory and SAT, focusing on Green-Tao numbers.
• The underlying report is Exact Ramsey Theory: Green-Tao numbers and SAT .
• The accompanying conference paper (SAT 2010) is Green-Tao Numbers and SAT (the slides for the conference talk are a shortened version of the above PCV-seminar slides).
• Several instances for the SAT 2011 competition .

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 .

Last modified: Tue Nov 1 01:05:45 GMT 2011