††thanks<EMAIL_ADDRESS>
# Rado Numbers and SAT Computations

Yuan Chang  Department of Mathematics, University of California, Davis
1 Shields Ave
Davis, CA 95616  Jesús A. De Loera<EMAIL_ADDRESS>Department of
Mathematics, University of California, Davis
1 Shields Ave
Davis, CA 95616  William J. Wesley<EMAIL_ADDRESS>Department of
Mathematics, University of California, Davis
1 Shields Ave
Davis, CA 95616

##  1 Introduction

A well-known result in arithmetic Ramsey theory is _Schur’s theorem_ , which
states that for any $k\geq 1$, there is an integer $n$ such that every
$k$-coloring of $[n]:=\\{1,2,3,\dots,n\\}$ induces a monochromatic solution to
$x+y=z$ [24]. The _Schur number_ $S(k)$ is the smallest such $n$ with this
property. It is very difficult to compute $S(k)$ and the largest known Schur
number is $S(5)=161$, which was computed in 2018 using SAT solving techniques
and created great attention with its massive parallel computation [15]. In
this paper we follow this symbolic approach to investigate natural variations
of Schur numbers.

The _Rado numbers_ are a generalization of Schur numbers, and are of great
importance in arithmetic Ramsey theory (see [12, 17, 19] and the references
below). For a given linear equation $\mathcal{E}$, the _$k$ -color Rado
number_ $R_{k}(\mathcal{E})$ is the smallest number $n$ such that every
$k$-coloring of $[n]$ induces a monochromatic solution to $\mathcal{E}$, or
infinity if there is a $k$-coloring of $\mathbb{N}$ with no monochromatic
solution to $\mathcal{E}$. Many 2-color Rado numbers for various types of
equations have been computed in, for example, [18, 23, 21, 16]. Explicit
formulas for the Rado numbers $R_{2}(a(x-y)=bz)$ and $R_{2}(a(x+y)=bz)$ are
given in [17] and [13]. However, no such formula is known for the general case
$R_{2}(ax+by=cz)$. There are some computations of 3-color Rado numbers
scattered throughout the literature [18, 22, 20], but Rado numbers with more
than two colors have not been studied as often. We present a systematic study
of these numbers.

Another interesting family of numbers is the _generalized Schur numbers_
$S(m,k)=R_{k}(x_{1}+\dots+x_{m-1}=x_{m})$. In [4] it was shown that
$S(m,3)\geq m^{3}-m^{2}-m-1$, and it was conjectured in [1] and later proved
in [8] that $S(m,3)=m^{3}-m^{2}-m-1$. Myers showed in [18] that the numbers
$R_{k}(x-y=(m-2)z)$ give an upper bound for $S(m,k)$, and several more values
of $R_{k}(x-y=(m-2)z)$ were shown to be equal to $S(m,k)$, thus giving exact
values for more generalized Schur numbers. Myers went on to make the following
conjecture in [18].

######  Conjecture 1.1 (Myers).

$R_{3}(x-y=(m-2)z)=m^{3}-m^{2}-m-1$ for $m\geq 3$.

In this paper we focus on computing Rado numbers for three variable linear
homogeneous equations using SAT-based methods described in Section 2. The main
contributions of this paper are exact formulas for several families of 3-color
Rado numbers. In particular, we show Conjecture 1.1 is true.

######  Theorem 1.2.

The values of the following Rado numbers are known:

  1. 1.

$R_{3}(x-y=(m-2)z)=m^{3}-m^{2}-m-1$ for $m\geq 3.$

  2. 2.

$R_{3}(a(x-y)=(a-1)z)=a^{3}+(a-1)^{2}$ for $a\geq 3$.

  3. 3.

$R_{3}(a(x-y)=bz)=a^{3}$ for $b\geq 1$, $a\geq b+2$, $gcd(a,b)=1$.

As a corollary, we obtain the result in [8], an exact formula for the 3-color
generalized Schur numbers.

######  Corollary 1.2.1.

$S(m,3)=m^{3}-m^{2}-m-1$ for $m\geq 1$.

We also compute exactly several 3-color and 4-color Rado numbers.

######  Theorem 1.3.

The values of the following Rado numbers are known.

  1. 1.

$R_{3}(a(x-y)=bz)$ for $1\leq a,b\leq 15$.

  2. 2.

$R_{3}(a(x+y)=bz)$ for $1\leq a,b\leq 10$.

  3. 3.

$R_{3}(ax+by=cz)$ for $1\leq a,b,c\leq 6$.

  4. 4.

$R_{4}(x-y=az)$ for $1\leq a\leq 4$.

  5. 5.

$R_{4}(a(x-y)=z)$ for $1\leq a\leq 5$.

We collect the 3-color Rado number values we computed in Theorem 1.3 in Tables
1 to 8. We also give the additional values $R_{3}(ax+ay=bz)$ for $3\leq a\leq
6,\ 11\leq b\leq 20$ as well as our values for $R_{4}(a(x-y)=bz)$ in the
Appendix (Tables 9 and 10). Underlined entries in these tables correspond to
equations whose coefficients are not coprime.

Table 1: 3-color Rado numbers $R_{3}(a(x-y)=bz)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
1 | 14 | 14 | 27 | 64 | 125 | 216 | 343 | 512 | 729 | 1000 | 1331 | 1728 | 2197 | 2744 | 3375
2 | 43 | 14 | 31 | 14 | 125 | 27 | 343 | 64 | 729 | 125 | 1331 | 216 | 2197 | 343 | 3375
3 | 94 | 61 | 14 | 73 | 125 | 14 | 343 | 512 | 27 | 1000 | 1331 | 64 | 2197 | 2744 | 125
4 | 173 | 43 | 109 | 14 | 141 | 31 | 343 | 14 | 729 | 125 | 1331 | 27 | 2197 | 343 | 3375
5 | 286 | 181 | 186 | 180 | 14 | 241 | 343 | 512 | 729 | 14 | 1331 | 1728 | 2197 | 2744 | 27
6 | 439 | 94 | 43 | 61 | 300 | 14 | 379 | 73 | 31 | 125 | 1331 | 14 | 2197 | 343 | 125
7 | 638 | 428 | 442 | 456 | 470 | 462 | 14 | 561 | 729 | 1000 | 1331 | 1728 | 2197 | 14 | 3375
8 | 889 | 173 | 633 | 43 | 665 | 109 | 644 | 14 | 793 | 141 | 1331 | 31 | 2197 | 343 | 3375
9 | 1198 | 856 | 94 | 892 | 910 | 61 | 896 | 896 | 14 | 1081 | 1331 | 73 | 2197 | 2744 | 125
10 | 1571 | 286 | 1171 | 181 | 43 | 186 | 1190 | 180 | 1206 | 14 | 1431 | 241 | 2197 | 343 | 31
11 | 2014 | 1508 | 1530 | 1552 | 1574 | 1596 | 1618 | 1584 | 1575 | 1580 | 14 | 1849 | 2197 | 2744 | 3375
12 | 2533 | 439 | 173 | 94 | 2005 | 43 | 2053 | 61 | 109 | 300 | 2024 | 14 | 2341 | 379 | 141
13 | 3134 | 2432 | 2458 | 2484 | 2510 | 2536 | 2562 | 2588 | 2574 | 2530 | 2541 | 2544 | 14 | 2913 | 3375
14 | 3823 | 638 | 3039 | 428 | 3095 | 442 | 43 | 456 | 3207 | 470 | 3113 | 462 | 3146 | 14 | 3571
15 | 4606 | 3676 | 286 | 3736 | 94 | 181 | 3826 | 3856 | 186 | 61 | 3795 | 180 | 3835 | 3836 | 14
Table 2: 3-color Rado numbers $R_{3}(a(x+y)=bz)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10
---|---|---|---|---|---|---|---|---|---|---
1 | 14 | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$
2 | 1 | 14 | 243 | $\underline{\infty}$ | $\infty$ | $\underline{\infty}$ | $\infty$ | $\underline{\infty}$ | $\infty$ | $\underline{\infty}$
3 | 54 | 54 | 14 | 384 | 2000 | $\underline{\infty}$ | $\infty$ | $\infty$ | $\underline{\infty}$ | $\infty$
4 | $\infty$ | 1 | 108 | 14 | 875 | 243 | 4459 | $\underline{\infty}$ | $\infty$ | $\underline{\infty}$
5 | $\infty$ | 105 | 135 | 180 | 14 | 864 | $3430$ | 3072 | 12393 | $\underline{\infty}$
6 | $\infty$ | 54 | 1 | 54 | 750 | 14 | $3087$ | 384 | 243 | 2000
7 | $\infty$ | 455 | 336 | 308 | 875 | $756$ | 14 | $1536$ | 8748 | 7500
8 | $\infty$ | $\infty$ | 432 | 1 | 1000 | 108 | $2744$ | 14 | 8019 | 875
9 | $\infty$ | $\infty$ | 54 | 585 | 1125 | 54 | 3087 | 1224 | 14 | 6000
10 | $\infty$ | $\underline{\infty}$ | 1125 | 105 | 1 | 135 | 3430 | 180 | 7290 | 14

