通过 SAT 与计算机代数系统为 Ramsey $R(3, 8)$ 和 $R(3, 9)$ 问题生成验证证书

Ramsey 问题 $R(3, k)$ 旨在确定最小值 $n$，使得任意给定大小为 $n$ 的完全图的红/蓝边着色必须包含蓝色三角形（3- clique）或红色大小为 $k$ 的 clique。尽管该问题具有重要意义，但许多针对 Ramsey $R(3, k)$ 问题的计算结果（如 $R(3, 8)$ 和 $R(3, 9)$）缺乏形式化验证。为此，我们使用 MathCheck 软件通过将布尔满足问题（SAT）求解器与计算机代数系统（CAS）集成，为 Ramsey 问题 $R(3, 8)$ 和 $R(3, 9)$（以及对称的 $R(8, 3)$ 和 $R(9, 3)$）生成证书。我们的 SAT+CAS 方法显著优于传统仅使用 SAT 的方法，在运行时间上提升了多个数量级。例如，我们的 SAT+CAS 方法依次在 59 小时（分别为 11 小时）内解决 $R(3, 8)$（分别为 $R(8, 3)$），而仅使用最先进 CaDiCaL 求解器的 SAT 方法在 7 天后仍会超时。此外，为扩展到更困难的 Ramsey 问题 $R(3, 9)$ 和 $R(9, 3)$，我们进一步优化了 SAT+CAS 工具，采用并行化的 cube-and-conquer 方法。我们的结果为这些 Ramsey 数提供了第一个独立可验证的证书，确保了 SAT+CAS 工具的穷举搜索过程的正确性和完整性。