针对高维Erd\H{o}s--Szekeres数的SAT攻击

Erd\H{o}s与Szekeres(1935)的一个著名结论断言:对所有$k,d \in \mathbb{N}$,存在最小整数$n = g^{(d)}(k)$,使得$\mathbb{R}^d$中任一处于一般位置的至少$n$个点之集合均包含一个$k$-边形,即处于凸位置的$k$个点的子集。本文中,我们提出一种基于非循环chirotopes(定向拟阵)的SAT模型,以研究小维度下的Erd\H{o}s--Szekeres数。为求解SAT实例,我们使用现代SAT求解器,且所有不可满足结果均通过DRAT证书验证。我们证明了$g^{(3)}(7) = 13$、$g^{(4)}(8) \le 13$与$g^{(5)}(9) \le 13$,这些是数十年来首次取得的改进。对于$k$-洞(即凸包内不含其他点的$k$-边形)的情形,其中$h^{(d)}(k)$表示使得$\mathbb{R}^d$中任一处于一般位置的至少$n$个点之集合均包含一个$k$-洞的最小整数$n$,我们证明$h^{(3)}(7) \le 14$、$h^{(4)}(8) \le 13$与$h^{(5)}(9) \le 13$。此外,所有获得的界在非循环chirotopes设定下均为紧的,我们猜想其在原始点集设定下亦为紧的。作为副产品,我们验证了先前已知的界。特别地,我们给出了Gerken(2008)上界$h^{(2)}(6)\le g^{(2)}(9) \le 1717$的首个计算机辅助证明。