If the number $R_{k}(\mathcal{E})$ is finite for a fixed $k$, we say that the
equation $\mathcal{E}$ is _$k$ -regular_. If $\mathcal{E}$ is $k$-regular for
all $k\geq 1$, we say $\mathcal{E}$ is _regular_. In its simplest version,
Rado’s classical theorem gives necessary and sufficient conditions for when a
linear homogeneous equation is regular [19].

######  Theorem 1.4 (Rado).

A linear equation $\sum_{i=1}^{m}c_{i}x_{i}=0$ with $c_{i}\in\mathbb{Z}$ is
regular if and only if there exists a nonempty subset of the $c_{i}$ that sums
to zero.

Nonregular equations may have finite Rado numbers for small $k$. The largest
$k$ for which an equation $\mathcal{E}$ is $k$-regular is the _degree of
regularity_ of $\mathcal{E}$, denoted $dor(\mathcal{E})$. We set
$dor(\mathcal{E}):=\infty$ if $\mathcal{E}$ is regular. Rado also proved a
theorem that characterized the 2-regular linear homogeneous equations in three
or more variables.

######  Theorem 1.5 (Rado).

Let $m\geq 3$ and $a_{1},\dots,a_{m}\in\mathbb{Z}\setminus\\{0\\}.$ Then the
equation $\sum_{i=1}^{m}a_{i}x_{i}=0$ is 2-regular if and only if there exists
$i$ and $j$ such that $a_{i}>0$ and $a_{j}<0$.

For $3\leq k<\infty$, there is no known characterization of the $k$-regular
equations. In [2] it was shown that for every $k$, there exists a linear
homogeneous equation in $k+1$ variables that has degree of regularity $k$.
However, for a fixed number of variables, the question of what degrees of
regularity are possible for homogeneous linear equations remains largely
unanswered. Rado made the following conjecture about this question in his
Ph.D. thesis [19].

Table 3: $R_{3}(ax+by=z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6
---|---|---|---|---|---|---
1 | 14 | 43 | 94 | 173 | 286 | 439
2 |  | $\infty$ | 1093 | $\infty$ | 2975 | 4422
3 |  |  | $\infty$ | $\infty$ | $\infty$ | $\infty$
4 |  |  |  | $\infty$ | $\infty$ | $\infty$
5 |  |  |  |  | $\infty$ | $\infty$
6 |  |  |  |  |  | $\infty$

Table 4: $R_{3}(ax+by=2z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6
---|---|---|---|---|---|---
1 | 1 | 14 | 54 | $\infty$ | 70 | 126
2 |  | 14 | 61 | 43 | 181 | 94
3 |  |  | 243 | $\infty$ | 395 | 648
4 |  |  |  | $\underline{\infty}$ | $\infty$ | $\underline{1093}$
5 |  |  |  |  | $\infty$ | $\infty$
6 |  |  |  |  |  | $\underline{\infty}$

Table 5: $R_{3}(ax+by=3z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6
---|---|---|---|---|---|---
1 | 54 | 1 | 27 | 54 | 89 | 195
2 |  | 54 | 31 | $\infty$ | 140 | 108
3 |  |  | 14 | 109 | 186 | 43
4 |  |  |  | 384 | 220 | $\infty$
5 |  |  |  |  | 2000 | 1074
6 |  |  |  |  |  | $\underline{\infty}$

Table 6: $R_{3}(ax+by=4z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6
---|---|---|---|---|---|---
1 | $\infty$ | $\infty$ | 1 | 64 | 100 | $\infty$
2 |  | 1 | $\infty$ | 14 | $\infty$ | 54
3 |  |  | 108 | 73 | 105 | $\infty$
4 |  |  |  | 14 | 180 | 61
5 |  |  |  |  | 141 | $\infty$
6 |  |  |  |  |  | 31

Table 7: $R_{3}(ax+by=5z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6
---|---|---|---|---|---|---
1 | $\infty$ | 45 | 60 | 1 | 125 | 150
2 |  | 105 | 1 | $\infty$ | 125 | 70
3 |  |  | 135 | 100 | 125 | 108
4 |  |  |  | 180 | 141 | $\infty$
5 |  |  |  |  | $\underline{14}$ | 300
6 |  |  |  |  |  | 864

Table 8: $R_{3}(ax+by=6z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5 | 6
---|---|---|---|---|---|---
1 | $\infty$ | 40 | 81 | $\infty$ | 1 | 216
2 |  | 54 | 81 | 1 | 90 | 27
3 |  |  | 1 | $\infty$ | 135 | 14
4 |  |  |  | 54 | $\infty$ | 31
5 |  |  |  |  | 750 | 241
6 |  |  |  |  |  | 14

######  Conjecture 1.6 (Rado’s Boundedness Conjecture).

For all $m\geq 1$, there is a number $\Delta(m)$ such that if a linear
equation in $m$ variables is $\Delta(m)$-regular, then it is regular.

In [10] it was shown that Rado’s boundedness conjecture is true if it is true
for the case of homogeneous equations. Those authors also proved the first
nontrivial case of the conjecture by showing that if a linear homogeneous
equation in three variables is 24-regular, then it is regular. However, it is
not known if 24 is the best possible bound. There are no known examples of a
nonregular linear homogeneous equation in three variables that is 4-regular.
Moreover, in [10], several coloring lemmas give more precise bounds on the
degree of regularity of 3-variable linear homogeneous equations. We contribute
further improvements on their results and compute the degree of regularity of
all sufficiently small equations $ax+by=cz$.

######  Theorem 1.7.

The degree of regularity of the equation $ax+by=cz$ is known for all $1\leq
a,b,c\leq 5$.

We also mention a related conjecture of Golowich [11].

######  Conjecture 1.8.

For each positive integer $k$ there is an integer $m(k)$ such that for any
$m\geq m(k)$, any linear homogeneous equation in $m$ variables with nonzero
integer coefficients not all of the same sign is $k-$regular.

We provide counterexamples to the Golowich conjecture. We show that for all
$m,k\geq 3$ there is a linear homogeneous equation in $m$ variables that is
not $k$-regular.

######  Theorem 1.9.

For all $m,k\geq 3$, there is a linear homogeneous equation $\mathcal{E}$ in
$m$ variables that is not $k$-regular. In particular,

$x_{1}+\dots+x_{m-1}=\lceil(m-1)^{\frac{k-1}{k-2}}\rceil x_{m}$

is not $k$-regular. Thus Conjecture 1.8 is false.

As a corollary, for $m\geq 3$ there exists a linear homogeneous equation in
$m$ variables with degree of regularity exactly 2.

######  Corollary 1.9.1.

For all $m\geq 3$, there is a linear homogeneous equation $\mathcal{E}$ in $m$
variables with $dor(\mathcal{E})=2$. In particular,

$dor(x_{1}+\dots+x_{m-1}=(m-1)^{2}x_{m})=2.$

This paper is organized as follows: in Section 2 we give background on SAT
solving and the computational methods we used to compute Rado numbers. Section
3 gives several lemmas used to obtain improved bounds on the degree of
regularity of certain families of equations. In Section 4 we introduce a new
SAT method to compute families of Rado numbers and prove our main results.
Section 5 gives additional details on the computational aspects of this
project. The Appendix contains additional tables of Rado numbers and
experimental data.

##  2 SAT Solving and Encoding

In this section we explain how to encode the problem of finding Rado numbers
as an instance of SAT and describe additional techniques used to increase
performance. The code used for our computations can be found at [9].

###  2.1 Background on Satisfiability

A _literal_ is a Boolean variable or its negation. A _clause_ is a logical
disjunction of literals, and a Boolean formula is in _conjunctive normal form_
(CNF) if it is a logical conjunction of clauses.

The Boolean satisfiability problem (SAT) is the problem of determining whether
a given Boolean formula is satisfiable, i.e., there is a true/false assignment
to the literals that makes the formula true. Any Boolean formula can be
expressed in conjunctive normal form, and most SAT solvers take CNF formulas
as input.

####  2.1.1 Encoding of the Problem

The problem of computing Rado numbers can be encoded as an instance of SAT.
Given an equation $\mathcal{E}$ and positive integers $n,k$, we construct a
formula $F_{n}^{k}(\mathcal{E})$ that is satisfiable if and only if there
exists a $k$-coloring of $[n]$ that does not contain a monochromatic solution
to $\mathcal{E}$. Therefore if $F_{n}^{k}(\mathcal{E})$ is satisfiable, then
$R_{k}(\mathcal{E})>n$, and otherwise $R_{k}(\mathcal{E})\leq n$. We use the
variables $v_{j}^{i}$ that are assigned the value true if and only if the
integer $j$ is colored with color $i$. Following the language used in [15], a
formula $F_{n}^{k}(\mathcal{E})$ consists of three different types of clauses:
_positive, negative,_ and _optional_.

  * •

Positive clauses encode that every number $j$ is assigned at least one color,
and are of the form $v_{j}^{1}\vee v_{j}^{2}\vee\dots\vee v_{j}^{k}$ for
$1\leq j\leq n$.

  * •

Negative clauses encode that there are no monochromatic solutions to
$\mathcal{E}$. If $(x_{1},x_{2},\dots,x_{m})$ is a solution to $\mathcal{E}$,
then its corresponding negative clauses are
$\bar{v}_{x_{1}}^{i}\vee\dots\vee\bar{v}_{x_{m}}^{i}$ for $1\leq i\leq k$.
Every positive integer solution $x$ to $\mathcal{E}$ with $\|x\|_{\infty}\leq
n$ contributes these $k$ negative clauses to $F_{n}^{k}(\mathcal{E})$.

  * •

Optional clauses encode that every number $j$ is assigned at most one color,
and are of the form $\bar{v}_{j}^{i_{1}}\vee\bar{v}_{j}^{i_{2}}$ for $1\leq
j\leq n$ and $1\leq i_{1}<i_{2}\leq k$. These clauses are not strictly
necessary since they do not affect the satisfiability of
$F_{n}^{k}(\mathcal{E})$, but they ensure that satisfying assignments are in
one-to-one correspondence with $k$-colorings of $[n]$ that avoid monochromatic
solutions to $\mathcal{E}$.

######  Example 2.1.

The clauses in the formula $F^{3}_{4}(x+y=z)$ are:

Positive clauses:

$\displaystyle({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}v^{1}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}v^{2}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}v^{3}_{1}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}v^{1}_{2}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}v^{2}_{2}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}v^{3}_{2}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}v^{1}_{3}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}v^{2}_{3}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}v^{3}_{3}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}v^{1}_{4}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}v^{2}_{4}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}v^{3}_{4}})$

