2025/05/17 by Tanbir Ahmed, Ahmed, Tanbir, Lamina Zaman +3 · 1 citation
Computer Science · #Advanced Graph Theory Research #Combinatorics (math.CO) #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Polynomial and algebraic computation #Symbolic Computation (cs.SC)
paper · pdf · doi:10.48550/arxiv.2505.12085
openalex publication_date 2025/05/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Given a linear equation \cal E of the form ax + by = cz where a, b, c are positive integers, the k-colour Rado number Rk(\cal E) is the smallest positive integer n, if it exists, such that every k-colouring of the positive integers \1, 2, \dotsc, n\ contains a monochromatic solution to \cal E. In this paper, we consider k = 3 and the linear equations ax + by = bz and ax + ay = bz. 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 difficult 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 \f(1), f(2), \dotsc, f(a)\ where a is a symbolic variable and f is a function possibly dependent on a. No computer algebra system that we are aware of currently has sufficiently 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.