Tuyển tập các báo cáo nghiên cứu khoa học trên tạp chí toán học quốc tế đề tài: Satisfiability and computing van der Waerden numbers. | Satisfiability and computing van der Waerden numbers Michael R. Dransfield National Security Agency Information Assurance Directorate Ft. Meade MD 20755 Victor W. Marek Department of Computer Science University of Kentucky Lexington KY 40506-0046 Lengning Liu Department of Computer Science University of Kentucky Lexington KY 40506-0046 Miroslaw Truszczynski Department of Computer Science University of Kentucky Lexington KY 40506-0046 Submitted Oct 23 2002 Accepted Jun 10 2004 Published Jun 16 2004 MR Subject Classifications 05D10 Abstract In this paper we bring together the areas of combinatorics and propositional 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 propositional 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 propositional 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 propositional theories that arise in this research can be of use in development testing and benchmarking of SAT solvers. 1 Introduction In this paper we discuss how the areas of propositional satisfiability and combinatorics can help advance each other. On one hand we show that recent dramatic improvements This is an expanded and updated version of the conference paper 4 . THE ELECTRONIC JOURNAL OF COMBINATORICS 11 2004 R41