Negative clauses:

$\displaystyle({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{3}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{3}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{4}})\wedge$
$\displaystyle({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{3}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{4}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{3}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{4}})\wedge$
$\displaystyle({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{2}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{2}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{3}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{3}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{4}})\wedge$
$\displaystyle({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{2}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{3}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{2}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{2}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{4}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{3}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{4}})\wedge$
$\displaystyle({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{2}})\wedge({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{2}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{3}})\wedge({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{3}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{4}})\wedge$
$\displaystyle({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{2}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{3}})\wedge({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{2}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{2}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{4}})\wedge({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{3}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{4}})$

Optional clauses:

$\displaystyle({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{1}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{1}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{2}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{2}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{2}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{2}})\wedge$
$\displaystyle({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{3}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{3}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{3}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{3}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{3}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{3}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{4}}\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{4}})\wedge({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{4}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{4}})\wedge({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{v}^{2}_{4}}\vee{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\overline{v}^{3}_{4}})$

If we input $F_{4}^{3}(x+y=z)$ into a SAT solver, it will output satisfiable.
The $3-$coloring
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}2},{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}3,4}$,
for example, avoids monochromatic solutions. We remark that even though some
clauses, such as
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{1}}\vee{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overline{v}^{1}_{2}}}$,
contain redundant literals, these literals are removed in a preprocessing
step.

We will use this SAT encoding to prove Theorem 1.3. In Section 5 we give
practical details on this encoding and how to generate formulas efficiently.

##  3 Degree of regularity coloring lemmas

Working towards the goal of computing the degree of regularity and Rado number
for as many equations as possible, in this section we collect several results
on colorings that avoid monochromatic solutions. These colorings give upper
bounds on the degree of regularity of certain equations, and this allows us to
avoid doing unnecessary computations. We are especially interested in cases
where we can show that the degree of regularity of an equation is at most
three. In these cases a computation of a (finite) 3-color Rado number is a
proof that the degree of regularity equals three.

The following result gives two algebraic conditions that guarantee an upper
bound on the degree of regularity. A version of the first condition was proved
in [10].

######  Lemma 3.1.

Let $\mathcal{E}$ be the equation $a_{1}x_{1}+\dots+a_{m-1}x_{m-1}=a_{m}x_{m}$
with $a_{1}\leq a_{2}\leq\dots\leq a_{m-1}$ and $a_{i}>0$ for all $i$. Let
$S:=\sum_{i=1}^{m-1}a_{i}$. Then $\mathcal{E}$ is not $k$-regular if one of
the following conditions holds:

  1. (i)

$S\leq\frac{a_{1}^{k-1}}{a_{m}^{k-2}}$, (ii) $S\leq
a_{1}^{\frac{1}{k-1}}a_{m}^{1-\frac{1}{k-1}}$.

###### Proof.

For the first condition, let
$d:=\left(\frac{S}{a_{m}}\right)^{\frac{1}{k-1}}$. Define the coloring
$\chi(n):=\lceil\log_{d}n\rceil\pmod{k}$. Suppose $(x_{1},\dots,x_{m})$ is a
solution to $\mathcal{E}$, and let $M:=\max\\{x_{1},\dots,x_{m-1}\\}$. Let $i$
be the unique integer such that $M\in(d^{i-1},d^{i}]$. Then
$x_{m}=\frac{\sum_{i=1}^{m-1}a_{i}x_{i}}{a_{m}}\leq d^{k-1}M\leq d^{i+k-1}$.
By hypothesis we have $d^{k-1}\leq\left(\frac{a_{1}}{a_{m}}\right)^{k-1}$.
Therefore $x_{m}\geq\frac{a_{1}M}{a_{m}}\geq dM>d^{i}$. We have shown that
$\chi(x_{m})\in[i+1,i+k-1]$, so $\chi(x_{m})\neq\chi(M)$ and there are no
$\chi$-monochromatic solutions to $\mathcal{E}$.

For the second condition, suppose $S\leq
a_{1}^{\frac{1}{k-1}}a_{m}^{1-\frac{1}{k-1}}$ and that $(x_{1},\dots,x_{m})$
is a solution to $\mathcal{E}$. Again let $M=\max\\{x_{1},\dots,x_{m-1}\\}$,
and let $d=\left(\frac{a_{1}}{a_{m}}\right)^{\frac{1}{k-1}}.$ Define a
$k$-coloring $\chi(n)=\lceil\log_{d}(n)\rceil\pmod{k}$. Suppose
$M\in(d^{i+1},d^{i}]$, so $\chi(M)=i\pmod{k}$. Note $d<1$ since
$a_{1}<S<=a_{1}^{\frac{1}{k-1}}a_{m}^{1-\frac{1}{k-1}}$ implies $a_{1}<a_{m}$.
Then $x_{m}=\frac{\sum_{i=1}^{m-1}a_{i}x_{i}}{a_{m}}\leq\frac{SM}{a_{m}}\leq
dM\leq d^{i+1}$. Moreover, $x_{m}\geq\frac{a_{1}M}{a_{m}}=d^{k-1}M>d^{i+k}$.
Therefore $\lceil\log_{d}x_{m}\rceil\in[i+k-1,i+1]$, so
$\chi(x_{m})\neq\chi(M)$ and there are no $\chi$-monochromatic solutions to
$\mathcal{E}$. ∎

Recall that for any prime $p$, the $p$-adic valuation $v_{p}(x)$ is the
largest integer $n$ such that $p^{n}$ divides $x$. Many useful colorings come
from $p$-adic valuations and studying the divisibility properties of an
equation’s coefficients. We will freely use the fact that
$v_{p}(xy)=v_{p}(x)+v_{p}(y)$ for all integers $x$ and $y$. In [10] the
following result was shown:

######  Lemma 3.2.

Suppose $\mathcal{E}$ is an equation of the form $ax+by+cz=0$ with
$v_{p}(a),v_{p}(b),v_{p}(c)$ all distinct for some prime $p$. Then
$\mathcal{E}$ has degree of regularity at most 3.

If the condition in Lemma 3.2 is strengthened to distinct $p$-adic valuations
modulo 3, then we obtain an improved bound on the degree of regularity.

######  Example 3.3.

Let $\mathcal{E}$ denote the equation $x+2y=4z$. Consider the 3-coloring
$\chi(n)=v_{2}(n)\pmod{3}$. If $(x,y,z)$ is a solution to $\mathcal{E}$ and
$\chi(x)=\chi(y)=\chi(z)$, then $v_{2}(x),v_{2}(2y),$ and $v_{2}(4z)$ are all
distinct since these values are all different modulo 3. Let
$\alpha=\min\\{v_{2}(x),v_{2}(2y),v_{2}(4z)\\}$. Then reducing each side of
$\mathcal{E}$ modulo $p^{\alpha+1}$ gives a contradiction. Therefore $\chi$
induces no monochromatic solutions to $\mathcal{E}$.

The following lemma generalizes the proof in the example above.

######  Lemma 3.4.

Let $\mathcal{E}$ be the equation $\sum_{i=1}^{m}a_{i}x_{i}$. If there is a
prime $p$ for which $v_{p}(a_{i})\not\equiv v_{p}(a_{j})\pmod{k}$ for all
$i\neq j$, then $\mathcal{E}$ is not $k$-regular.

###### Proof.

Define a $k$-coloring $\chi(n):=v_{p}(n)\pmod{k}$. Suppose
$(x_{1},\dots,x_{m})$ is a monochromatic solution to $\mathcal{E}$. Then
$v_{p}(a_{i}x_{i})\neq v_{p}(a_{j}x_{j})$ for $i\neq j$ since these values are
distinct modulo $k$. Let $\alpha=\min_{i=1}^{m}\\{v_{p}(a_{i}x_{i})\\}$. Then
$\sum_{i=1}^{m}a_{i}x_{i}\not\equiv 0\pmod{p^{\alpha}+1}$, so
$\sum_{i=1}^{m}a_{i}x_{i}\neq 0$, a contradiction. ∎

The following two results are similar to Lemma 5 and Lemma 6 in [10]. Here we
show that under additional assumptions on $v_{p}(a+b)$ and $v_{p}(b+c)$,
respectively, it follows that the degrees of regularity of certain equations
are at most six, which is stronger than the corresponding best bounds in [10].
We also show that another hypothesis on the order a particular group element
further improves this upper bound to four.

######  Lemma 3.5.

Let $\mathcal{E}$ denote the equation $ax+by+cz=0$. If $\mathcal{E}$ is not
regular and $0=v_{p}(a)=v_{p}(b)=v_{p}(a+b)<v_{p}(c)=:r$, then
$dor(\mathcal{E})<6$. If additionally the element $-ab^{-1}$ in the
multiplicative group $G=\mathbb{Z}_{p^{r}}^{\times}$ has even order, then
$dor(\mathcal{E})<4$.

###### Proof.

Since $v_{p}(a)=v_{p}(b)=0$, let $g:=-ab^{-1}\in G$. Since $a+b\not\equiv
0\pmod{p^{r}}$, it follows that $g$ is not the identity element of $G$. Let
$\Gamma$ denote the graph with vertex set $\\{1,\dots,p^{r}-1\\}$ and edges
$(x,y)$ if $x\equiv gy\pmod{p^{r}}$ (see Figure 1 for an example). Since
$v_{p}(a+b)=0$, it follows that $-ab^{-1}\not\equiv 1\pmod{p}$, so $\Gamma$ is
loopless. Then $\Gamma$ is a union of disjoint cycles, and each cycle has size
$\frac{ord(g)}{p^{i}}$ for some $i$. If $ord(g)$ is even, then all of the
cycles in $\Gamma$ have even length, and so $\Gamma$ is 2-colorable (note the
conditions $0=v_{p}(a)=v_{p}(b)=v_{p}(a+b)$ imply $p\neq 2$). Otherwise,
$\Gamma$ is 3-colorable since each vertex has degree at most 2. Let $C_{1}$ be
a proper vertex coloring of $\Gamma$ that uses the fewest number of colors. We
will construct a (4- or 6-) coloring $C$ to show that $\mathcal{E}$ is not 4-
or 6- regular and conclude $dor(\mathcal{E})<4$ or $dor(\mathcal{E})<6$,
respectively.

Let $q:=p^{2r}$. For all $n\in\mathbb{N}$, write $n=q^{\alpha}n^{\prime}$ with
$n^{\prime}\not\equiv 0\pmod{q}$. Define the coloring $C_{2}$ to be

$C_{2}(n)=\begin{cases}1&\text{if }n^{\prime}\not\equiv 0\pmod{p^{r}},\\\
2&\text{if }n^{\prime}\equiv 0\pmod{p^{r}}.\end{cases}$

Let $C$ be the product coloring

$C(n)=\begin{cases}(C_{1}(n^{\prime}),1)&\text{if }C_{2}(n)=1\\\
(C_{1}(n^{\prime}/p^{r}),2)&\text{if }C_{2}(n)=2.\\\ \end{cases}.$

We claim that $C$ is a coloring with no monochromatic solutions to
$\mathcal{E}$.

Suppose $(x,y,z)$ is a monochromatic solution to $\mathcal{E}$. Write
$x=q^{\alpha}x^{\prime},y=q^{\beta}y^{\prime},z=q^{\gamma}z^{\prime}$ with
$x^{\prime},y^{\prime},z^{\prime}\nmid q$ and $ax+by+cz=0$. Without loss of
generality, we may assume that at least one of $\alpha,\beta$, and $\gamma$ is
zero, and in each case we will show a contradiction.

Suppose first that $C_{2}(x)=C_{2}(y)=C_{2}(z)=1.$

Case 1: Suppose $\alpha=0$. Then if $\beta>0$, then we may reduce
$\mathcal{E}$ modulo $p^{r}$ to obtain a contradiction since $b,c\equiv
0\pmod{p^{r}}$, but $ax\not\equiv 0\pmod{p^{r}}$. So we may assume $\beta=0$.
Now suppose $ax+by\equiv 0\pmod{p^{r}}$. Then $y\equiv gx\pmod{p^{r}}$. But
this is impossible since $x$ and $y$ would have different colors by the
coloring $C_{1}$ (recall that $\Gamma$ is loopless). Therefore
$ax+by\not\equiv 0\pmod{p^{r}}$, and so $ax+by+cz\not\equiv 0\pmod{p^{r}}$, a
contradiction.

Case 2: The case $\beta=0$ is similar to the case $\alpha=0$.

Case 3: Suppose $\gamma=0$ and $\alpha,\beta>0$. Then $ax+by\equiv 0\pmod{q}$,
but $cz\not\equiv 0\pmod{q}$, and so $ax+by+cz\not\equiv 0\pmod{q},$ a
contradiction. Therefore $\alpha=0$ or $\beta=0$, and the proof follows from
one of the previous cases.

If $C_{2}(x)=C_{2}(y)=C_{2}(z)=2$, then in all cases we may divide
$x^{\prime},y^{\prime},$ and $z^{\prime}$ by $p^{r}$, and the proof follows
similarly.

∎

######  Lemma 3.6.

Let $\mathcal{E}$ denote the equation $ax+by+cz=0$. If $\mathcal{E}$ is not
regular and $0=v_{p}(a)<v_{p}(b)=v_{p}(c)=v_{p}(b+c)=:r$ for some prime $p$,
then $dor(\mathcal{E})<6$. Write $b=p^{r}b^{\prime}$ and $c=p^{r}c^{\prime}$.
If additionally the element $g:=-b^{\prime}c^{\prime-1}$ in the multiplicative
group $G=\mathbb{Z}_{p^{s}}^{\times}$ has even order, then
$dor(\mathcal{E})<4$.

###### Proof.

Since $v_{p}(b+c)=r$ and $v_{p}(b^{\prime})=v_{p}(c^{\prime})=0$, $g\in G$ and
$g$ is not the identity element of $G$. Let $\Gamma$ denote the graph with
vertex set $\\{1,\dots,p^{r}-1\\}$ and edges $(x,y)$ if $x\equiv
gy\pmod{p^{r}}$. Then $\Gamma$ is a union of disjoint cycles, and each cycle
has size $\frac{ord(g)}{p^{i}}$ for some $i$. Note that $\Gamma$ is not
loopless since $v_{p}(b+c)=r$. If $g$ has even order, then $\Gamma$ is
2-colorable, and otherwise $\Gamma$ is 3-colorable. Let $C_{1}$ be a proper
vertex coloring of $\Gamma$ that uses the fewest number of colors. We will
construct a (4- or 6-) coloring $C$ to show that $\mathcal{E}$ is not 4- or 6-
regular and conclude $dor(\mathcal{E})<4$ or $dor(\mathcal{E})<6$,
respectively.

Let $q:=p^{2r}$, and for all $n\in\mathbb{N}$, write $n=q^{\alpha}n^{\prime}$
with $n^{\prime}\not\equiv 0\pmod{p^{2r}}$. Define the coloring $C_{2}$ to be

$C_{2}(n)=\begin{cases}1&\text{if }n^{\prime}\not\equiv 0\pmod{p^{r}},\\\
2&\text{if }n^{\prime}\equiv 0\pmod{p^{r}}.\end{cases}$

Let $C$ be the product coloring

$C(n)=\begin{cases}(C_{1}(n^{\prime}),1)&\text{if }C_{2}(n)=1\\\
(C_{1}(n^{\prime}/p^{r}),2)&\text{if }C_{2}(n)=2.\\\ \end{cases}.$

Suppose $(x,y,z)$ is a monochromatic solution to $\mathcal{E}$ with respect to
$C$. Write
$x=q^{\alpha}x^{\prime},y=q^{\beta}y^{\prime},z=q^{\gamma}z^{\prime}$ with
$x^{\prime},y^{\prime},z^{\prime}\nmid q$ and $ax+by+cz=0$. Without loss of
generality, we may assume that at least one of $\alpha,\beta$, and $\gamma$ is
zero, and in each case we will show a contradiction.

Suppose $C_{2}(x^{\prime})=C_{2}(y^{\prime})=C_{2}(z^{\prime})=1.$ Case 1:
Suppose $\alpha=0$. Then $ax+by+cz\not\equiv 0\pmod{p^{r}}$. Case 2: Suppose
$\alpha>0$ and $\beta=0$. Then if $\gamma>0$, then $ax+by+cz\not\equiv
0\pmod{q}$, so assume $\gamma=0$. If $by+cz\equiv 0\pmod{q}$, then
$z=z^{\prime}\equiv-b^{\prime}c^{\prime-1}y^{\prime}\pmod{p^{r}}$. But by
coloring $C_{1}$ it follows that $z$ and $y$ have different colors, a
contradiction. The case $\gamma=0$ is similar.

Suppose $C_{2}(x^{\prime})=C_{2}(y^{\prime})=C_{2}(z^{\prime})=2$. If
$\alpha=0$, then $ax+by+cz\not\equiv 0\pmod{q}$. The cases $\beta=0,\gamma=0$
are similar to above. ∎

Figure 1: 2-coloring of graph with vertex set [8] and edges $(x,y)$ if
$x\equiv 2y\pmod{9}$.

##  4 Two parameter 3-color Rado numbers

In [17] the formulas for the 2-color Rado numbers $R_{2}(a(x-y)=bz)$ and
$R_{2}(a(x+y)=bz)$, $a,b\geq 0$ are given. However, a formula for the 2-color
Rado numbers $R_{2}(ax+by=cz)$ is unknown. Here we give bounds on some 3-color
Rado numbers of the form $R_{3}(a(x-y)=bz)$ and $R_{3}(a(x+y)=bz)$ and prove
our main results.

###  4.1 Rado Numbers $R_{3}(a(x-y)=bz)$

By Rado’s theorem, the equation $a(x-y)=bz$ is regular. Table 1 gives values
of the 3-color Rado numbers $R_{3}(a(x-y)=bz)$ for $1\leq a,b\leq 15$.

The following lemma gives a simple lower bound on the Rado numbers
$R_{k}(a(x-y)=bz)$.

######  Lemma 4.1.

Suppose $a,b\geq 1$ and $\gcd(a,b)=1$. Then $R_{k}(a(x-y)=bz)\geq a^{k}$.

###### Proof.

Let $v_{a}(n)$ denote the highest power of $a$ that divides $n$. Then
$v_{a}:[1,a^{k}-1]\to\\{0,1,\dots,k-1\\}$ defines a $k-$coloring of
$[1,a^{k}-1]$ that has no monochromatic solutions of $a(x-y)=bz$. To see this,
suppose $(x,y,z)$ is a monochromatic solution in color $c$. If $x\leq y,$ then
there is no $z\in[1,a^{k}-1]$ that satisfies $a(x-y)=bz$, so suppose $x>y$.
Then $x=a^{c}x^{\prime}$ and $y=a^{c}y^{\prime}$, where $a\nmid
x^{\prime},y^{\prime}$. Since $\gcd(a,b)=1$,
$v_{a}(z)=v_{a}(bz)=v_{a}(a(x-y))=v_{a}(a^{c+1}(x^{\prime}-y^{\prime}))\geq
c+1$, a contradiction. ∎

For the case $b=a-1$, we have an improved lower bound on
$R_{3}(a(x-y)=(a-1)z).$

######  Lemma 4.2.

$R_{3}(a(x-y)=(a-1)z)\geq a^{3}+(a-1)^{2}$.

###### Proof.

We will construct a coloring of $[1,a^{3}+(a-1)^{2}-1]$ that induces no
monochromatic solutions to $a(x-y)=(a-1)z$. Define

$\chi(i):=\begin{cases}0&v_{a}(i)=2\text{ or }(v_{a}(i)=0\text{ and
}(i<a^{2}-a\text{ or }i>a^{3}-a)),\\\ 1&v_{a}(i)=1,\\\
2&\text{otherwise.}\end{cases}$

Let $(x,y,z)$ be a positive integer solution to $a(x-y)=(a-1)z$. Suppose
$\chi(x)=\chi(y)=0$. If $v_{a}(x)=v_{a}(y)\geq 2$, then since $a$ and $a-1$
are relatively prime, $v_{a}(z)=v_{a}((a-1)z)=v_{a}(a(x-y))\geq 3$, and
$\chi(z)\neq 0$. If $v_{a}(x)=2$ and $v_{a}(y)=0$, then
$v_{a}(z)=v_{a}(a(x-y))=1$, so $\chi(z)=1$. The case $v_{a}(x)=0$ and
$v_{a}(y)=2$ is similar. Note that $x>y$ since $z$ must be positive. If
$v_{a}(x)=v_{a}(y)=0$, $x\geq a^{3}-a$ and $y\leq a^{2}-a$, then $a(x-y)\geq
a(a^{3}-a^{2})>(a-1)(a^{3}-a)$. Then $z\in[a^{3}-a,a^{3}+(a-1)^{2}-1]$. Since
$(a-1)z=a(x-y)$, it follows that $v_{a}(z)\geq 1$, so $v_{a}(z)\neq 0$. But
the only value $z\in[a^{3}-a,a^{3}+(a-1)^{2}-1]$ with $v_{a}(z)\geq 2$ is
$a^{3}$, so $\chi(z)\neq 0$. Now if $v_{a}(x)=v_{a}(y)=0$ and
$x,y\in[1,a^{2}-a)$ or $x,y\in(a^{3}-a,a^{3}+(a-1)^{2}-1]$, then
$x-y<a^{2}-a$, so $(a-1)z=a(x-y)<a^{3}-a^{2}$. Then $v_{a}(z)\in\\{1,2\\}.$ If
$v_{a}(z)=1$, then $\chi(z)=1\neq 0$. If $v_{a}(z)=2$, then $z\geq a^{2}$ and
$(a-1)z\geq a^{3}-a^{2}$, a contradiction.

Now suppose $\chi(x)=\chi(y)=1$. Then $v_{a}(z)=v_{a}(a(x-y))\geq 2$, so
$\chi(z)\neq 1$.

If $\chi(x)=\chi(y)=2$, then either $v_{a}(x)=v_{a}(y)=0$, or $x=a^{3}$. In
the former case we have $v_{a}(z)=v_{a}(a(x-y))\geq 1$. We have $z\neq a^{3}$
since this implies $x-y=a^{3}-a^{2}$, but this is impossible since
$x,y\in[1,a^{3}-(a-1)^{2}-1]$, and it follows that $\chi(z)\neq 2$. If
$x=a^{3}$, then $y\neq a^{3}$ and $v_{a}(y)=0$. Therefore
$v_{a}(z)=v_{a}(a(x-y))=1$, so $\chi(z)\neq 2$.

Therefore there are no monochromatic solutions to $a(x-y)=(a-1)z$. ∎

###  4.2 3-regularity of $a(x+y)=bz$

In his thesis [19], Rado proved the following result on the family of
equations $a(x+y)=bz$.

######  Theorem 4.3 (Rado).

If $a/b\neq 2^{k}$ for all $k\in\mathbb{Z}$, then $dor(a(x+y)=bz)\leq 3$.

The following lemma strengthens Rado’s result to include the case when
$a/b=2^{k}$ for some integer $k$.

######  Lemma 4.4.

$R_{3}(x+y=bz)=\infty$ for $b\geq 4$, and $R_{3}(a(x+y)=z)=\infty$ for $a\geq
2$. Moreover, $dor(a(x+y)=bz)\leq 3$ unless $a=1,b=2$.

###### Proof.

The results follow immediately from Lemma 3.1 and Theorem 4.3. ∎

Table 2 gives the 3-color Rado numbers $R_{3}(a(x+y)=bz)$ for $1\leq a,b\leq
10.$ We also give the values of some additional Rado numbers for the equations
$a(x+y)=bz$ with $b>10$ in the Appendix.

###  4.3 Proofs of Main Results

In this section we prove Theorem 1.2 using an encoding of the Rado number
problem similar to that in Section 2. The key difference is that in this new
encoding, indices of variables are indexed by symbolic polynomial expressions
rather than fixed integers.

