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 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., 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,
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 (a $k$-gon with no other points in its convex hull),
we show
$h^{(3)}(7) \le 14$,
$h^{(4)}(8) \le 13$, and
$h^{(5)}(9) \le 13$.
We conjecture that all our obtained bounds are sharp
as they are sharp in the setting of chirotopes.
## Short description of the programs

We provide a python programs to formulate a SAT instance
to verify bounds on $g^{(d)}(k)$ and $h^{(d)}(k)$ for dimensions $d=3,4,5$.
For example, to create an instance for testing $g^{(3)}(7) \stackrel{?}{\le} 13$, run
## Downloads

python test3d.py 0 7 13To create an instance for testing $h^{(4)}(8) \stackrel{?}{\le} 13$, run

python test4d.py 1 8 13The 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]

- The source code of the program "test3d.py" to verify $g^{(3)}(7) \le 13$ and $h^{(3)}(7) \le 14$. [download]
- The source code of the program "test4d.py" to verify $g^{(4)}(8) \le h^{(4)}(8) \le 13$. [download]
- The source code of the program "test5d.py" to verify $g^{(5)}(9) \le h^{(5)}(9) \le 13$. [download]