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

Abstract

A famous result by Erdős and Szekeres (1935) asserts that, for all $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, that is, a subset of $k$ points which is in convex position. In this article, we present a SAT model based on acyclic chirotopes (oriented matroids) to investigate Erdős--Szekeres numbers in small dimensions. To solve the SAT instances we use modern SAT solvers and all our unsatisfiability results are verified using DRAT certificates. We show $g^{(3)}(7)=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 acyclic chirotopes and we conjecture them to be sharp also in the original setting of point sets. As a byproduct, we verify previously known bounds. In particular, we present the first computer-assisted proof of the upper bound $h^{(2)}(6)\le g^{(2)}(9)\le 1717$ by Gerken (2008).