Given a linear equation ℰ of the form + = where , , are positive integers, the -colour Rado number (ℰ) is the smallest positive integer , if it exists, such that every -colouring of the positive integers {1, 2, . . . , } contains a monochromatic solution to ℰ. In this paper, we consider = 3 and the linear equations + = and + = . Using SAT solvers, we compute a number of previously unknown Rado numbers corresponding to these equations. We prove new general bounds on Rado numbers inspired by the satisfying assignments discovered by the SAT solver. Our proofs require extensive case-based analyses that are dificult to check for correctness by hand, so we automate checking the correctness of our proofs via an approach which makes use of a new tool we developed with support for operations on symbolically-defined sets-e.g., unions or intersections of sets of the form { (1), (2), . . . , ()} where is a symbolic variable and is a function possibly dependent on . No computer algebra system that we are aware of currently has suficiently capable support for symbolic sets, leading us to develop a tool supporting symbolic sets using the Python symbolic computation library SymPy coupled with the Satisfiability Modulo Theories solver Z3.
the positive integers with no monochromatic solution to ℰ (, ; 1, 2, . . . , ). Surprisingly, not much
is known about the properties of Rado numbers for = 3. In 1995, Schaal [
• 3(ℰ (3, 0; , −, )) for 1 ≤ , ≤ 15, • 3(ℰ (3, 0; , , )) for 1 ≤ , ≤ 10, • 3(ℰ (3, 0; , , )) for 1 ≤ , , ≤ 6, as well as the following theorem.
Theorem 1.2. 3(ℰ (3, 0; 1, 1, )) = ∞ for ≥ 4 and 3(ℰ (3, 0; , , 1)) = ∞ for ≥ 2.
In this paper, we have investigated values and bounds of Rado numbers for the equations ℰ (3, 0; , , )
and ℰ (3, 0; , , ). We have computed a number of previously unknown exact values using SAT solvers,
extending the results presented by Chang, De Loera, and Wesley [
Note that we may assume that and are coprime, since if and share a common factor we may divide the coeficients of the equation ℰ by without changing its solutions, e.g., 3(ℰ (3, 0; , , )) = 3(ℰ (3, 0; /, /, /)). Guided by the satisfying assignments generated by the SAT solver in the process of computing these values, we proved the following two theorems.
Theorem 1.3. For coprime positive integers , with > ≥ 3 and 2 + + > 2 + , Theorem 1.4. For odd integers ≥ 7, 3(ℰ (3, 0; , , )) ≥ 3 + 2 + (2 + 1) + 1.
3(ℰ (3, 0; , , + 1)) ≥ 3( + 1).
Based on the computational data we generated and the above lower bounds, we propose the following conjectures.
Conjecture 1.1. For coprime positive integers , with > ≥ 3 and 2 + + > 2 + , 3(ℰ (3, 0; , , )) = 3 + 2 + (2 + 1) + 1.
Conjecture 1.2. For coprime positive integers , , with odd, if 3 ≤ < ≤ 2 − 1 then 3(ℰ (3, 0; , , )) = 3.
The proofs of Theorems 1.3 and 1.4 are automatically verified using a symbolic analyzer we developed in Python called AutoCase.1 The motivation has been to avoid errors in the intricate case-based analysis which is often routine and repetitive. For example, in order to verify Theorem 1.4, AutoCase takes as input three symbolically-defined subsets , , of the integers [1, 3( + 1) − 1] (where ≥ 7 is a symbolic odd integer). AutoCase verifies that the union of , , and is the set [1, 3( + 1) − 1] and that , , are mutually disjoint—thereby confirming that , , form a 3-colouring of the positive
integers less than 3( + 1). Finally, AutoCase confirms that there are no monochromatic solutions of the equation + = ( + 1), i.e., the set ⋃︀+=(+1){(, , )} is disjoint with 3, 3, and 3. We stress that the sets defining the colouring are defined symbolically, e.g., ⋃︀,,{ (, , )} where is a function (possibly depending on ), the upper and lower bounds on the indices , , may depend on , and the elements of the set may be filtered by divisibility predicates such as specifying that all elements are divisible by .
Although it would be easy to perform the necessary set operations in a typical computer algebra
system like Maple, Mathematica, and SageMath if was a known fixed integer, in our application is
a symbolic variable, and we are aware of no computer algebra system supporting the operations on
symbolic sets we require in this paper. Maple and Mathematica seem to lack the ability to even express
the set [1, ] when is symbolic. SageMath does have support for a “ConditionSet” allowing sets like
[1, ] to be formulated, but the operations supported by ConditionSets was too limited for our purposes.
In AutoCase, operations on symbolic sets are performed by employing a combination of the Python
symbolic computation library SymPy [
Our work therefore fits into the “SC-Square” paradigm of combining satisfiability checking with
symbolic computation [
One of the key challenges in Ramsey theory on the integers is the scarcity of data, as generating
individual data points is an exceptionally dificult task. However, modern computational tools, including
SAT solvers, have alleviated some of these computational challenges. During the last two decades,
SAT solvers have been employed to compute Ramsey-type numbers at diferent scales and capacities.
Some examples are the computation of the values and bounds of van der Waerden numbers (Kouril and
Paul [
Recently, Chang, De Loera, and Wesley [
A literal is a Boolean variable (say ) or its negation (denoted̄ ). A clause is a logical disjunction of literals. A formula is in Conjunctive Normal Form (CNF) if it is a logical conjunction of clauses.
A truth assignment is a mapping of each variable in its domain to true or false. A truth assignment satisfies a clause if it maps at least one of its literals to true and the assignment satisfies a formula if it satisfies each of its clauses. A formula is called satisfiable if it is satisfied by at least one truth assignment and otherwise it is called unsatisfiable. The problem of recognizing satisfiable formulas is known as the satisfiability problem, or SAT for short.
Given positive integers and and a linear equation ℰ , we now construct a formula in conjunctive normal form that is satisfiable if and only if there exists a -colouring of [1, ] avoiding monochromatic solutions of ℰ . Therefore, if our formula is satisfiable then (ℰ ) > and if our formula is unsatisfiable then (ℰ ) ≤ .
Variables: Variables are denoted by , for 0 ≤ ≤ − 1 and 1 ≤ ≤ , such that , is true if and only if colour is assigned to integer . There are variables in the formula.
At least one colour is assigned to every integer: For each integer ∈ [1, ], the clause ensures at least one colour ∈ [0, − 1] is assigned to .
At most one colour is assigned to every integer: For each integer ∈ [1, ], the clauses (0, ∨ 1, ∨ · · · ∨ −1, )
⋀︁ 0≤ 1<2≤−1
(̄ 1, ∨̄ 2, ) ensure at most one colour ∈ [0, − 1] is assigned to .
There is no monochromatic solution to ℰ : For each colour ∈ [0, − 1] and for each solution (1, 2, . . . , ) to ℰ , the clause (̄ ,1 ∨̄ ,2 ∨ · · · ∨̄ , ) ensures the solution (1, 2, . . . , ) is not monochromatic in colour . Let ℰ, denote the set of all solutions (1, 2, . . . , ) in [1, ] that satisfy the equation ℰ . There will be · | ℰ,| such clauses. We may compute |ℰ,| by summing over all possible values of (1, 2, . . . , −1 ) in the range [1, ] via |ℰ,| = ∑︁ ∑︁ · · · 1=1 2=1
∑︁ −1 =1 [︃ ∑︀−1 ]︃ =1 ∈ [1, ] , where summand uses Iverson bracket notation to ensure that the remaining variable (determined by the equation) falls within [1, ]. This gives |ℰ,| ≤ −1 , since [·] ≤ 1.
Breaking permutation symmetry of colours: So far, no distinction has been made amongst the colours. This artificially increases the size of the search space by a factor of !, the number of permutations on colours. To avoid having the SAT solver explore all 3! colour permutations on {0, 1, 2} during solving, we ensure that colours are introduced in ascending order, i.e., colour 0 appears before colour 1 and colour 1 appears before colour 2. To ensure that colour 0 appears in the first position, we add the unit clause 0,1. To ensure that colour 1 appears before colour 2, we add the clause (⋁︀=−11̄ 0,) ∨̄ 2, for = 2, . . . , 1(ℰ ). These say that colour 2 cannot immediately follow an initial colouring consisting only of colour 0s, and thus the first colour other than 0 must be 1. One can work out the exact value of 1(ℰ ) by hand for the cases we consider in this paper, as in the following lemma whose proof we provide in appendix A.
Lemma 2.1. If and are positive coprime integers then 1(ℰ (3, 0; , , )) = max( + 1, ), 1(ℰ (3, 0; , , 1)) = 2, and 1(ℰ (3, 0; , , )) = max(, ⌈/2⌉) when > 1.
To eficiently generate all integer solutions (, , ) within the interval [1, ] for + = , we iterate from 1 to and construct three linear Diophantine equations = − = − = + where = , where = , where = .
The goal is to independently find solutions for each equation. • Step 1 (Solving a linear Diophantine equation). To begin, we solve one of the above equations (say + = ) for unknowns (, ) using the Extended Euclidean Algorithm, providing a particular integer solution (0, 0). The general solution is = 0 +
gcd(, ) and = 0 −
gcd(, ) , where is a parameter that runs over all integers to generate all solutions. • Step 2 (Restricting to the interval [1, ]). Since we are only interested in solutions within [1, ], we impose the constraints
1 ≤ 0 + gcd(, ) ≤ and 1 ≤ 0 −
gcd(, ) ≤ .
These inequalities provide upper and lower bounds on , ensuring that both and remain in the valid range. • Step 3 (Iterating over valid values of ). Once the feasible range for is determined, we iterate over all valid values of and solve for and at each step, adding (, , ) to our list of solutions. • Finally, we repeat these steps for the remaining two equations = − and = − .
For this work, we used the SAT solvers CaDiCaL [
Once a Rado number was determined (or suspected to be known based on the patterns we observed), we transitioned to using a non-incremental solver and generated two instances: one for − 1 , the last satisfiable instance, and one for , the first unsatisfiable instance. We generated clauses in DIMACS format, wrote them to two CNF files, and used Kissat to solve both instances. To be consistent in our timings, all instances were ultimately solved non-incrementally using Kissat. Our largest instance, the unsatisfiable instance showing 3(ℰ (3, 0; 15, 15, 8)) = 97875, contained 293,625 variables and 255,884,401 clauses and took 58.8 hours to solve.
Altogether, generating the SAT instances took around 11 hours, the total CPU time used to solve the unsatisfiable instances (i.e., the instances that prove an upper bound) was around 251 hours, and the total CPU time used on satisfiable instances (i.e., the instances that prove a lower bound) was around 53 hours. Our computations were performed on the Compute Canada cluster Cedar, utilizing Intel
2.5. Some new exact values of 3(ℰ (3, 0; , , )) We have computed 3(ℰ (3, 0; , , )) for 1 ≤ ≤ 15 and 1 ≤ ≤ 30 and given the results in Table 1. By Rado’s theorem 1.1, all elements in Table 1 are finite. Altogether, the total CPU time on unsatisfiable \ 1 14 43 94 173 286 439 638 889 1198 1571 2014 2533 3134 3823 4606 5489 6478 7579 8798 10141 11614 13223 14974 16873 18926 21139 23518 26069 28798 31711 instances was 21,790 seconds, and the total CPU time on satisfiable instances was 13,516 seconds, amounting to 9.81 total hours. A maximum of 4.3 GiB of memory was used across all instances. 2.6. Some new exact values of 3(ℰ (3, 0; , , )) By Theorem 1.2, 3(ℰ (3, 0; , , 1)) is infinite for ≥ 2 and 3(ℰ (3, 0; 1, 1, )) is infinite for ≥ 4 . √ Also, by Chang et al. [4, Lemma 3.1], 3(ℰ (3, 0; , , )) is infinite if 2 ≤ 2/ or 2 ≤ . They provided the values of 3(ℰ (3, 0; , , )) for 1 ≤ , ≤ 10 and also for 3 ≤ ≤ 6 and 11 ≤ ≤ 20 . We have extended them for 1 ≤ ≤ 15 and 1 ≤ ≤ 25 and reported these numbers in Table 2. The instances in this table proving upper bounds required a CPU time of 882,211 seconds to solve, while the instances proving lower bounds required 176,375 seconds to solve, amounting to 294.05 total hours. A maximum of 26.3 GiB of memory was used across all instances. 2.7. Some new patterns for 3(ℰ (3, 0; , , )) The data on 3(ℰ (3, 0; , , )) presented in Table 1 inspired us to make some general observations and a conjecture described below.
Observation 2.1. For coprime integers and , the data in Table 1 reveals the following. \ 1 ∞ ∞ ∞ 243 ∞ ∞ 14 384 2000 108 14 875 135 180 14 1 54 750 336 308 875 432 1 1000 54 585 1125 1125 105 1 2019 847 1958 54 2400 1710 3445 455 3675 5408 54 5725 8330 12069 16397 ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ 3072 12393 ∞ 384 243 2000 1536 8748 7500 14 8019 875 1224 14 6000 180 7290 14 1672 8019 5500 54 108 750 1456 9477 6500 308 10206 875 2760 135 54 1 11664 1000 3825 12393 8500 585 1 1125 4332 16853 9500 105 19080 1 6699 336 12579 847 25047 1958 8556 32453 17250 54 432 2400 10200 42975 105 3(ℰ (3, 0; , , )) for 1 ≤ ≤ 15 and 1 ≤ ≤ 25 . The previously unknown values are presented in boldface, and the underlined entries correspond to equations whose coeficients are not coprime.
Range of sequence and ultimately arriving at the following conjecture. 3(ℰ (3, 0; , , )) = 3 + 2 + (2 + 1) + 1.
Conjecture 2.1. For coprime positive integers and with 2 + + > 2 + and > ≥ 3 ,
Before proceeding, we note the equation ℰ (3, 0; , −, ) can be transformed into ℰ (3, 0; , , )
by permuting variables. This equivalence along with a theorem of Chang, De Loera, and Wesley [
Proposition 2.1. 3(ℰ (3, 0; , 1, 1)) = 3 + 52 + 7 + 1 for ≥ 1. for ≥ 3 , 3(ℰ (3, 0; 1, −1, − 2)) = 3 − 2 − − 1 3(ℰ (3, 0; 1, −1, )) = 3 + 52 + 7 + 1. Hence, 3(ℰ (3, 0; , 1, 1)) = 3 + 52 + 7 + 1. Proof. By permuting variables we have 3(ℰ (3, 0; , 1, 1)) = 3(ℰ (3, 0; 1, −1, )) . By [4, Thm 1.2], . Replacing with − 2 , we get for ≥ 1 , 2.8. Some new patterns for 3(ℰ (3, 0; , , )) The data on 3(ℰ (3, 0; , , )) presented in Table 2 has inspired the following conjecture and some general observations described below.
Conjecture 2.2. For coprime positive integers and , if is odd, then for 3 ≤ < ≤ 2 − 1 3(ℰ (3, 0; , , )) = 3. , Observation 2.2. For odd positive integers 7 ≤ ≤ 15, we have • 3(ℰ (3, 0; , , − 1)) = 3(ℰ (3, 0; , , + 2)) = 3( + 2); • if gcd(, + 3) = 1, then 3(ℰ (3, 0; , , − 2)) = 3(ℰ (3, 0; , , + 3)) = 3( + 3); • 3(ℰ (3, 0; , , +21 )) = 3(ℰ (3, 0; , , 2 − 1)) = 3(2 − 1); • if gcd(, +23 ) = 1, then 3(ℰ (3, 0; , , +23 )) = 3(ℰ (3, 0; , , 2 − 4)) = 3(2 − 4). Observation 2.3. For coprime positive integers and , 3(ℰ (3, 0; , , )) = {︃3/2 if ∈ {6, 10, 14} and < ≤ 2 − 1,
3/4 if ∈ {12} and < ≤ 2 − 1.
A general characterization of the cases with even is not possible at the moment due to lack of further data.
In Section 2, we extended the known numerical values of Rado numbers corresponding to the equations ℰ (3, 0; , , ) and ℰ (3, 0; , , ) and observed several new bounds for these numbers. In this section, we discuss and prove some of those bounds using AutoCase. An overview of how AutoCase works is first provided in Section 3.1, and then as a demonstrative example we use AutoCase to prove Proposition 2.1 in Section 3.2. Finally, we use AutoCase to prove Theorems 1.3 and 1.4 in Sections 3.3 and 3.4.
Shallit [
The input provided to AutoCase is the linear equation to be considered along with a colouring of the integers [1, ] specified by a collection of symbolic sets as described in Section 3.1.1. AutoCase verifies that the colouring is valid by ensuring the size of the symbolic sets sum to exactly (see Section 3.1.2) and that the sets are pairwise disjoint (see Section 3.1.3). This verifies the provided symbolic sets provide a partition of [1, ]. Finally, AutoCase verifies that there are no solutions of the linear equation under consideration where all variables are from symbolic sets of the same colour (see Section 3.1.4). Thus, the symbolic sets define a colouring of the integers [1, ] that have no monochromatic solutions to the linear equation, thereby proving a lower bound of + 1 on the Rado number for that linear equation. 3.1.1. Input specification The input to our automated system consists of: • A symbolic linear equation ℰ , such as + = ( + 1), where coeficients and assumptions on the coeficients (e.g., ≥ 7, odd) are symbolic. • A symbolic corresponding to the lower bound on (ℰ ), e.g., = 3( + 1) − 1. • A partition of the domain [1, ] into named symbolic sets, each specified by – symbolic bounds (e.g., [, 4 + 3 − ]), – a format expression generating integers in the set (e.g., ( + 1) + + ), and – optional divisibility filters (e.g., integers in the set must be divisible by 2 but not 3). • A -colouring of [1, ] defined in terms of the above symbolic sets.
These inputs are defined using SymPy to facilitate symbolically: • Building and manipulating (e.g., simplifying, expanding, combining, substituting symbolically) interval bounds, format expressions, and divisibility properties. • Calculating size, disjointness, and covering conditions. The union ⋃︀ of [1, ] if and only if ⋃︀
=1 has size , the sets are pairwise disjoint, and ⋃︀ • Simplifying and structurally transforming constraints before they are fed to Z3. =1 is considered a partition =1 ⊆ [1, ]. 3.1.2. Symbolic size computation using SymPy SymPy plays a central role in enabling symbolic reasoning, algebraic manipulation, and structured enumeration in the symbolic size analysis pipeline. The key uses of SymPy can be itemized as follows: • Size with divisibility filters: Let the underlying interval be defined as [, ]. Let and ND denote the sets of required and excluded divisors, respectively, and consider For ⊆ ND , define = { ∈ [, ] : ∀ ∈ , | and ∀ ∈ ND , ∤ } .
= { ∈ [, ] : lcm( ∪ ) | } .
The number of elements ∈ [, ] divisible by all divisors in and none in ND is || = ∑︁ (−1) | || | =
∑︁ (−1) | | ⊆ND ⊆ND ︂(⌊
lcm( ∪ ) − ︂⌋ ︂⌊
− 1 lcm( ∪ ) ︂⌋) .
ND = {2}. Then the size of the resulting set is This formula uses inclusion-exclusion to subtract overlapping exclusions in order to count elements satisfying the divisibility constraints. SymPy contributes with floor, ceiling, and lcm to enforce and combine arithmetic conditions. For example, consider the interval [1, 2] with = {} and ︂⌊
2 ⌋︂ lcm() − ︂⌊
2 lcm(, 2) ︂⌋ = ︂⌊ 2 ⌋︂ − ︂⌊ 2 ⌋︂ 2 = − = ( − 1). • Format-based symbolic summation: Consider a symbolic set defined by a format expression = (1, 2, . . . , ) where ∈ [ , ℎ ]. When is injective, the total size of the set is given by |{ = (1, . . . , ) | ≤ ≤ ℎ }| = ℎ1 ∑︁ ∑︁
ℎ2 1=1 2=2 · · · ℎ ∑︁ 1. = denominator polynomials. algebraic rules. For example, ∑︀
∑︀ =0
=1 1 = ( + 1)/2.
For example, the format expression = + where 0 ≤ < and 1 ≤ ≤ . If some variables are symbolic (e.g., ), the size remains symbolic and can be simplified using defines a set of size • Symbolic floor simplification: Let
be a symbolic variable representing a positive integer, and consider the rational expression () = ()/(), where and are polynomials in . We aim to simplify ⌊()/()⌋ which can often be simplified using the degrees of the numerator and Consider deg() < deg(). When the degree of the numerator () is strictly less than that of the denominator (), the value of the rational expression ()/() has magnitude less than 1 for all suficiently large , and is dominated by the leading terms of and . Its sign for large enough is therefore determined by the sign of LC()/ LC() where LC(·) denotes the leading coeficient, so ︂⌊ () ⌋︂ () = {︃0
if LC()/LC() > 0, −1 if LC()/LC() < 0, assuming that the bound on is large enough for this simplification to occur. For example, ⌊−1/⌋ = −1 if ≥ 1 , ⌊1/⌋ = 0, ⌊( + 1)/⌋ = 1, and ⌊︀ (2 + 1)/3⌋︀ = 0 if ≥ 2 , and ⌊︀ −( + 5)/ 2⌋︀ = −1 if ≥ 3. • Unified symbolic simplification: Applies simplify and expand to normalize symbolic size expressions such as converting 2( + 1) + (2 + 3 + 1) + 4 to 3 + 52 + 7. 3.1.3. Symbolic disjointness checking using SymPy and Z3 AutoCase constructs a symbolic system of constraints to determine whether two symbolic sets are disjoint. The key idea is to introduce a symbolic integer variable that hypothetically belongs to both sets. Then, disjointness reduces to checking whether the conjunction of the constraints defining both sets is unsatisfiable. Z3 is used to test satisfiability. • Domain constraints (bounds): For each interval, we require ∈ [lower, upper], encoded via Ge(z, lower) and Le(z, upper). If sets and are defined over [1, 2 + 2] and [2 + 3 + 1, 3 + 52 + 7], respectively, then ≥ 1 ∧ ≤
2 + 2 and ≥ 2 + 3 + 1 ∧ ≤ 3 + 52 + 7.
• Divisibility and non-divisibility constraints: Divisibility constraints are encoded as | using Mod(, ) == 0, and non-divisibility as ∤ using Mod(, ) ̸= 0. Suppose set contains all ∈ [1, ] such that | , while set contains those where ∤ . The constraint system ≡ 0 mod ∧ ̸≡ 0 mod is unsatisfiable, so the sets are disjoint. • Format expression constraints: To avoid symbol collisions in format expressions, all format variables are renamed using fresh symbols (e.g., _fmt_i). If a set is defined by a format expression = (1, . . . , ), then we add sp.Eq(z, format_expr) along with symbolic bounds on the variables (e.g., 0 ≤ < 2).
For instance, consider the set defined by = ( + 1) + + where 0 ≤ < 2, and 2⌊/2⌋ + 1 ≤ ≤ − 1, with constraint ̸≡ 0 (mod ). Also, let the set be defined by = (3 + 2),
1 ≤ ≤ ⌊( − 1)/2⌋.
Now, assume ∈ ∩ . Then ∈ implies ≡ 0 (mod ) , and this contradicts the constraint from . Therefore, ∩ = ∅. 3.1.4. Monochromatic solution analysis using Z3 For a linear equation ∑︀=−11 = and ≥ 1 sets (each given a colour class), the tool now generates all possible ways to assign the − 1 left-hand-side (LHS) variables across sets using Cartesian products. AutoCase iterates over every way to assign the LHS variables to the same colour class and for every colour class it generates a list of cases for verification.
The prover systematically explores all combinations of sets assigned to the variables in the equation, where each variable is taken from the same colour class. For each such case, it verifies that no solution exists satisfying the equation under the imposed divisibility, format, and value constraints. If all such cases succeed this confirms the absence of monochromatic solutions. • For each assignment of sets to the variables in the equation, the tool aggregates all associated symbolic constraints: interval bounds (e.g., ∈ [1, 3]), format constraints (e.g., = 2 + ), and arithmetic iflters (e.g., ∤ , | 2). • It then encodes the target equation (e.g., + = ( + 1)) and all constraints into an SMT expression, along with assumptions (e.g., ≥ 7 , prime(), gcd(, ) = 1). The translation process supports a broad range of symbolic constructs in SymPy, including integer inequalities, polynomial equalities, floor and ceiling operations, divisibility conditions, and logical connectives. • The solver checks that the symbolic system is unsatisfiable. The contradiction analysis is exhaustive—it verifies that under all parameter values satisfying the assumptions, the given assignment cannot yield a valid solution.
If every such assignment leads to a contradiction, the tool concludes that the equation has no monochromatic solution in the constructed colouring, and thus the lower bound for the Rado number is symbolically proven.
Example 3.1. We illustrate a symbolic case analyzed by AutoCase, where each variable in the equation 1 + 2 = ( + 1)3 is assigned to distinct symbolic intervals with bounds, divisibility filters, and format expressions. The analyzer constructs the following constraint system: • Global Assumptions: ∈ Z and ≥ 1 • Equation Constraint: 1 + 2 = ( + 1)3 • Bounds: 1, 2, 3 ∈ [1, 2] ⇒ ≥ 1, ≤ 2 for ∈ {1, 2, 3} • Divisibility Filter on 1: | 1 ⇒ 1 = · 1, 1 > 0 • Non-divisibility Filter on 2: 2 ∤ 2 ⇒ 2 ̸= 2 · 2 for all 2 > 0 • Format Expression for 3:
3 = ( + 1) + + with 0 ≤ < 2, 0 ≤ ≤ , and 2⌊/2⌋ + 1 ≤ ≤ − 1 • Total Constraint Set (passed to Z3): 1 + 2 = ( + 1)3 1 = · 1, 1 > 0 ∀2 > 0, 2 ̸= 2 · 2 3 = ( + 1) + + 0 ≤ < 2, 1, 2, 3 ∈ [1, 2] The set of constraints in Z3 are given in Appendix D. If Z3 determines that this system is unsatisfiable for all admissible values of , then this configuration leads to a contradiction—contributing to the overall proof that the equation has no monochromatic solution in the constructed colouring.
A general technique to prove a lower bound is to construct a colouring avoiding forbidden patterns.
Specifically, to show (ℰ ) ≥ + 1 , constructing a -colouring of the positive integers [1, ]
avoiding any monochromatic solution to equation ℰ would be suficient. As an example, Proposition 2.1
states 3(ℰ (3, 0; , 1, 1)) = 3 + 52 + 7 + 1. Although we already showed this proposition is a
consequence of a theorem of Chang, De Loera, and Wesley [
Consider the partition of [1, 3 + 52 + 7] using the intervals
From these, we define the colouring function : [1,
3 + 52 + 7] → [
– 6 = [3 + 52 + 6 + 1, 3 + 52 + 7]: Again, is far smaller than min(6), so ∈/ 6. Since is forced outside the monochromatic partitions, we conclude that no monochromatic solution exists in colour 0 when ∈ 0 and ∈ 0.
The same type of analysis applies to all other colour cases, ensuring that the generated constraints exhaustively eliminate any monochromatic solution. As a result, AutoCase has shown that 3(ℰ (3, 0; , 1, 1)) ≥ 3 + 52 + 7 + 1 for all ≥ 1. 3.3. Proof of Theorem 1.3 (lower bound for 3(ℰ (3, 0; , , ))) 3.3.1. Construction of the partition Since gcd(, ) = 1, the variable to be an integer in the equation + = , the variable must be a multiple of . Consider the partition of [1, 3 + 2 + (2 + 1)] using the intervals 0 = [1, ], 1 = [ + 1, 2], 2 = [2 + 1, 2 + ], 3 = [2 + + 1, 3 + 2 + ( + 1)], and 4 = [3 + 2 + ( + 1) + 1, 3 + 2 + (2 + 1)].
Note that indeed [1, 3 + 2 + (2 + 1)] = 0 ∪ 1 ∪ 2 ∪ 3 ∪ 4 and ∩ = ∅ for ̸= . Define the following sets to filter the above intervals for colouring in Dark Gray (0), Red (1), and Blue (2): 1 = { ∈ 0 : ̸≡ 0
(mod )} 2 = {︀ ∈ 0 ∪ 1 : ≡ 0
(mod 2)}︀
Now, consider the colouring : [1, 3 + 2 + (2 + 1)] → [
Example 3.3. Below is the colouring of [
3( + 1) of length 3( + 1) − 1 Observation 3.1. For odd positive integers ≥ 7 , there exists a certificate (computed using a SAT solver) where certain repetitive patterns appear as blocks of coloured integers of size ( + 1). Consider the following examples for 3(ℰ (3, 0; 7, 7, 8)).
Colour block 1 for 3(ℰ(3, 0; 7, 7, 8))
Colour-block 2 for 3(ℰ(3, 0; 7, 7, 8)) r1 r8 b15 b22 b29 b36 b43 b50 r2 r9 b16 b23 b30 b37 b44 b51 r338 r345 b352 b359 b366 b373 b380 b387 r337 r344 b351 b358 b365 b372 b379 b386 r3 r10 r17 r24 b31 b38 b45 b52 r339 r346 r353 r360 b367 b374 b381 b388 r4 r11 r18 r25 b32 b39 b46 b53 r340 r347 r354 r361 b368 b375 b382 b389 r5 r12 r19 r26 r33 r40 b47 b54 r341 r348 r355 r362 r369 r376 b383 b390 r6 r13 r20 r27 r34 r41 b48 b55 r342 r349 r356 r363 r370 r377 b384 b391 7 14 21 28 35 42 r49 56 b343 350 357 364 371 378 385 r392 r57 r64 b71 b78 b85 b92 b99 b106 r58 r65 b72 b79 b86 b93 b100 b107 r2690 r2697 b2704 b2711 b2718 b2725 b2732 b2739 r2689 r2696 b2703 b2710 b2717 b2724 b2731 b2738 r59 r66 r73 r80 b87 b94 b101 b108 r2691 r2698 r2705 r2712 b2719 b2726 b2733 b2740 r60 r67 r74 r81 b88 b95 b102 b109 r2692 r2699 r2706 r2713 b2720 b2727 b2734 b2741 r61 r68 r75 r82 r89 r96 b103 b110 r2693 r2700 r2707 r2714 r2721 r2728 b2735 b2742 r62 r69 r76 r83 r90 r97 b104 b111 r2694 r2701 r2708 r2715 r2722 r2729 b2736 b2743 63 70 77 84 91 r98 105 112 b2695 2702 2709 2716 2723 2730 2737 Colour-block 7 for 3(ℰ(3, 0; 7, 7, 8))
Colour-block 49 for 3(ℰ(3, 0; 7, 7, 8)) The integers that are not divisible by get coloured in a consistent way in each block, while the integers that are divisible by need to be carefully coloured in such a way (a diferent way in each block) to avoid monochromatic solutions to the equation + = ( + 1). 3.4.1. Construction of the partition with ≥ 7 being an odd positive integer. Consider, Before we prove the lower bound, we construct a partition of the set [1, ] where = 3( + 1) − 1 [1, + 1] = {︀ · ( + 1) + · + : 0 ≤ ≤ 2 − 1, 0 ≤ ≤ , 1 ≤ ≤ partition [1, ] = ( ) ∪ ( ) with Let ( ) and ( ) denote { ∈ [1, ] : | } and { ∈ [1, ] : ∤ }, respectively. We have the ( ) = {︀ · ( + 1) + · + : 0 ≤ ≤ ( ) = {︀ · ( + 1) + · + : 0 ≤ ≤ 2 − 1, 0 ≤ ≤ 2 − 1, 0 ≤ ≤ , 1 ≤ ≤ − 1 ︀} ∖ { + 1} , and Let ( ) = ℓ ∪ ℓ be a partition defined by 1 − =1 1 − =0 1 − =1 = ⋃︁ {︀ 4 + 2}︀ ∪ ⋃︁ {︀ 3 + 2 : 0 ≤ ≤ − 1 ︀{ 3 + 2}︀ , and = {︀ 4}︀ ∪ ⋃︁ {︀ 3 + 2 : + 1 ≤ ≤ − 1 ︀} ∪ ︀} .
︀} ︀} . ︀} .
︀} , and ︀}
∪ (−1)/2 ⋃︁ =1 1 − ⋃︁ =(+1)/2 ︀{ 3 + 2}︀ . ℓ = {︀ · ( + 1) + · + : 0 ≤ ≤ ℓ = {︀ · ( + 1) + · + : 0 ≤ ≤ 2 − 1, 0 ≤ ≤ , 2⌊/2⌋ + 1 ≤ ≤ − 1 2 − 1, 0 ≤ ≤ , 1 ≤ ≤ 2⌊/2⌋
Let 2 ( ) = ∪ be a partition defined by 2 ( ) = {︀ · ( + 1) + · + : 0 ≤ ≤ 2 − 1, 0 ≤ ≤ , | ( + + 1) ∖ { + 1} .
Our colouring : [1, ] → [
1 if ∈ ℓ ∪ , ⎪ ⎪⎩0 if ∈ ( ) ∖ 2 ( ).
Proof of Theorem 1.4. A written proof of Theorem 1.4 is provided in Appendix C. The symbolic correctness of the partition and the verification of the cases can be found in the AutoCase repository.
In this work, we explored the computation of 3-colour Rado numbers for certain 3-term linear equations. Our SAT-based approach enabled us to extend the known values of 3(ℰ (3, 0; , , )) and 3(ℰ (3, 0; , , )), computing previously unknown Rado numbers and formulating new conjectures based on observed patterns. We proved the lower bounds 3(ℰ (3, 0; , , )) ≥ 3 + 2 + (2 + 1) + 1 and 3(ℰ (3, 0; , , + 1)) ≥ 3( + 1) for certain ranges of and . The case-based proofs were automatically verified using a combination of symbolic computation and SMT solvers in a tool we call
We did not attempt to compute Rado numbers involving more than three colours due to the rapid growth in the SAT instances, and for simplicity we focused on linear equations with a constant term of zero. In principle, our methods should be applicable to nonhomogeneous linear equations and to Rado numbers involving four or more colours, though they may require more computational resources or more advanced combinatorial optimization techniques. We leave such cases for future work.
In this section we assume and are positive coprime integers. Lemma 2.1 then says {︃2
if = 1, max(, ⌈/2⌉) if > 1.
(1) 1(ℰ (3, 0; , , )) = max( + 1, ) and 1(ℰ (3, 0; , , )) =
For the first equation of (1), we want to find the solution (, , ) of + = that minimizes max(, , ); then 1(ℰ (3, 0; , , )) = max(, , ). Since and are coprime, must be divisible by , so (, 1, + 1) is the solution of + = with smallest possible and values. Since = ( + )/, the solution with the smallest possible and will also minimize . Thus, the smallest possible value of max(, , ) is max(, 1, + 1) = max( + 1, ).
For the second equation of (1), we want to find the solution (, , ) of + = that minimizes max(, , ); then 1(ℰ (3, 0; , , )) = max(, , ). Since and are coprime, must be divisible by , so say = , giving + = . Then max(, , ) is minimized when and are as close to equal as possible (i.e., ≈ ≈ /2).
If is even, max(, , ) is minimized when = 1 and = = /2, giving max(, , ) = max(, /2), so 1(ℰ (3, 0; , , )) = max(, /2) when is even. If > 1 is odd, then max(, , ) is minimized when = 1 and {, } = {⌊/2⌋, ⌈/2⌉}, so 1(ℰ (3, 0; , , )) = max(, ⌈/2⌉) when > 1 is odd. If = 1, then max(, , ) is minimized when = 2 and = = 1 (note + = has no solutions in positive integers when = 1) and then 1(ℰ (3, 0; , , )) = max(1, 1, 2) = 2.
Suppose there is a solution to + = monochromatic in colour 0 (Dark Gray). Since gcd(, ) = 1 and there is no multiple of in 1, the variable must be in 2. Taking = 2 + + and = min(1) = + 1 as smallest possible values, we get = 3 + 2 + ( + 1) + 1, but () = 1 (Red) for ≥ 3 + 2 + ( + 1) + 1, a contradiction.
Suppose there is a solution to + = monochromatic in colour 1 (Red). Since 1 does not contain a multiple of , variable cannot be in 1. Also, if , ∈ 3, then clearly > 3 +2 +(2+1). So, and both cannot be in 3. Now we consider the following cases: (a) ∈ 2 and ∈ 1: We have = + = + for 1 ≤ ≤ . Since, ̸≡ 0 (mod ) , we have + ̸≡ 0 (mod ) which implies + ̸≡ 0 (mod 2). Hence + ̸∈ 2. If + ∈ 1, then since ≥ 1 and ≥ 1 , we have + > = max (1), a contradiction. (b) ∈ 2 and ∈ 2: We have ̸∈ 3 since ≤ ( 2)/ + 2 = 2 + 2
≤ 3 + 2 + ( + 1) < min(3) when 2 + + > 2 + . Suppose ∈ 2. In that case, 1 + 2 = 3 with 1 ≤ 1, 2, 3 ≤ 2 implies 1 + 2 = 3 with 1 ≤ 1, 2, 3 ≤ . Then, 1 = (/)(3 − 2) has no integer solution since gcd(, ) = 1 and 0 ≤ 3 − 2 < . Hence, () ̸= 1. (c) ∈ 3 and ∈ 1: Consider the condition, with 3 + 2 + ( + 1) + being the smallest integer in 3 which is divisible by . Then, we have 2 + + > + 2 which can be re-written as (3 + 2 + ( + 1) + ) + 1 > (2 + 2 + + ) + 1, which implies
> (3 + 2 + 2/ + /) > max(3).
Hence, () ̸= 1, a contradiction. (d) ∈ 3 and ∈ 2: As in the previous case, with 3 + 2 + ( + 1) + being the smallest integer in 3 which is divisible by , and 2 being the smallest integer in 2, we get > max(3) implying ̸∈ 3 implying () ̸= 1, a contradiction.
Suppose there is a solution to + = monochromatic in colour 2 (Blue). Then we have the following cases: (i) If , ∈ 2, then =
which results a contradiction since integers beyond max(2) are coloured in either colour 0 or in colour 1. (ii) If , ∈ 1, then in the equation = + , we have ≡ 1, 2, . . . , − 1 (mod ) . Since gcd(, ) = 1, we have ≢ 0 (mod ) . Hence, = + ̸≡ , 2, . . . , ( − 1) (mod 2) and ̸≡ 0 (mod ) implying () ̸= 2, a contradiction. (iii) If ∈ 1 and ∈ 2, then as in the previous case, we have ≢ 0 (mod ) . Since ≡ 0 (mod ), we have + ̸≡ 0 (mod ), that is, ̸∈ 2. Hence, () ̸= 2, a contradiction. (iv) If ∈ 2 and ∈ 1, then = + ≥ ( 2 + )/ + = 2 + + > max(1). Also, since ̸≡ 0 (mod ), we have ̸∈ 2. Hence, () ̸= 2, a contradiction.
3(ℰ (3, 0; , , )) ≥ 3 + 2 + (2 + 1) + 1
Lemma C.1. Let be a positive integer. There is no integer solution 1, 2, 3 to the equation 1 +2 = ( + 1)3 if any of the following is true: a. 1, 2, 3 ̸≡ 0 (mod ); b. 1, 2, 3 ≡ 0 (mod ) and 1, 2, 3 ̸≡ 0 (mod 2); c. 1, 2 ≡ 0 (mod 2) and 3 ̸≡ 0 (mod ); d. 1, 3 ≡ 0 (mod 2) and 2 ̸≡ 0 (mod ); e. 2, 3 ≡ 0 (mod 2) and 1 ̸≡ 0 (mod ); f. 1 ≡ 0 (mod 2) and 2, 3 ̸≡ 0 (mod ); g. 2 ≡ 0 (mod 2) and 1, 3 ̸≡ 0 (mod ); Proof. In each of the cases, assume that an integer solution 1, 2, 3 exists to 1 + 2 = ( + 1)3. a. Simplifying the equation, we get 1 + 2 = 3 + 3/, which due to the integrality assumption, implies |3, that is, 3 ≡ 0 (mod ), a contradiction. b. For = 1, 2, 3, since ≡ 0 (mod ) and ̸≡ 0 (mod 2), let = · such that ̸≡ 0 (mod ). Upon substitution, we obtain 2 · ( 1 + 2 − 3) = · 3 which implies 3 ≡ 0 (mod ) , a contradiction. c. Let 1 = 21 and 2 = 22. Then after substitution and simplification, we obtain 21 + 22 = 3 + 3/, which due to the integrality assumption, implies |3, that is, 3 ≡ 0 (mod ) , a contradiction. d. Let 1 = 21 and 3 = 23. Then after substitution and simplification, we obtain 1 + 2/ = 3 + 3, which due to the integrality assumption, implies |2, that is, 2 ≡ 0 (mod ) , a contradiction. e. Let 2 = 22 and 3 = 23. Then after substitution and simplification, we obtain 1/ + 2 = 3 + 3, which due to the integrality assumption, implies |1, that is, 1 ≡ 0 (mod ) , a contradiction. f. Let 1 = 21. Then after substitution and simplification, we obtain 21 + 2 = 3 + 3/, which due to the integrality assumption, implies |3, that is, 3 ≡ 0 (mod ), a contradiction. g. Let 2 = 22. Then after substitution and simplification, we obtain 1 + 22 = 3 + 3/, which due to the integrality assumption, implies |3, that is, 3 ≡ 0 (mod ), a contradiction.
Lemma C.2. For odd positive integer ≥ 7 , there exists no monochromatic solution to 1 + 2 = ( + 1)3 in colour 0.
Proof. If ∈ ( ) ∖ 2 ( ), then by Lemma C.1(b), there exists no solution to 1 + 2 = ( + 1)3. Hence there is no solution to 1 + 2 = ( + 1)3 monochromatic in colour 0. Lemma C.3. There exists no monochromatic solution to 1 + 2 = ( + 1)3 if 1, 2, 3 ∈ . Proof. Given 1, 2 ∈ , assume that 3 ∈ where 3 = (1 + 2)/( + 1). Let 1 = 12 and 2 = 22 for positive integers 1 and 2. Substituting for 3, we get the numerator to be 3(1 + 2). Since 3 shares no factor with + 1, if + 1 does not divide 1 + 2, then 3 ̸∈ Z, a contradiction. Assume that 1 + 2 = ( + 1) for some positive integer .
Assume that 1 + 2 = ( + 1) for some positive integer . Then, = 3, but for 1 ≤ ≤ − 1 , by definition of the sets and , we have 3 ∈ and since ∩ = ∅, we have 3 ̸∈ . If = 4, then = implying 1 + 2 = ( + 1) which is impossible since 1 + 2 ≤ + ≤ 2 − 1 < ( + 1) given 0 ≤ ≤ − 1, + 1 ≤ ≤ − 1.
Lemma C.4. For odd positive integer ≥ 7 , there exists no monochromatic solution to 1 + 2 = ( + 1)3 if 1, 2 ∈ ℓ and 3 ∈ .
Proof. Since 1, 2 ∈ ℓ, let 1 = 1( + 1) + 1 and 2 = 2( + 1) + 2 with 0 ≤ 1, 2 ≤ 2 − 1 , 1 ≤ 1, 2 < ( + 1). Also, let 3 = 23. Therefore, 3 = (1 + 2) + 1 + 2 ( + 1) .
If 1 + 2 = ( + 1), then by construction of ℓ and ℓ, the integers 1 and 2 both not in the same set, a contradiction.
Lemma C.5. For odd positive integer ≥ 7 , there exists no monochromatic solution to 1 + 2 = ( + 1)3 in colour 1.
Proof. Let = 1 ∪ 2 ∪ 3 with 1 = {︀ 4}︀ , 2 = ⋃︀=−11 ︀{ 3 + 2 : + 1 ≤ ≤ − 1 ︀} , and 3 = ⋃︀(−1)/2 {︀ 3 + 2}︀ . There are 43 = 64 ways to select an integer for the variables 1, 2, 3 =1 from the 4 sets ℓ, 1, 2, 3. Most of these cases can be analyzed directly using Lemma C.1 as follows: • 1, 2, 3 ∈ ℓ: No monochromatic solution by Lemma C.1 (a) covering 1 case. • 1 ∈ ℓ, 2, 3 ∈ : No monochromatic solution by Lemma C.1 (e) covering 9 cases. • 2 ∈ ℓ, 1, 3 ∈ : No monochromatic solution by Lemma C.1 (d) covering 9 cases. • 3 ∈ ℓ, 1, 2 ∈ : No monochromatic solution by Lemma C.1 (c) covering 9 cases. • 2, 3 ∈ ℓ, 1 ∈ : No monochromatic solution by Lemma C.1 (f) covering 3 cases. • 1, 3 ∈ ℓ, 2 ∈ : No monochromatic solution by Lemma C.1 (g) covering 3 cases. • 1, 2 ∈ ℓ, 3 ∈ : No monochromatic solution by Lemma C.4 covering 3 cases. • 1, 2, 3 ∈ : No monochromatic solution by Lemma C.3 covering 27 cases.
Hence, there exists no monochromatic solution to 1 + 2 = ( + 1)3 in colour 1. Lemma C.6. For an odd positive integer ≥ 7, the set contains no solution to ℰ (3, 0; , , + 1). Proof. Given 1, 2 ∈ , assume that 3 = 1+2 and 3 ∈ . Let 1 = 12 and 2 = 22 +1 for positive integers 1 and 2. Substituting for 3, we get the numerator to be 3(1 + 2). Since 3 shares no factor with + 1, if + 1 does not divide 1 + 2, then ̸∈ Z, a contradiction. Assume that 1 + 2 = ( + 1) for some positive integer . Then, = 3 and assume ∈ . For 1 ≤ ≤ − 1 , 4 + 2 is not an integer multiple of 3. Since min() = 3, we have 1 + 2 ≥ 2 and the smallest integer value of is obtained when 1 + 2 = ( + 1). This implies ≥ 4, but max(2 ∪ 3) < 4. Hence, ̸∈ .
Therefore, the set contains no solution to 1 + 2 = ( + 1)3.
Lemma C.7. For odd positive integer ≥ 7 , there exists no monochromatic solution to 1 + 2 = ( + 1)3 if 1, 2 ∈ ℓ and 3 ∈ .
Lemma C.8. For odd positive integer ≥ 7 , there exists no monochromatic solution to 1 + 2 = ( + 1)3 in colour 2.
Proof. Let = 1 ∪ 2 ∪ 3 with partition blocks 1 = ⋃︀=−11 ︀{ 4 + 2}︀ , 2 = ⋃︀=−11 ︀{ 3 + 2 : 0 ≤ ≤ − 1 ︀} , and 3 = ⋃︀=−1(+1)/2 ︀{ 3 + 2}︀ . There are 43 = 64 ways to select an integer for the variables 1, 2, 3 from the 4 sets ℓ, 1, 2, 3. Most of these cases can be analyzed directly using Lemma C.1 as follows: • 1, 2, 3 ∈ ℓ: No monochromatic solution by Lemma C.1 (a) covering 1 case. • 1 ∈ ℓ, 2, 3 ∈ : No monochromatic solution by Lemma C.1 (e) covering 9 cases. • 2 ∈ ℓ, 1, 3 ∈ : No monochromatic solution by Lemma C.1 (d) covering 9 cases. • 3 ∈ ℓ, 1, 2 ∈ : No monochromatic solution by Lemma C.1 (c) covering 9 cases. • 2, 3 ∈ ℓ, 1 ∈ : No monochromatic solution by Lemma C.1 (f) covering 3 cases. • 1, 3 ∈ ℓ, 2 ∈ : No monochromatic solution by Lemma C.1 (g) covering 3 cases. • 1, 2 ∈ ℓ, 3 ∈ : No monochromatic solution by Lemma C.7 covering 3 cases. • 1, 2, 3 ∈ : No monochromatic solution by Lemma C.6 covering 27 cases.
Hence, there exists no monochromatic solution to 1 + 2 = ( + 1)3 in colour 2. D. SMT Instance via the Z3 Python API for Example 3.1 from z3 import * # Declare symbolic variables a = Int('a') x1, x2, x3 = Ints('x_1 x_2 x_3') k1, k2 = Ints('k_1 k_2') i, j, k = Ints('i j k') # Create the solver s = Solver() # Global assumptions s.add(a >= 1) # Equation constraint # Non-divisibility: not(a^2 | x2) s.add(ForAll([k2], And(k2>0, x2 != a**2 * k2))) # Format expression for x3 s.add(x3 == a*(a + 1)*i + a*j + k) # Bounds for x1, x2, x3 s.add(x1 >= 1, x1 <= a**2) s.add(x2 >= 1, x2 <= a**2) s.add(x3 >= 1, x3 <= a**2)