Satisfiability and computing van der Waerden numbers

MaRDI QIDQ1883655zbMATH OpenFDO

Authors Michael R. Dransfield, Lengning Liu, Wiktor Marek, Mirosław Truszczyński

Publication date 13 October 2004

Published in The Electronic Journal of Combinatorics (Search for Journal in Brave)

Full work available at URL https://eudml.org/doc/124096, http://www.emis.de/journals/EJC/Volume_11/Abstracts/v11i1r41.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

computing van der Waerden numberspropositional satisfiabilityRamsey theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ramsey theory (05D10) Analysis of algorithms and problem complexity (68Q25)

Review text

Summary: 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 parametrized 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.

Recommendations

• Theory and Applications of Satisfiability Testing
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• On computation of exact van der Waerden numbers
• Theory and Applications of Satisfiability Testing
• Green-Tao Numbers and SAT

Cited in

(14)

• Optimal symmetry breaking for graph problems
• On orthogonal symmetric chain decompositions
• A novel SAT solver for the van der Waerden numbers
• Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• Weak Schur numbers and the search for G. W. Walker's lost partitions
• Green-Tao Numbers and SAT
• The packing chromatic number of the infinite square lattice is between 13 and 15
• Theory and Applications of Satisfiability Testing
• On the \(n\)-color weak Rado numbers for the equation \(x_1+x_2+\cdots +x_k+c=x_{k+1}\)
• Theory and Applications of Satisfiability Testing
• On orthogonal symmetric chain decompositions
• On generalized Schur numbers of the equation x+ay=z
• Bounds on some van der Waerden numbers

This page was built for publication: Satisfiability and computing van der Waerden numbers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1883655)