Rado Numbers and SAT Computations

Abstract

Given a linear equation $\mathcal{E}$, the $k$-color Rado number $R_k(\mathcal{E})$ is the smallest integer $n$ such that every $k$-coloring of $\{1,2,3,\dots ,n\}$ contains a monochromatic solution to $\mathcal{E}$. The degree of regularity of $\mathcal{E}$, denoted $dor(\mathcal{E})$, is the largest value $k$ such that $R_k(\mathcal{E})$ is finite. In this article we present new theoretical and computational results about the Rado numbers $R_3(\mathcal{E})$ and the degree of regularity of three-variable equations $\mathcal{E}$. % We use SAT solvers to compute many new values of the three-color Rado numbers $R_3(ax+by+cz=0)$ for fixed integers $a,b,$ and $c$. We also give a SAT-based method to compute infinite families of these numbers. In particular, we show that the value of $R_3(x-y=(m-2)z)$ is equal to $m^3-m^2-m-1$ for $m\ge 3$. This resolves a conjecture of Myers and implies the conjecture that the generalized Schur numbers $S(m,3)=R_3(x_1+x_2+\dots x_{m-1}=x_m)$ equal $m^3-m^2-m-1$ for $m\ge 3$. Our SAT solver computations, combined with our new combinatorial results, give improved bounds on $dor(ax+by=cz)$ and exact values for $1\le a,b,c\le 5$. We also give counterexamples to a conjecture of Golowich.