Rado Numbers and SAT Computations

TL;DR

This paper combines theoretical analysis and SAT solver computations to determine new values and bounds for three-color Rado numbers and the degree of regularity of certain linear equations, resolving existing conjectures.

Contribution

It introduces a SAT-based method for computing Rado numbers, proves a specific formula for Rado numbers of certain equations, and provides new bounds and counterexamples in the study of Rado numbers.

Findings

Rado number R_3(x - y = (m-2)z) equals m^3 - m^2 - m - 1 for m ≥ 3

Confirmed the conjecture that generalized Schur numbers S(m,3) equal m^3 - m^2 - m - 1 for m ≥ 3

Provided improved bounds on the degree of regularity for equations with coefficients up to 5

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.