Symbolic Sets for Proving Bounds on Rado Numbers
Tanbir Ahmed, Lamina Zaman, Curtis Bright
给定形式 ax + by = cz 的线性方程 E,其中 a, b, c 是正整数, k 色 R_k(E) 是最小的正整数 n,如果它存在,使得正整数 {1, 2, ..., n} 的每个 k 着色都包含 E 的单色解。 在本文中,我们考虑 k = 3 和线性方程 ax + by = bz 和 ax + ay = bz。 使用SAT求解器,我们计算了一些与这些方程对应的以前未知的Rado数字。 我们证明了对 Rado 数字的新的一般界限,灵感来自 SAT 求解器发现的令人满意的作业。 我们的证明需要广泛的基于案例的分析,这些分析很难用手检查正确性,所以我们通过使用我们开发的新方法自动检查证明的正确性,该方法支持符号定义集的操作 - 例如,表单{f(1),f(2),...,f(a)}的集合的工会或交叉点,其中a是一个符号变量,f是可能依赖于a的函数。 我们所知的计算机代数系统目前对符号集有足够能力的支持,导致我们开发了一个支持符号集的工具,使用Python符号计算库SymPy加上可满足性模块理论解决器Z3。
Given a linear equation E of the form ax + by = cz where a, b, c are positive integers, the k-colour Rado number R_k( E) is the smallest positive integer n, if it exists, such that every k-colouring of the positive integers {1, 2, …, n} contains a monochromatic solution to 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 bound...