Abstract
We aim at using the problems from exact Ramsey theory, concerned with computing Ramsey-type numbers, as a rich source of test problems for SAT solving, targeting especially hard problems. Particularly we consider the links between Ramsey theory in the integers, based on van der Waerden’s theorem, and (boolean, CNF) SAT solving. Based on Green-Tao’s theorem (“the primes contain arbitrarily long arithmetic progressions”) we introduce the Green-Tao numbers grt m k 1, ..., k m , which in a sense combine the strict structure of van der Waerden problems with the quasi-randomness of the distribution of prime numbers. In general the problem sizes become quickly infeasible here, but we show that for transversal extensions these numbers only grow linearly, thus having a method at hand to produce more problem instances of feasible sizes. Using standard SAT solvers (look-ahead, conflict-driven, and local search) we determine the basic Green-Tao numbers. It turns out that already for this single case of a Ramsey-type problem, when considering the best-performing solvers a wide variety of solver types is covered. This is different to van der Waerden problems, where apparently only simple look-ahead solvers succeed (regarding complete methods). For m > 2 the problems are non-boolean, and we introduce the generic translation scheme for translating non-boolean clause-sets to boolean clause-set. This general method 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 over its competitors (including the direct translation).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ahmed, T.: Some new van der Waerden numbers and some van der Waerden-type numbers. INTEGERS: Electronic Journal of Combinatorial Number Theory 9, 65–76 (2009)
Ahmed, T.: Two new van der Waerden numbers: w(2;3,17) and w(2;3,18). To appear in INTEGERS: Electronic Journal of Combinatorial Number Theory (2010)
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)
Braunstein, A., Mézard, M., Zecchina, R.: Survey propagation: An algorithm for satisfiability. Random Structures and Algorithms 27(2), 201–226 (2005)
Dransfield, M.R., Liu, L., Marek, V.W., Truszczyński, M.: Satisfiability and computing van der Waerden numbers. The Electronic Journal of Combinatorics 11(#R41) (2004)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Green, B., Tao, T.: The primes contain arbitrarily long arithmetic progressions. Annals of Mathematics 167(2), 481–547 (2008)
Herwig, P.R., Heule, M.J.H., van Lambalgen, P.M., van Maaren, H.: A new method to construct lower bounds for van der Waerden numbers. The Electronic Journal of Combinatorics 14(#R6) (2007)
Heule, M.J.H.: SMART solving: Tools and techniques for satisfiability solvers. PhD thesis, Technische Universiteit Delft, ISBN 978-90-9022877-8 (2008)
Büning, H.K., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, et al. (eds.) [3], ch. 11, pp. 339–401.
Kouril, M., Paul, J.L.: The van der Waerden number W(2,6) is 1132. Experimental Mathematics 17(1), 53–61 (2008)
Kullmann, O.: Investigating the behaviour of a SAT solver on random formulas. Technical Report CSR 23-2002, Swansea University, Computer Science Report Series, 119 pages (October 2002), http://www-compsci.swan.ac.uk/reports/2002.html
Kullmann, O.: The OK library: Introducing a holistic research platform for (generalised) SAT solving. Studies in Logic 2(1), 20–53 (2009)
Kullmann, O.: Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability. Technical Report TR 07-055, version 02, Electronic Colloquium on Computational Complexity (ECCC) (January 2009)
Kullmann, O.: Fundaments of branching heuristics. In: Biere, et al. (eds.) [3], ch. 7, pp. 205–244
Kullmann, O.: Constraint satisfaction problems in clausal form I: Autarkies and deficiency. In: Fundamenta Informaticae (to appear, 2010)
Kullmann, O.: Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure. In: Fundamenta Informaticae (to appear, 2010)
Kullmann, O.: Exact Ramsey theory: Green-Tao numbers and SAT. Technical Report arXiv:1004.0653v2 [cs.DM], arXiv (April 2010)
Landman, B.M., Robertson, A.: Ramsey Theory on the Integers. Student mathematical library, vol. 24. American Mathematical Society, Providence (2003) ISBN 0-8218-3199-2
Li, C.M.: A constraint-based approach to narrow search trees for satisfiability. Information Processing Letters 71(2), 75–80 (1999)
Prestwich, S.: CNF encodings. In: Biere, et al. (eds.) [3], ch. 2, pp. 75–97
Tompkins, D.A.D., Hoos, H.H.: UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H. H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005)
van der Waerden, B.L.: Beweis einer Baudetschen Vermutung. Nieuw Archief voor Wiskunde 15, 212–216 (1927)
Zhang, H.: Combinatorial designs by SAT solvers. In: Biere, et al. (eds.) [3], ch. 17, pp. 533–568
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kullmann, O. (2010). Green-Tao Numbers and SAT. In: Strichman, O., Szeider, S. (eds) Theory and Applications of Satisfiability Testing – SAT 2010. SAT 2010. Lecture Notes in Computer Science, vol 6175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14186-7_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-14186-7_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14185-0
Online ISBN: 978-3-642-14186-7
eBook Packages: Computer ScienceComputer Science (R0)