On the van der Waerden numbers w(2; 3, t)
From MaRDI portal
Publication:400514
DOI10.1016/J.DAM.2014.05.007zbMATH Open1298.05313arXiv1102.5433OpenAlexW1706312069WikidataQ29037270 ScholiaQ29037270MaRDI QIDQ400514FDOQ400514
Tanbir Ahmed, Oliver Kullmann, Hunter Snevily
Publication date: 22 August 2014
Published in: Discrete Applied Mathematics (Search for Journal in Brave)
Abstract: We present results and conjectures on the van der Waerden numbers w(2;3,t) and on the new palindromic van der Waerden numbers pdw(2;3,t). We have computed the new number w(2;3,19) = 349, and we provide lower bounds for 20 <= t <= 39, where for t <= 30 we conjecture these lower bounds to be exact. The lower bounds for 24 <= t <= 30 refute the conjecture that w(2;3,t) <= t^2, and we present an improved conjecture. We also investigate regularities in the good partitions (certificates) to better understand the lower bounds. Motivated by such reglarities, we introduce *palindromic van der Waerden numbers* pdw(k; t_0,...,t_{k-1}), defined as ordinary van der Waerden numbers w(k; t_0,...,t_{k-1}), however only allowing palindromic solutions (good partitions), defined as reading the same from both ends. Different from the situation for ordinary van der Waerden numbers, these "numbers" need actually to be pairs of numbers. We compute pdw(2;3,t) for 3 <= t <= 27, and we provide lower bounds, which we conjecture to be exact, for t <= 35. All computations are based on SAT solving, and we discuss the various relations between SAT solving and Ramsey theory. Especially we introduce a novel (open-source) SAT solver, the tawSolver, which performs best on the SAT instances studied here, and which is actually the original DLL-solver, but with an efficient implementation and a modern heuristic typical for look-ahead solvers (applying the theory developed in the SAT handbook article of the second author).
Full work available at URL: https://arxiv.org/abs/1102.5433
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- PSATO: A distributed propositional prover and its application to quasigroup problems
- Theory and Applications of Satisfiability Testing
- Constraint satisfaction problems in clausal form. II: Minimal unsatisfiability and conflict structure
- The \(Multi\)-SAT algorithm
- A machine program for theorem-proving
- Small Ramsey numbers
- A new method to construct lower bounds for van der Waerden numbers
- Bounds on some van der Waerden numbers
- Satisfiability and computing van der Waerden numbers
- Branching rules for satisfiability
- Generalising unit-refutation completeness and SLUR via nested input resolution
- Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10--13, 2004. Revised selected papers.
- Ramsey theory applications
- Computing the van der Waerden number \(W(3,4)=293\)
- On computation of exact van der Waerden numbers
- Generalising and Unifying SLUR and Unit-Refutation Completeness
- Top-Down Algorithms for Constructing Structured DNNF: Theoretical and Practical Implications
- The van der Waerden NumberW(2, 6) Is 1132
- Tutorial on Model Checking: Modelling and Verification in Computer Science
- Some new van der Waerden numbers and some van der Waerden-type numbers
- On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
- Some Progression-Free Partitions Constructed using Folkman's Method
- Two Techniques for Minimizing Resolution Proofs
- Green-Tao Numbers and SAT
- Partitioning SAT Instances for Distributed Solving
- Two New Van Der Waerden Numbers: w(2; 3, 17) and w(2; 3, 18)
- Software Verification for Weak Memory via Program Transformation
- Some new van der Waerden numbers
- A parallelization scheme based on work stealing for a class of SAT solvers
- Theory and applications of satisfiability testing -- SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11--14, 2010. Proceedings
Cited In (10)
- On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
- Projection heuristics for binary branchings between sum and product
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Title not available (Why is that?)
- Title not available (Why is that?)
- Some results on a class of mixed van der Waerden numbers
- Computing the van der Waerden number \(W(3,4)=293\)
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- The SAT+CAS method for combinatorial search with applications to best matrices
- New lower bounds for van der Waerden numbers
Uses Software
This page was built for publication: On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q400514)
