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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Beeler, M.D., O’Neil, P.E.: Some new van der Waerden numbers. Discrete Mathematics 28, 135–146 (1979)
Berlekamp, E.: A construction for partitions which avoid long arithmetic progressions. Canadian Mathematical Bulletin 11, 409–414 (1968)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7, 201–215 (1960)
East, D., Truszczyński, M.: Propositional satisfiability in answer-set programming. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001. LNCS (LNAI), vol. 2174, pp. 138–153. Springer, Heidelberg (2001)
Erdös, P., Rado, R.: Combinatorial theorems on classifications of subsets of a given set. Proceedings of London Mathematical Society 2, 417–439 (1952)
Freeman, J.W.: Improvements to propositional satisfiability search algorithms. PhD thesis, Department of Computer Science, University of Pennsylvania (1995)
Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust SAT-Solver. In: DATE 2002, pp. 142–149 (2002)
Goldstein, D.: Personal communication (2002)
Gowers, T.: A new proof of Szemerédi theorem. Geometric and Functional Analysis 11, 465–588 (2001)
Graham, R.L., Rotschild, B.L., Spencer, J.H.: Ramsey Theory. Wiley, Chichester (1990)
Hales, A., Jewett, R.I.: Regularity and positional games. Transactions of American Mathematical Society 106, 222–229 (1963)
Jeroslaw, R.E., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence 1, 167–187 (1990)
Liu, L., Truszczyński, M.: Local-search techniques in propositional logic extended with cardinality atoms (in preparation)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. IEEE Transactions on Computers 48, 506–521 (1999)
Moskewicz, M.W., Magidan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: SAT 2001 (2001)
Ramsey, F.P.: On a problem of formal logic. Proceedings of London Mathematical Society 30, 264–286 (1928)
Selman, B., Kautz, H.A., Cohen, B.: Noise Strategies for Improving Local Search. In: Proceedings of AAAI 1994, pp. 337–343. MIT Press, Cambridge (1994)
Shelah, S.: Primitive recursive bounds for van der Waerden numbers. Journal of American Mathematical Society 1, 683–697 (1988)
Szemerédi, E.: On sets of integers containing no k elements in arithmetic progression. Acta Arithmetica 27, 199–243 (1975)
van der Waerden, B.L.: Beweis einer Baudetschen Vermutung. Nieuwe Archief voor Wiskunde 15, 212–216 (1927)
Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of CADE-17. LNCS (LNAI), vol. 1104, pp. 308–312. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dransfield, M.R., Marek, V.W., Truszczyński, M. (2004). Satisfiability and Computing van der Waerden Numbers. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive