Rado Numbers and SAT Computations

Rado Numbers and SAT Computations

1 Introduction

2 SAT Solving and Encoding

3 Degree of regularity coloring lemmas

4 Two parameter 3-color Rado numbers

5 Rado CNF file generation

6 Acknowledgements

References

Appendix A Additional Rado Number calculations

Appendix B Degree of Regularity Values

Appendix C Heuristic search procedure in proof of Theorem 1.2

1 Introduction

2 SAT Solving and Encoding

3 Degree of regularity coloring lemmas

4 Two parameter 3-color Rado numbers

5 Rado CNF file generation

6 Acknowledgements

References

Appendix A Additional Rado Number calculations

Appendix B Degree of Regularity Values

Appendix C Heuristic search procedure in proof of Theorem 1.2

2.1 Background on Satisfiability

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

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

4.3 Proofs of Main Results

5.1 Generating CNF Files

5.2 Symmetry Breaking

5.3 SAT Solvers

5.4 Binary Search

A.1 3-color Rado Numbers

A.2 4-color Rado Numbers

2.1 Background on Satisfiability

4.1 Rado Numbers R3​(a​(x−y)=b​z)R_{3}(a(x-y)=bz)

4.2 3-regularity of a​(x+y)=b​za(x+y)=bz

4.3 Proofs of Main Results

5.1 Generating CNF Files

5.2 Symmetry Breaking

5.3 SAT Solvers

5.4 Binary Search

A.1 3-color Rado Numbers

A.2 4-color Rado Numbers

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

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

2.1.1 Encoding of the Problem

5.1.1 Generating all solutions

5.1.2 Writing Clauses to File

2.1.1 Encoding of the Problem

5.1.1 Generating all solutions

5.1.2 Writing Clauses to File

Conjecture 1.1 (Myers).

Theorem 1.2.

Corollary 1.2.1.

Theorem 1.3.

Theorem 1.4 (Rado).

Theorem 1.5 (Rado).

Conjecture 1.6 (Rado’s Boundedness Conjecture).

Theorem 1.7.

Conjecture 1.8.

Theorem 1.9.

Corollary 1.9.1.

Example 2.1.

Lemma 3.1.

Proof.

Lemma 3.2.

Example 3.3.

Lemma 3.4.

Proof.

Lemma 3.5.

Proof.

Lemma 3.6.

Proof.

Lemma 4.1.

Proof.

Lemma 4.2.

Proof.

Theorem 4.3 (Rado).

Lemma 4.4.

Proof.

Lemma 4.5.

Proof of Theorem 1.2.

Proof of Theorem 1.3.

Proof of Theorem 1.7.

Proof of Theorem 1.9 and Corollary 1.9.1.

Example 5.1.

Conjecture 1.1 (Myers).

Theorem 1.2.

Corollary 1.2.1.

Theorem 1.3.

Theorem 1.4 (Rado).

Theorem 1.5 (Rado).

Conjecture 1.6 (Rado’s Boundedness Conjecture).

Theorem 1.7.

Conjecture 1.8.

Theorem 1.9.

Corollary 1.9.1.

Example 2.1.

Lemma 3.1.

Proof.

Lemma 3.2.

Example 3.3.

Lemma 3.4.

Proof.

Lemma 3.5.

Proof.

Lemma 3.6.

Proof.

Lemma 4.1.

Proof.

Lemma 4.2.

Proof.

Theorem 4.3 (Rado).

Lemma 4.4.

Proof.

Lemma 4.5.

Proof of Theorem 1.2.

Proof of Theorem 1.3.

Proof of Theorem 1.7.

Proof of Theorem 1.9 and Corollary 1.9.1.

Example 5.1.

\AtBeginShipoutNext\AtBeginShipoutDiscard

Yuan Chang Department of Mathematics, University of California, Davis
1 Shields Ave
Davis, CA 95616 Jesús A. De Loera [email protected] Department of Mathematics, University of California, Davis
1 Shields Ave
Davis, CA 95616 William J. Wesley [email protected] Department of Mathematics, University of California, Davis
1 Shields Ave
Davis, CA 95616

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].

$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.

The values of the following Rado numbers are known:

1.

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

$R_{3}(a(x-y)=(a-1)z)=a^{3}+(a-1)^{2}$ for $a\geq 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.

$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.

The values of the following Rado numbers are known.

1.

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

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

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

$R_{4}(x-y=az)$ for $1\leq a\leq 4$ .
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)

	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)

	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].

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.

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)

	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)

	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)

Table 6:

R_{3}(ax+by=4z)

Table 7:

R_{3}(ax+by=5z)

	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)

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$ .

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].

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.

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.

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.

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].

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.

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}$ .

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.

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].

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:

(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}}$ .

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:

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.

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.

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.

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.

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$ .

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.

∎

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$ .

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. ∎

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

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.

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)$ .

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

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).$

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

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$ . ∎

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

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$ .

$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$ .

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.

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.

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.

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.

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.

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

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. ∎

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.

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}$ .

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]$ .

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.

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.

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.

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.

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.

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

[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.

In this section we give additional bounds and exact values for various 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)

	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

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)

	1	2	3	4	5
1	45	56	81	256	625
2	171	45	103	56
3	469	$>225$	45
4	1037

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)

	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)

	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)

	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)

	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)

	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$

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

S

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

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

C\leftarrow\emptyset

for

p,q\in S

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

$\underline{\infty}$