精确拉姆齐理论：Green-Tao数与SAT

我们考虑了基于范德瓦尔登定理的整数拉姆齐理论与（布尔、CNF）SAT求解之间的联系。我们的目标是将精确拉姆齐理论中涉及计算拉姆齐型数的问题作为一个丰富的测试问题源，特别是可以借此开发求解困难问题的方法。为了控制问题实例的增长，我们引入了“横截扩展”，作为构造范德瓦尔登型数 $N(k_1, \dots, k_m)$ 的混合参数元组 $(k_1, \dots, k_m)$ 的一种自然方式，从而保证这些数的增长是线性的。基于 Green-Tao 定理，我们引入了“Green-Tao数” $\text{grt}(k_1, \dots, k_m)$，它在某种意义上结合了范德瓦尔登问题的严格结构与素数分布的（伪）随机性。使用标准SAT求解器（前瞻、冲突驱动和局部搜索），我们确定了其基本值。结果表明，即使对于这种单一形式的拉姆齐型问题，当考虑性能最佳的求解器时，也涵盖了种类繁多的求解器类型。对于 $m > 2$，问题是非布尔的，我们引入了“通用翻译方案”，它提供了无限多样的翻译（“编码”），并涵盖了已知的方法。在大多数情况下，被称为“嵌套翻译”的特殊实例被证明具有极大的优越性。