用于证明Rado数 bounds的符号集

给定形式为 $ax + by = cz$ 的线性方程 $\cal E$，其中 $a$, $b$, $c$ 为正整数，$k$ 色Rado数 $R_k({\cal E})$ 是指最小的正整数 $n$（若存在），使得 $\{1, 2, \dotsc, n\}$ 中的每个 $k$ 色染色都包含满足 $\cal E$ 的单色解。本文考察 $k = 3$ 以及线性方程 $ax + by = bz$ 和 $ax + ay = bz$。我们利用SAT求解器计算了若干此前未知的Rado数。我们受SAT求解器发现的满足赋值启发，证明了关于Rado数的若干新型界限。我们的证明需要大量的案例分析，这些分析对手工检查正确性困难，因此我们通过一种利用我们新开发的工具进行自动化检查正确性的方法来实现，其中支持对符号定义集的操作——例如形如 $\{f(1), f(2), \dotsc, f(a)\}$ 的集合的并或交，其中 $a$ 为符号变量，$f$ 可能依赖于 $a$。目前尚无任何计算机代数系统能够提供足够强大的符号集支持，因此我们开发了一个基于SymPy coupled with SAT求解器 Z3 的工具来支持符号集。