On SAT Solvers and Ramsey-type Numbers

Burcu Canakci; Hannah Christenson; Robert Fleischman; William Gasarch; Nicole McNabb; Daniel Smolyak

paper

On SAT Solvers and Ramsey-type Numbers

arXiv:2312.01159

Abstract

We created and parallelized two SAT solvers to find new bounds on some Ramsey-type numbers. For $c > 0$ , let $R_{c} (L)$ be the least $n$ such that for all $c$ -colorings of the $[n] \times [n]$ lattice grid there will exist a monochromatic right isosceles triangle forming an $L$ . Using a known proof that $R_{c} (L)$ exists we obtained $R_{3} (L) \leq 2593$ . We formulate the $R_{c} (L)$ problem as finding a satisfying assignment of a boolean formula. Our parallelized probabilistic SAT solver run on eight cores found a 3-coloring of $20 \times 20$ with no monochromatic $L$ , giving the new lower bound $R_{3} (L) \geq 21$ . We also searched for new computational bounds on two polynomial van der Waerden numbers, the "van der Square" number $R_{c} (V S)$ and the "van der Cube" number $R_{c} (V C)$ . $R_{c} (V S)$ is the least positive integer $n$ such that for some $c > 0$ , for all $c$ -colorings of $[n]$ there exist two integers of the same color that are a square apart. $R_{c} (V C)$ is defined analogously with cubes. For $c \leq 3$ , $R_{c} (V S)$ was previously known. Our parallelized deterministic SAT solver found $R_{4} (V S)$ = 58. Our parallelized probabilistic SAT solver found $R_{5} (V S) > 180$ , $R_{6} (V S) > 333$ , and $R_{3} (V C) > 521$ . All of these results are new.

8 pages, 1 figure. Unpublished