Let $\mathcal{E}$ be a linear equation in $m$ variables, and let $S$ be a set
of polynomials. Let $C\subseteq S^{m}$ be a set of solutions to $\mathcal{E}$.
The variable $v_{s}^{i}$ is assigned the value true if and only if the
expression $s\in S$ is assigned color $i$. Positive and optional clauses are
constructed similarly to the method in Section 2. The negative clauses are
constructed from the solutions in $C$. For example, if $S=\\{ia:1\leq i\leq
7$}, and $\mathcal{E}$ is the equation $x-y=5z$, then $(x,y,z)=(7a,2a,a)$ is a
solution. If $(7a,2a,a)\in C$, then we add the negative clause
$\bar{v}_{7a}^{1}\vee\bar{v}_{2a}^{1}\vee\bar{v}_{a}^{1}$ to our formula. The
following lemma formalizes this procedure and describes how to use these
formulas to compute Rado numbers for families of equations.

######  Lemma 4.5.

Let $\Sigma=\\{\sigma_{1},\dots,\sigma_{\ell}\\}$ be a finite alphabet of
parameters. Let $\mathcal{E}$ be a linear equation in the variables
$x_{1},\dots,x_{m}$ with coefficients in $\Sigma$. Let $S$ be a set of
expressions over $\Sigma$, and let $C\subset S^{m}$ be a set of solutions to
$\mathcal{E}$. We define $F_{k,S,C}(\mathcal{E})$ to be the corresponding
formula for the $k$-color Rado number generated by the clauses from $C$ as
follows.

$\displaystyle F_{k,S,C}(\mathcal{E})$ $\displaystyle:=Pos_{k,S}\wedge
Neg_{k,C}\wedge Opt_{k,S},\text{where}$ $\displaystyle Pos_{k,S}$
$\displaystyle:=\bigwedge_{s\in S}\left(\bigvee_{i=1}^{k}v_{s}^{i}\right),$
$\displaystyle Neg_{k,C}$ $\displaystyle:=\bigwedge_{(s_{1},\dots,s_{m})\in
C}\bigwedge_{i=1}^{k}\bigvee_{j=1}^{m}\bar{v}_{s_{j}}^{i},$ $\displaystyle
Opt_{k,S}$ $\displaystyle:=\bigwedge_{s\in S}\bigwedge_{1\leq i_{1}<i_{2}\leq
k}(\bar{v}_{s}^{i_{1}}\vee\bar{v}_{s}^{i_{2}}).$

Let $A\subset\mathbb{Z}^{\ell}$. If $1\leq s(a)=s(a_{1},\dots,a_{\ell})\leq
f(a)$ for all $s\in S$, $a\in A$ and $F_{k,S}(\mathcal{E})$ is unsatisfiable,
then $R_{k}(\mathcal{E})\leq f(a)$ for all $a\in A$.

In other words, if substituting values for parameters in a formula $F$ always
gives a valid formula, i.e., one whose variables are bounded between 1 and
$n$, then the unsatisfiability of $F$ gives an upper bound on the Rado numbers
for a family of equations. For each equation $\mathcal{E}$ in the family, $F$
is an unsatisfiable subformula in the corresponding Rado number formula for
$\mathcal{E}$.

We are able to prove Conjecture 1.1 using Lemma 4.5.

###### Proof of Theorem 1.2.

For the Rado numbers $R_{3}(x-y=(m-2)z)$, in Lemma 4.5 let $\Sigma=\\{m\\}$,
and let $\mathcal{E}$ be the equation $x-y=(m-2)z$. The set $S$ is a family of
685 polynomials and the set $C$ contains 9468 solutions to $\mathcal{E}$. It
is straightforward to show that $1\leq s(m)\leq m^{3}-m^{2}-m-1$ for all
$m\geq 3$ and all $s\in S$. The formula $F_{3,S}(\mathcal{E})$ was shown to be
unsatisfiable in 0.03 seconds by Satch, proving $R_{3}(x-y=(m-2)z)\leq
m^{3}-m^{2}-m-1$ for $m\geq 3$. By results in [4] and [18], we have
$R_{3}(\mathcal{E})\geq S(m,3)\geq m^{3}-m^{2}-m-1$ for $m\geq 3$, and so
$R_{3}(x-y=(m-2)z)=m^{3}-m^{2}-m-1$ for $m\geq 3$.

For the Rado numbers $R_{3}(a(x-y)=(a-1)z)$, let $\Sigma=\\{a\\}$, and let
$\mathcal{E}$ denote the equation $a(x-y)=(a-1)z$. We constructed a set $S$ of
1365 polynomials and a set $C$ of 20811 solutions to $\mathcal{E}$. It is
again straightforward to show that $1\leq s(a)\leq a^{3}+(a-1)^{2}$ for all
$a\geq 16$ and all $s\in S$. The formula $F_{3,S,C}(\mathcal{E})$ was shown to
be unsatisfiable in 0.05 seconds by Satch, proving $R_{3}(\mathcal{E})\leq
a^{3}+(a-1)^{2}$ for $a\geq 16$. By Lemma 4.2 and Theorem 1.3, it follows that
$R_{3}(\mathcal{E})=a^{3}+(a-1)^{2}$ for $a\geq 3$.

For the Rado numbers $R_{3}(a(x-y)=bz)$, let $\Sigma=\\{a,b\\}$, and let
$\mathcal{E}$ denote the equation $a(x-y)=bz$. We constructed a set $S$ of
40645 polynomials and a set $C$ of 490897 solutions to $\mathcal{E}$. All
polynomials $p(a,b)$ were verified to satisfy $1\leq p(a,b)\leq a^{3}$ for all
integers $a,b$ satisfying $a\geq 16,b\geq 1$, and $a\geq b+2$ using the
software GloptiPoly 3 [14]. Some additional valid inequalities were added to
the region specified in GloptiPoly 3 using elementary calculus techniques. The
formula $F_{3,S,C}$ was shown to be unsatisfiable in 1.72 seconds by Satch,
proving $R_{3}(a(x-y)=bz)\leq a^{3}$ for all $(a,b)$ satisfying $a\geq 16$,
$b\geq 1$, and $a\geq b+2$. By Theorem 1.3 and Lemma 4.1,
$R_{3}(a(x-y)=bz)=a^{3}$ for $a\geq 3,b\geq 1,a\geq b+2$ with $\gcd(a,b)=1$.

For each of these formulas, the sets $S$ and $C$ were constructed using a
heuristic search procedure. We give details of this procedure in the Appendix.

∎

The results in Theorem 1.3 were proven by computer.

###### Proof of Theorem 1.3.

For each finite number $R_{k}(ax+by=cz)$, we produced a $k$-coloring of
$[R_{k}(ax+by=cz)-1]$ that contained no monochromatic solutions to $ax+by=cz$
and verified using a SAT solver that the formula
$F_{R_{k}(ax+by=cz)}^{k}(ax+by=cz)$ from the encoding in Section 2 is
unsatisfiable. For the remaining cases we concluded $R_{3}(ax+by=cz)=\infty$
using Lemma 3.1. ∎

We are now able to prove Theorem 1.7.

###### Proof of Theorem 1.7.

Let $\mathcal{E}$ denote the equation $ax+by=cz$. For each triple $(a,b,c)$
that satisfies $1\leq a,b,c\leq 5$ and $a\leq b$, we performed the following
calculations. If a nonempty subset of $\\{a,b,-c\\}$ sums to zero, then
$dor(\mathcal{E})=\infty$ by Theorem 1.4. If $v_{p}(a),v_{p}(b)$, and
$v_{p}(c)$ are all distinct modulo 3 for some prime $p$, or if one of the
inequalities $a+b\leq\frac{a^{2}}{c}$ or $a+b\leq\sqrt{ac}$ holds, then
$dor(\mathcal{E})=2$ by Lemma 3.4, Lemma 3.1, and Theorem 1.5.

In all other cases $dor(\mathcal{E})\leq 3$ by either Theorem 4.3, Lemma 3.1,
Lemma 3.5, or Lemma 3.6. The computation of a finite Rado number in Theorem
1.3 gives $dor(\mathcal{E})=3$. ∎

We now prove Theorem 1.9 and Corollary 1.9.1

###### Proof of Theorem 1.9 and Corollary 1.9.1.

The proof of Theorem 1.9 is immediate from Lemma 3.1 condition $(ii)$ since
$S=m-1\leq\lceil(m-1)^{\frac{k-1}{k-2}}\rceil^{\frac{k-2}{k-1}}.$ Corollary
1.9.1 follows from Theorem 1.5 and setting $k=3$ in Theorem 1.9. ∎

##  5 Rado CNF file generation

In this section we discuss some of the computational details from our
calculations. The main workflow when computing a Rado number for a given
linear equation $\mathcal{E}$ is the following:

  * •

Generate the CNF file encoding $F_{n}^{k}(\mathcal{E})$.

  * •

Apply symmetry breaking preprocessing.

  * •

