A SAT attack on higher dimensional Erdős--Szekeres numbers

A famous result by Erd\H{o}s and Szekeres (1935) asserts that, for every $k,d \in \mathbb{N}$, there is a smallest integer $n = g^{(d)}(k)$, such that every set of at least $n$ points in $\mathbb{R}^d$ in general position contains a $k$-gon, i.e., a subset of $k$ points which is in convex position. We present a SAT model for higher dimensional point sets which is based on chirotopes, and use modern SAT solvers to investigate Erd\H{o}s--Szekeres numbers in dimensions $d=3,4,5$. We show $g^{(3)}(7) \le 13$, $g^{(4)}(8) \le 13$, and $g^{(5)}(9) \le 13$, which are the first improvements for decades. For the setting of $k$-holes (i.e., $k$-gons with no other points in the convex hull), where $h^{(d)}(k)$ denotes the minimum number $n$ such that every set of at least $n$ points in $\mathbb{R}^d$ in general position contains a $k$-hole, we show $h^{(3)}(7) \le 14$, $h^{(4)}(8) \le 13$, and $h^{(5)}(9) \le 13$. Moreover, all obtained bounds are sharp in the setting of chirotopes and we conjecture them to be sharp also in the original setting of point sets.