TY - CHAP

T1 - Satisfiability and computing van der Waerden numbers

AU - Dransfield, Michael R.

AU - Marek, Victor W.

AU - Truszczyński, Mirosław

PY - 2004

Y1 - 2004

N2 - In this paper we bring together the areas of combinatorics and prepositional satisfiability. Many combinatorial theorems establish, often constructively, the existence of positive integer functions, without actually providing their closed algebraic form or tight lower and upper bounds. The area of Ramsey theory is especially rich in such results. Using the problem of computing van der Waerden numbers as an example, we show that these problems can be represented by parameterized prepositional theories in such a way that decisions concerning their satisfiability determine the numbers (function) in question. We show that by using general-purpose complete and local-search techniques for testing prepositional satisfiability, this approach becomes effective - competitive with specialized approaches. By following it, we were able to obtain several new results pertaining to the problem of computing van der Waerden numbers. We also note that due to their properties, especially their structural simplicity and computational hardness, prepositional theories that arise in this research can be of use in development, testing and benchmarking of SAT solvers.

AB - In this paper we bring together the areas of combinatorics and prepositional satisfiability. Many combinatorial theorems establish, often constructively, the existence of positive integer functions, without actually providing their closed algebraic form or tight lower and upper bounds. The area of Ramsey theory is especially rich in such results. Using the problem of computing van der Waerden numbers as an example, we show that these problems can be represented by parameterized prepositional theories in such a way that decisions concerning their satisfiability determine the numbers (function) in question. We show that by using general-purpose complete and local-search techniques for testing prepositional satisfiability, this approach becomes effective - competitive with specialized approaches. By following it, we were able to obtain several new results pertaining to the problem of computing van der Waerden numbers. We also note that due to their properties, especially their structural simplicity and computational hardness, prepositional theories that arise in this research can be of use in development, testing and benchmarking of SAT solvers.

UR - http://www.scopus.com/inward/record.url?scp=35048880130&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35048880130&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-24605-3_1

DO - 10.1007/978-3-540-24605-3_1

M3 - Chapter

AN - SCOPUS:35048880130

SN - 3540208518

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 1

EP - 13

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Giunchiglia, Enrico

A2 - Tacchella, Armando

ER -