Determine the satisfiability of $F_{n}^{k}(\mathcal{E})$ with SAT solvers.

  * •

Adjust $n$ to find the smallest $n$ for which $F_{n}^{k}(\mathcal{E})$ is
unsatisfiable.

In the following subsections, we explain how to achieve each step of the
computation procedure.

###  5.1 Generating CNF Files

Before we compute a given Rado number with a SAT solver, we must write the
formula $F_{n}^{k}(\mathcal{E})$ to a file in DIMACS format (see [7], Chapter
2). For many of our Rado number calculations, this step took far longer than
the SAT solving process. The paper [15] uses divide-and-conquer and several
CPU years to solve a single difficult SAT formula in five colors; in contrast,
we solve many easier problems with only three colors. Generating negative
clauses is the most difficult step as it involves enumerating the positive
integer solutions to $\mathcal{E}$.

####  5.1.1 Generating all solutions

For efficient solution generation to homogeneous linear equations, we used the
built-in function isolve in Maple to parameterize the solutions. We then used
SymPy to parse the output of Maple and generate the solutions with values in
$[1,n]$.

######  Example 5.1.

If we want to generate all integer solutions in the interval $[1,1000]$ for
the equation $43x-5y=13z$, we can feed $43x-5y=13z$ into Maple’s isolve
function, which gives the output

$\\{x=i,y=6i-13j,z=i+5j\\}.$

Since we want all integer solutions within $[1,1000]$, we can loop $i$ from
$1$ to $1000$ and manipulate the inequality

$1\leq y=6i-13j\leq 1000$

into an inner loop where $j$ is looped from $\lceil\frac{1000-6i}{-13}\rceil$
to $\lfloor\frac{1-6i}{-13}\rfloor$. For $z$, we can simply check whether
$1\leq i+5j\leq 1000$ is satisfied or not inside the loops to determine if
$(x,y,z)$ is a solution.

####  5.1.2 Writing Clauses to File

Some of the formulas in our computations contain millions of clauses, and
writing these clauses to a file is a time-consuming part of CNF file
generation. For example, the CNF file which encodes $F_{16397}^{3}(5x+5y=19z)$
contains more than 20 million clauses, of which only $65588$ are positive or
optional.

The algorithm to generate all the positive and optional clauses is done though
Python. Since the parameterization of the equation $\mathcal{E}$ is also
passed to Python, we also used Python to generate the CNF files. We were able
to improve CNF file generation speeds for 3-color Rado numbers by implementing
loop unrolling.

###  5.2 Symmetry Breaking

Symmetry breaking is a SAT solving technique that can lead to drastic speedups
by preventing the solver from looking in isomorphic areas of the search space.
In our case we want to prevent the solver from searching for different
permutations of the same coloring.

We can break this symmetry in the formula $F_{4}^{3}(x+y=z)$, for example, by
adding the clauses
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(v^{1}_{1})}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(v^{2}_{2})}$.
These clauses force number $1$ to be red and number $2$ to be blue. In
general, if $\mathcal{E}$ is a linear homogeneous equation in three variables
and we have a solution $(x,y,z)$ where two of $x,y,$ and $z$ are equal to each
other, then we can add clauses that force the two equal variables to be the
first color and the remaining variable to be the second color. For Rado
numbers $R_{k}(\mathcal{E})$ with $k>3$, we can also add clauses that break
the symmetries on the other colors (see [15]).

Generating a larger set of symmetry breaking clauses with more sophisticated
preprocessing is more difficult and requires far more time than normal file
generation. We included only a simple preprocessing step in our solving
process. The benefit of this preprocessing becomes more apparent when the
number of integers to color or the number of colors grows. Without symmetry
breaking, Satch takes nearly 15 minutes to determine that $F^{4}_{45}(x+y=z)$
is unsatisfiable, but only a few seconds after adding symmetry breaking
clauses.

###  5.3 SAT Solvers

Most of the SAT solving computations were done with the solver Satch v0.4.17,
developed by Biere [5]. We initially used Satch because it is remarkably fast
at proving upper bounds for many 3-color Rado numbers and relatively easy to
use. For example, Satch is able to prove the upper bounds for the values in
the first column and last row of Table 1 in under 10 seconds for each
equation. Later, as we moved towards larger CNF files and more colors, Satch
started to struggle.

In order to take advantage of the computation hardware that we had, we also
experimented with the multithreaded SAT solver Glucose [3]. In general, Satch
performed better on smaller instances, but Glucose solved larger instances up
to two times as quickly.

###  5.4 Binary Search

In order to compute the exact value of a Rado number $R_{k}(\mathcal{E})$, we
often must determine the satisfiability of $F_{n}^{k}(\mathcal{E})$ for many
values of $n$. A convenient property of the formulas $F_{n}^{k}(\mathcal{E})$
is that if $m<n$, then we can obtain the formula $F_{m}^{k}(\mathcal{E})$
simply by deleting all the clauses that contain variables $v_{j}^{i}$ with
$j>m$. Therefore, once we have a formula $F_{u}^{k}(\mathcal{E})$ that is
unsatisfiable, we have an upper bound $R_{k}(\mathcal{E})\leq u$, and we no
longer need to do any solution (negative clause) generation. After obtaining a
lower bound $R_{k}(\mathcal{E})>\ell$ with a satisfiable formula
$F_{\ell}^{k}(\mathcal{E})$, we can compute the exact value of the Rado number
$R_{k}(\mathcal{E})$ using binary search to jump between $\ell$ and $u$. Our
initial guesses for suitable bounds on $R_{k}(\mathcal{E})$ were made largely
through trial and error. However, even with the poor estimates $10\leq
R_{3}(x-y=bz)\leq 5000$ for $1\leq b\leq 15$, it is possible to compute the
exact values for all of these numbers in under two hours.

##  6 Acknowledgements

This project was supported by National Science Foundation grant DMS-1818969.

## References

  * [1] T. Ahmed and D. J. Schaal.  On generalized Schur numbers.  Exp. Math., 25(2):213–218, 2016.
  * [2] B. Alexeev and J. Tsimerman.  Equations resolving a conjecture of Rado on partition regularity.  J. Combin. Theory Ser. A, 117(7):1008–1010, 2010.
  * [3] G. Audemard and L. Simon.  Predicting learnt clauses quality in modern sat solvers.  Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09), 2009.
  * [4] A. Beutelspacher and W. Brestovansky.  Generalized Schur numbers.  In Combinatorial theory (Schloss Rauischholzhausen, 1982), volume 969 of Lecture Notes in Math., pages 30–38. Springer, Berlin-New York, 1982.
  * [5] A. Biere.  SAT Solver SATCH (version 0.4.17).  https://github.com/arminbiere/satch, 2021.
  * [6] A. Biere, K. Fazekas, M. Fleury, and M. Heisinger.  CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020.  In T. Balyo, N. Froleyks, M. Heule, M. Iser, M. Järvisalo, and M. Suda, editors, Proc. of SAT Competition 2020 – Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51–53. University of Helsinki, 2020.
  * [7] A. Biere, M. Heule, H. van Maaren, and T. Walsh.  Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications.  IOS Press, NLD, 2009.
  * [8] L. Boza, J. M. Marín, M. P. Revuelta, and M. I. Sanz.  3-color Schur numbers.  Discrete Appl. Math., 263:59–68, 2019.
  * [9] Y. Chang, J. A. D. Loera, and W. J. Wesley.  Ramsey research software.  https://github.com/itis2010me/Ramsey_Research, 2021.
  * [10] J. Fox and D. J. Kleitman.  On Rado’s boundedness conjecture.  J. Combin. Theory Ser. A, 113(1):84–100, 2006.
  * [11] N. Golowich.  Resolving a conjecture on degree of regularity of linear homogeneous equations.  Electron. J. Combin., 21(3):Paper 3.28, 8, 2014.
  * [12] R. L. Graham, B. L. Rothschild, and J. H. Spencer.  Ramsey theory.  Wiley Series in Discrete Mathematics and Optimization. John Wiley & Sons, Inc., Hoboken, NJ, 2013.
  * [13] H. Harborth and S. Maasberg.  All two-color Rado numbers for $a(x+y)=bz$.  volume 197/198, pages 397–407, 1999.  16th British Combinatorial Conference (London, 1997).
  * [14] D. Henrion, J.-B. Lasserre, and J. Löfberg.  GloptiPoly 3: moments, optimization and semidefinite programming.  Optim. Methods Softw., 24(4-5):761–779, 2009.
  * [15] M. J. H. Heule.  Schur number five.  Proceedings of AAAI-18, pages 6598–6606, 2018.
  * [16] M. J. H. Heule, O. Kullmann, and V. W. Marek.  Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer.  In Theory and applications of satisfiability testing—SAT 2016, volume 9710 of Lecture Notes in Comput. Sci., pages 228–245. Springer, [Cham], 2016.
  * [17] B. M. Landman and A. Robertson.  Ramsey theory on the integers, volume 73 of Student Mathematical Library.  American Mathematical Society, Providence, RI, second edition, 2014.
  * [18] K. Myers.  Computational advances in Rado numbers.  ProQuest LLC, Ann Arbor, MI, 2015.  Thesis (Ph.D.)–Rutgers The State University of New Jersey - New Brunswick.
  * [19] R. Rado.  Studien zur Kombinatorik.  Math. Z., 36(1):424–470, 1933.
  * [20] K. Rendall Truman and D. Schaal.  Three-color Rado numbers for $x_{1}+x_{2}+c=x_{3}$ for negative values of $c$.  In Proceedings of the Thirty-Seventh Southeastern International Conference on Combinatorics, Graph Theory and Computing, volume 183, pages 5–10, 2006.
  * [21] D. Saracino.  The 2-color Rado number of $x_{1}+x_{2}+\dots+x_{n}=y_{1}+y_{2}+\dots+y_{k}$.  Ars Combin., 129:315–321, 2016.
  * [22] D. Schaal.  A family of $3$-color Rado numbers.  In Proceedings of the Twenty-sixth Southeastern International Conference on Combinatorics, Graph Theory and Computing (Boca Raton, FL, 1995), volume 111, pages 150–160, 1995.
  * [23] D. Schaal and M. Zinter.  Two-color Rado numbers for the equations $2x_{1}+2x_{2}+c=x_{3}$ and $2x_{1}+2x_{2}+2x_{3}+c=x_{4}$.  J. Combin. Math. Combin. Comput., 95:201–214, 2015.
  * [24] I. Schur.  Über kongruenz $x^{m}+y^{m}=z^{m}\pmod{p}$.  Jahresbericht der Deutschen Mathematiker-Vereinigung, 25:114–116, 1917.

