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
python test3d.py 0 7 13
To create an instance for testing $h^{(4)}(8) \stackrel{?}{\le} 13$, run
python test4d.py 1 8 13
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]

Downloads

Last update: 09.03.2021, (c) 2021 Manfred Scheucher