Computer Science – Discrete Mathematics
Scientific paper
2010-04-05
Theory and Applications of Satisfiability Testing - SAT 2010, LNCS 6175, 352-362
Computer Science
Discrete Mathematics
25 pages; a shortened version appears in LNCS (Springer), "Theory and Applications of Satisfiability Testing - SAT 2010", edit
Scientific paper
10.1007/978-3-642-14186-7_32
We consider the links between Ramsey theory in the integers, based on van der Waerden's theorem, and (boolean, CNF) SAT solving. We aim at using the problems from exact Ramsey theory, concerned with computing Ramsey-type numbers, as a rich source of test problems, where especially methods for solving hard problems can be developed. In order to control the growth of the problem instances, we introduce "transversal extensions" as a natural way of constructing mixed parameter tuples (k_1, ..., k_m) for van-der-Waerden-like numbers N(k_1, ..., k_m), such that the growth of these numbers is guaranteed to be linear. Based on Green-Tao's theorem we introduce the "Green-Tao numbers" grt(k_1, ..., k_m), which in a sense combine the strict structure of van der Waerden problems with the (pseudo-)randomness of the distribution of prime numbers. Using standard SAT solvers (look-ahead, conflict-driven, and local search) we determine the basic values. It turns out that already for this single form of Ramsey-type problems, when considering the best-performing solvers a wide variety of solver types is covered. For m > 2 the problems are non-boolean, and we introduce the "generic translation scheme", which offers an infinite variety of translations ("encodings") and covers the known methods. In most cases the special instance called "nested translation" proved to be far superior.
No associations
LandOfFree
Exact Ramsey Theory: Green-Tao numbers and SAT does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Exact Ramsey Theory: Green-Tao numbers and SAT, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Exact Ramsey Theory: Green-Tao numbers and SAT will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-637506