##  Appendix A Additional Rado Number calculations

In this section we give additional bounds and exact values for various Rado
numbers.

###  A.1 3-color Rado Numbers

Table 9 gives $R_{3}(ax+ay=bz)$ for $3\leq a\leq 6$, $11\leq b\leq 20$.

Table 9: $R_{3}(ax+ay=bz)$ $b$ $a$ | 3 | 4 | 5 | 6
---|---|---|---|---
11 | 2019 | 847 | 1958 | 1188
12 | $\underline{\infty}$ | 54 | 2400 | 1
13 | $\infty$ | 1710 | 3445 | 1963
14 | $\infty$ | 455 | 3675 | 336
15 | $\underline{\infty}$ | 5408 | 54 | 105
16 | $\infty$ | $\underline{\infty}$ | 5725 | 432
17 | $\infty$ | $\infty$ | 8330 | 4743
18 | $\underline{\infty}$ | $\underline{\infty}$ | 12069 | 54
19 | $\infty$ | $\infty$ | 16397 | 6726
20 | $\infty$ | $\underline{\infty}$ | $\underline{\infty}$ | 1025

###  A.2 4-color Rado Numbers

Table 10 gives some values for the 4-color Rado numbers $R_{4}(a(x-y)=bz)$.
These numbers are considerably more difficult to compute than
$R_{3}(a(x-y)=bz)$, and it took the solver CaDiCaL [6] up to 20 hours to prove
some of the upper bounds. Notably, $R_{4}(x-y=(m-2)z)=m^{4}-m^{3}-m^{2}-m-1$
for $4\leq m\leq 6$, which implies $S(4,4)=171,\ S(5,4)=469,$ and
$S(6,4)=1037$ by results in [4] and [18].

Table 10: $R_{4}(a(x-y)=bz)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5
---|---|---|---|---|---
1 | 45 | 56 | 81 | 256 | 625
2 | 171 | 45 | 103 | 56 |
3 | 469 | $>225$ | 45 |  |
4 | 1037 |  |  |  |

##  Appendix B Degree of Regularity Values

Tables 12 to 15 give the values of $dor(ax+by=cz)$ for all $a,b,c$ with $1\leq
a,b,c\leq 5$.

Table 11: $dor(ax+by=z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5
---|---|---|---|---|---
1 | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$
2 | $\infty$ | $2$ | $3$ | $2$ | $3$
3 | $\infty$ | $3$ | $2$ | $2$ | $2$
4 | $\infty$ | $2$ | $2$ | $2$ | $2$
5 | $\infty$ | $3$ | $2$ | $2$ | $2$

Table 12: $dor(ax+by=2z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5
---|---|---|---|---|---
1 | $\infty$ | $\infty$ | $3$ | $2$ | $3$
2 | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$
3 | $3$ | $\infty$ | $3$ | $2$ | $3$
4 | $2$ | $\infty$ | $2$ | $2$ | $2$
5 | $3$ | $\infty$ | $3$ | $2$ | $2$

Table 13: $dor(ax+by=3z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5
---|---|---|---|---|---
1 | $3$ | $\infty$ | $\infty$ | $3$ | $3$
2 | $\infty$ | $3$ | $\infty$ | $2$ | $3$
3 | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$
4 | $3$ | $2$ | $\infty$ | $3$ | $3$
5 | $3$ | $3$ | $\infty$ | $3$ | $3$

Table 14: $dor(ax+by=4z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5
---|---|---|---|---|---
1 | $2$ | $2$ | $\infty$ | $\infty$ | $3$
2 | $2$ | $\infty$ | $2$ | $\infty$ | $2$
3 | $\infty$ | $2$ | $3$ | $\infty$ | $3$
4 | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$
5 | $3$ | $2$ | $3$ | $\infty$ | $3$

Table 15: $dor(ax+by=5z)$ $b$ $a$ | 1 | 2 | 3 | 4 | 5
---|---|---|---|---|---
1 | $2$ | $3$ | $3$ | $\infty$ | $\infty$
2 | $3$ | $3$ | $\infty$ | $2$ | $\infty$
3 | $3$ | $\infty$ | $3$ | $3$ | $\infty$
4 | $\infty$ | $2$ | $3$ | $3$ | $\infty$
5 | $\infty$ | $\infty$ | $\infty$ | $\infty$ | $\infty$

##  Appendix C Heuristic search procedure in proof of Theorem 1.2

Here we detail the method FindPolynomials which we used to find the sets $S$
of polynomials in the proof of Theorem 1.2. We give the version of
FindPolynomials used for the equation $a(x-y)=(a-1)z$. The procedures for the
other two equations were similar, but had minor modifications.

In brief, we initialize $S$ to a set of polynomials $S_{0}$, and we use an
auxiliary set of “gaps” $G$ to add more polynomials to $S$. The procedure
BoundedIntegerPolynomial returns true if and only if all of its arguments are
polynomials $p(a)\in\mathbb{Z}[a]$ that satisfy $1\leq p(a)\leq
a^{3}+(a-1)^{2}$ for all $a\geq 16$. The FindPolynomials procedure is not
guaranteed to produce a set of clauses that yields an unsatisfiable formula,
and it took several attempts to come up with suitable choices for the initial
sets $S_{0}$ and $G_{0}$. For the equation $a(x-y)=(a-1)z$, we set
$S_{0}=\\{1,a-1,a,a+1,a^{2}-1,a^{2},a^{2}+1,a^{3},a^{3}+(a-1)^{2}\\}$,
$G_{0}=\\{1,a-1,a,(a-1)^{2},a^{2}\\}$, and maxIterations = 3. Files containing
the polynomials and clauses used in our formulas can be found in [9].

Algorithm 1 FindPolynomials($S_{0},G_{0}$,maxIterations)

$S\leftarrow S_{0}$

$G\leftarrow G_{0}$

for $i=1$ to maxIterations do

for $p,q$ in $S$ do

$r\leftarrow\frac{p-q}{a-1}$

if BoundedIntegerPolynomial($r$) then

$G\leftarrow G\cup\\{r\\}$

end if

end for

for $p\in S$, $q\in G$ do

$r_{+}\leftarrow p+(a-1)q$

if BoundedIntegerPolynomial($r_{+}$) then

$S\leftarrow S\cup\\{r_{+}\\}$

end if

$r_{-}\leftarrow p-(a-1)q$

if BoundedIntegerPolynomial($r_{-}$) then

$S\leftarrow S\cup\\{r_{-}\\}$

end if

end for

end for

$C\leftarrow\emptyset$

for $p,q\in S$ do

$x\leftarrow p$

$y\leftarrow p-(a-1)q$

$z\leftarrow aq$ $\triangleright$ Here $(x,y,z)$ is a solution to
$a(x-y)=(a-1)z.$

if BoundedIntegerPolynomial($x,y,z$) then

$S\leftarrow S\cup\\{x,y,z\\}$

$C\leftarrow C\cup\\{\\{x,y,z\\}\\}$

end if

end for

return $S,C$