Back to my homepage

A SAT attack on higher dimensional Erd\H{o}s--Szekeres numbers

This website provides programs to verify the computer-assisted results from my paper "A SAT attack on higher dimensional Erd\H{o}s--Szekeres numbers".

Abstract of the paper

A famous result by Erd\H{o}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 \emph{$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\H{o}s--Szekeres numbers in small dimensions. To solve the SAT instances 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 \emph{$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 all previous known bounds and, in particular, present the first computer-assisted proof of the upper bound $h^{(2)}(6)\le g^{(2)}(9) \le 1717$ by Gerken (2008).

Description of the programs

We provide a python program "" to formulate a SAT instance to verify our obtained bounds on $g^{(d)}(k)$ and $h^{(d)}(k)$ for dimensions $d=3,4,5$. The program can also be used to verify previously known bounds on $g^{(d)}(k)$ and $h^{(d)}(k)$ in dimensions $d=2,3$. The first parameter "0" indicates that we forbid $k$-gons and "1" indicates that we forbid $k$-holes. The value $k$ is specified in the second parameter. The third parameter specifies the dimension $d$. The fourth parameter specifies the number of points $n$. The SAT instance is written to a CNF-file, which then can be solved using a SAT solver such as CaDiCaL:
cadical [instance]
In case of unsatisfiability, CaDiCal can create a unsatisfiability proof, which can then be verified by a proof checking tool such as DRAT-trim:
cadical [instance] [proof] && drat-trim [instance] [proof]

Existence of planar 6-holes

We have slightly adapted the general program "" to verify the bound $h^{(2)}(6) \le g^{(2)}(9)$ (Gerken 2008). To create an instance with $9$ extremal and $n-9$ inner points, for $n=9,\ldots,22$, run
for n in {9..22}; do python $n; done
Similar as the program "", the created SAT instances can be solved and verified using CaDiCaL and DRAT-trim, respectively:
for n in {9..22}; do cadical _planar_6holes_n$ _planar_6holes_n$n.proof -q; done
for n in {9..22}; do drat-trim _planar_6holes_n$ _planar_6holes_n$n.proof -w; done


Programs: Witnesses: Last update: 17.04.2022, Manfred Scheucher