Two Disjoint 5-Holes in Point Sets
Manfred Scheucher



Synthesizing CT from Ultrashort Echo-Time MR Images via Convolutional Neural Networks
    Snehashis Roy1 
Support for this work included funding from the Department of Defense in the
Center for Neuroscience and Regenerative Medicine.
John A. Butman2 
Dzung L. Pham1

    December 30, 2023
====================================================================================================================================================================================




Given a set of points S ⊆ℝ^2, 
a subset  with |X|=k is called 
 if all points of X lie on the boundary of the convex hull of X,
and k-hole if, in addition, no point of S ∖ X lies in the convex hull of X.
We use computer assistance to show that every set of 17 points in general position 
admits two disjoint 5-holes, that is, holes with disjoint respective convex hulls.
This answers a question of Hosono and Urabe (2001).
We also provide new bounds for three and more pairwise disjoint holes.

In a recent article, Hosono and Urabe (2018) 
present new results on interior-disjoint holes – a variant,
which also has been investigated in the last two decades. 
Using our program, we show
that every set of 15 points contains two interior-disjoint 5-holes.

Moreover, our program can be used to verify 
that every set of 17 points contains a 6-gon
within significantly smaller computation time
than the original program by Szekeres and Peters (2006).
Another independent verification of this result 
was done by Marić (2019).







§ INTRODUCTION


A set S of points in the Euclidean plane is in general position
if no three points lie on a common line.
Throughout this paper all point sets are considered to be finite and in general position.
A subset X ⊆ S of size |X| = k is a  
if all points of X lie on the boundary of the convex hull of X, denoted by (X).
A classical result of Erdős and Szekeres from the 1930s asserts that, for fixed k ∈ℕ, 
every set of 2k-4k-2+1 points contains a k-gon <cit.> (cf. <cit.>).
They also constructed point sets of size 2^k-2 with no k-gon.
There were several small improvements on the upper bound by various researchers in the last decades, 
each of order 4^k-o(k),
until Suk <cit.> significantly improved the upper bound to 2^k+o(k).
However, the precise minimum number g(k) 
of points needed to guarantee the existence of a k-gon is still 
unknown for k≥7 (cf. <cit.>)[
Erdős offered $500 for a proof of Szekeres' conjecture that g(k) = 2^k-2+1.].

In the 1970s, Erdős <cit.> asked 
whether every sufficiently large point set
contains a k-hole, that is, 
a k-gon with no other points of S lying inside its convex hull.
Harborth <cit.> showed that every set of 10 points contains a 5-hole
and Horton <cit.> introduced a construction of arbitrarily large point sets without 7-holes.
The question, whether  exist in sufficiently large point sets, remained open until 2007, 
when Nicolas <cit.> and Gerken <cit.> 
independently showed that point sets with large k-gons also contain 6-holes[
For a reasonably short proof for the existence of 6-holes we refer to <cit.>.].
In particular, Gerken proved that every point set
that contains a 9-gon also contains a .
The currently best upper bound on the number of points is by Koshelev <cit.>[
Koshelev's publication covers more than 50 pages (written in Russian)],
who showed that every set of 463 points contains a .
However, the largest set without  currently known has 29 points 
and was found using a simulated annealing-based approach by Overmars <cit.>.


In 2001, Hosono and Urabe <cit.> 
and Bárány and Károlyi <cit.>
started the investigation of disjoint holes,
where two holes X_1,X_2 of a given point set S 
are said to be disjoint
if their respective convex hulls are disjoint 
(that is, (X_1) ∩(X_2) = ∅; see Figure <ref>).
This led to the following question: 
What is the smallest number h(k_1,…,k_l) such that
every set of h(k_1,…,k_l) points determines
a k_i-hole for every ,
such that the holes are pairwise disjoint <cit.>?
As there are arbitrarily large point sets without 7-holes,
only parameters k_i < 7 are of interest.
Moreover, 
since the gap between the upper bound and the lower bound for h(6) is still huge, 
mostly values with parameters k_1,…,k_l ≤ 5 were investigated.
Also note that, if all k_i are at most 3, 
then the value h(k_1,…,k_l)=  k_1 + … + k_l is straight-forward
because every set of k_1+…+k_l points can be 
cut into blocks of k_1,…,k_l points (from left to right), 
which clearly determine the desired holes.






In Sections <ref> and <ref>,
we summarize the current state of the art 
for two- and three-parametetric values
and we present some new results 
that were obtained using computer-assistance.
Our main contribution is 
that every set of 17 points contains two disjoint 5-holes (Theorem <ref>).
Moreover, we describe some direct consequenses for multi-parametric values 
in Section <ref>.
The basic idea behind our computer-assisted proofs 
is to encode point sets and disjoint holes only using triple orientations (see Section <ref>),
and then to use a SAT solver to disprove 
the existence of sets with certain properties (see Section <ref>).

In the Final Remarks (Section <ref>)
we outline how our SAT model can be adapted to tackle related questions on point sets.
For interior-disjoint holes, we show that every set of 15 points contains two interior-disjoint 5-holes.
Also it is remarkable,
that our SAT model can be used to prove g(6)=17 with significantly smaller computation time
than the original program from Szekeres and Peters <cit.>[
Szekeres and Peters  considered the problem of finding sets without 6-gons
also in the setting of triple-orientations (cf. Section <ref>),
and implemented a sophisticated exhaustive search technique in a classical program 
 (no SAT solvers involved).
].
Last but not least, we also outline how SAT solvers can be used to 
count occurences of certain substructures (such as k-holes in point sets).




§ TWO DISJOINT HOLES



For two parameters, the value h(k_1,k_2) has been determined 
for all k_1,k_2 ≤ 5, except for h(5,5), 
by Hosono and Urabe <cit.> 
and by Bhattacharya and Das <cit.>.
Table <ref> summarizes the currently best bounds for two-parametric values.
The upper bounds were obtained via case distinctions 
and, to obtain values of h(k,5), also the value h(5)=10 was utilized <cit.>.
Lower bounds are witnessed by concrete examples of point sets.
It is also worth mentioning that all statements, which involve  11 or less points,
can be verified by checking the order type database of 11 points[
The database of all combinatorially different sets of n ≤ 10 points is available online 
at <cit.> 
and requires roughly 550 MB of storage.
The database for n=11 requires about 100 GB of storage and is available on request.
For more information we refer to <cit.>.].
However, for  h(4,5)=12 <cit.> 
this database does not directly allow a direct proof.

Concerning the value h(5,5), the best bounds are .
The lower bound h(5,5) ≥ 17 is witnessed by a set of 16 points 
with no two disjoint 5-holes (taken from Hosono and Urabe <cit.>),
which is depicted Figure <ref>. 
For the upper bound, Bhattacharya and Das <cit.>
used elaborate case distinctions to reveal more and more structural information
of point sets without (two disjoint) 5-holes to finally conclude that h(5,5) ≤ 19.






As our main result of this paper,
we determine the precise value of h(5,5).
The proof is based on a SAT model which we later describe in Section <ref>.
We remark that our SAT model can easily be adapted 
to also verify the other entries of Table <ref>.



Every set of 17 points contains two disjoint 5-holes, 
hence h(5,5)=17.


The computations for verifying Theorem <ref>
take about two hours on a single 3 GHz CPU using a modern SAT solver such as 
glucose (version 4.0)[<http://www.labri.fr/perso/lsimon/glucose/>, see also <cit.>] or 
picosat (version 965)[<http://fmv.jku.at/picosat/>, see also <cit.>].
Moreover, we have verified the output of glucose and picosat with the proof checking tool
drat-trim[<http://cs.utexas.edu/ marijn/drat-trim>, see also <cit.>]
(see Section <ref>).






§ THREE DISJOINT HOLES



For three parameters, 
most values h(k_1,k_2,k_3) for k_1,k_2,k_3 ≤ 4  
and also the values h(2,3,5)=11 and h(3,3,5)=12 have been determined by Hosono and Urabe <cit.> and by You and Wei <cit.>.
Tables <ref> and <ref> 
summarize the currently best known bounds for three-parametric values.
Again it is worth mentioning that all statements, which involve  11 or less points,
can be verified by checking the order type database of 11 points <cit.>.




The values h(2,2,4), h(3,3,4), and h(2,4,4) 
have not been explicitly stated in literature.
However, the former two can be derived directly from other values as follows:

    8 = 2+2+4 ≤ h(2,2,4)    ≤ 2+h(2,4)= 8
    
    10 = 3+3+4 ≤ h(3,3,4)    ≤ 3+h(3,4) = 10

To determine the value h(2,4,4)=11,
observe that h(2,4,4) ≤ 2+h(4,4) = 11 clearly holds.
Equality is witnessed by
the double circle  
with 10 points 
(cf. Figure <ref>).
This statement can be verified by computer or as follows:
First, observe that no 4-hole contains 
two consecutive extremal points,
thus every 4-hole contains at most two exterior points.
Now consider two disjoint 4-holes.
Since not both 4-holes can contain two extremal points,
one of them
contains  two exterior points
while the other one contains  one exterior point.
As illustrated in Figure <ref>,
this configuration is unique up to symmetry and
does not allow any further disjoint 2-hole.
This completes the argument.



Also we could not find the value h(2,2,5) in literature,
however, using a SAT instance similar to the one for Theorem <ref>
one can also easily verify that h(2,2,5) ≤ 10,
and equality follows from h(5)=10 <cit.>.
One can also use the order type database <cit.> 
to verify h(2,2,5) ≤ 10.






We now use
Theorem <ref> to derive new bounds 
on the value h(k,5,5) for k =2,3,4,5.


We have 

                 h(2,5,5)     =     17,

17     ≤     h(3,5,5)     ≤     19,

17     ≤     h(4,5,5)     ≤     23,

22     ≤     h(5,5,5)     ≤     27.



 
To show h(2,5,5) ≤ 17,
observe that, due to Theorem <ref>,
every set of 17 points contains two disjoint 5 holes
that are separated by a line ℓ. 
By the pigeonhole principle there are at least 9 points on one of the two sides of such a separating line ℓ.
It is implied by h(2,2,5)=10 that
every set of 9 points with a 5-hole also contains a 2-hole which is
disjoint from the 5-hole.
This completes the argument.
We remark that one can also use the order type database of 9 points to verify this statement.

To show h(3,5,5) ≤ 2· h(3,5)-1 =19,
observe that, due to Theorem <ref>,
every set of 19 points contains two disjoint 5 holes
that are separated by a line ℓ. 
Now there are at least 10 points on one side of such a separating line ℓ,
and since h(3,5)=10, there is a 3-hole and a 5-hole that are disjoint 
on that particular side. 

An analogous argument shows h(4,5,5) ≤ 2· h(4,5)-1 = 23.

The set of 21 points depicted in Figure <ref> witnesses h(5,5,5) > 21
(can be easily verified by computer),
while h(5,5,5) ≤ h(5)+h(5,5) = 27.
We remark that this point set was found using local search techniques,
implemented in our framework pyotlib[
The “python order type library” was initiated during 
the Bachelor's studies of the author <cit.> 
and provides many features to work with (abstract) order types
such as 
local search techniques, 
realization or proving non-realizability of abstract order types, 
coordinate minimization and “beautification” for nicer visualizations.
For more information, please consult the author.].
The key idea was to start with an arbitrary set of 21 points
and to move points around until 
the number of triples of disjoint 5-holes becomes zero.










§ MANY DISJOINT HOLES



As introduced by Hosono and Urabe <cit.>, we use the following notation:
Given positive integers k and n, let F_k(n) denote the maximum number of pairwise disjoint k-holes that 
can be found in every set of n points,
that is,

    F_k(n) := max ({0}∪{t ∈ℕ h(k;t) ≤ n }) 
      with   
    h(k;t) := h(k,k,…,k^t parameters).

In the following, we revise and further improve results by
Hosono and Urabe <cit.>
and by
Bárány and Károlyi <cit.>.
The currently best bounds are the following:

      F_k(n)     =      ⌊n/k ⌋      for k=1,2,3 

3n/13 - o(n)       ≤     F_4(n)     ≤     n/4

2n/17 -O(1)     ≤     F_5(n)     ≤     n/6+O(1)

n/h(6)-O(1)     ≤    F_6(n)     ≤     n/8+O(1)

      F_k(n)     =      0       for k ≥ 7.


Concerning the lower bounds, 
Theorem <ref> clearly implies F_5(n) ≥⌊ 2n/17 ⌋.
In the following, we outline the proof of   F_4(n) ≥ 3n/13 - o(n).
Hosono and Urabe <cit.> showed that F_4(n) ≥ (3n-1)/13 
holds for an infinite sequence of integers n, which we denote by N.
Let T := {F_4(n) : n ∈ N}.
Note that T is also infinite.
From the definition of F_4(n) and the F_4(n) ≥ (3n-1)/13 bound for n∈ N,
we conclude that

    h(4;F_4(n))  ≤ n ≤13F_4(n)+1/3

holds for every n ∈ N,
and hence h(4;t) ≤13t+1/3 for every t ∈ T.
Since h(4;s+t) is subadditive,
that is h(4;s+t) ≤ h(4;s) + h(4;t),
Fekete's subadditivity lemma
(see for example <cit.>)
asserts 

    lim_t →∞h(4;t)/t = inf_t ∈ℕh(4;t)/t ≤ inf_t ∈ T h(4;t)/t = 13/3.

Hence,
h(4;t) ≤13t/3 (1+o(1)) and
we conclude F_4(n) ≥3n/13 (1-o(1)).




Concerning the upper bounds,
Bárány and Károlyi <cit.> remarked
that no nontrivial upper bound is known for F_4 (n) in general.
They mentioned F_5(n)<n/6 
without an explicit construction 
but we only know a construction for
F_5(n) ≤n+1/6 (Gyula Károlyi, personal communication).
In the following, we give the construction
for F_5(n) ≤n+1/6 and F_6(n) ≤n+1/8.



We assume that n is even, and show F_5(n) ≤n/6 and F_6(n) ≤n/8. 
(For n odd, we can then conclude  
F_5(n) ≤ F_5(n+1) ≤n+1/6 and F_6(n) ≤ F_6(n+1) ≤n+1/8 from monotonicity.)
As illustrated in Figure <ref>, 
we take the
vertices of a regular n/2-gon (extremal points) plus the vertices
of a slightly shrinked copy of the regular n/2-gon with the same center (inner points).
If n/2 is even, we slightly rotate the inner points
around the center to maintain general position.
This way we get n/2 pairs of very close points.



We now show that no three extremal points form a 3-hole.
Suppose towards a contradiction 
that three extremal points a,b,c span an empty triangle .
By symmetry we may assume 
that a is the top-most vertex of the outer n/2-gon,
and that b lies below c.
Both points b and c must either lie to the left 
or to the right of a, 
as otherwise the inner partner of a would lie inside of .
Now, however, the inner partner of c lies in  
(cf. Figure <ref>) and hence  cannot be empty. A contradiction.

We conclude that every 5-hole (6-hole) 
is incident 
to at most 2 extremal points
and hence to at least 3 (4) inner points.
Therefore, 
at most 2/3 (2/4) of the exterior points 
can be covered by disjoint 5-holes (6-holes),
and we conclude F_5(n) ≤n/6 and F_6(n) ≤n/8 for n even.



§ ENCODING WITH TRIPLE ORIENTATIONS



In this section
we describe how point sets and disjoint holes 
can be encoded only using triple orientations.
This combinatorial description allows us to 
get rid of the actual point coordinates
and to only consider a discrete parameter-space.
This is essential for our SAT model of the problem.





 §.§ Triple Orientations



Given a set of points S={s_1,…,s_n} with s_i = (x_i,y_i),
we say that the triple (a,b,c) is positively (negatively) oriented 
if 

    χ_abc := [   1   1   1; x_a x_b x_c; y_a y_b y_c ]∈{-1,0,+1}

is positive (negative)[
 The letter χ is commonly used in literature 
 to denote triple orientations as the word “chirality”
 is derived from the Greek word for “hand”.].
 Equivalently, the triple (a,b,c) is positively (negatively) oriented 
 if the point c lies to the left (right) of the directed line ab.
 Figure <ref> gives an illustration.
 Note that χ_abc=0 indicates collinear points, 
 in particular, χ_aaa=χ_aab=χ_aba=χ_baa=0.
 


It is easy to see, 
that convexity is a combinatorial rather than a geometric property 
since k-gons
can be described only by the relative position of the points:
If the points s_1,…,s_k are the vertices of a convex polygon
(ordered along the boundary),
then, for every i=1,…,k, 
the cyclic order of the other points around s_i is 
s_i+1,s_i+2,…,s_i-1 (indices modulo k).
Similarly, one can also describe containment (and thus k-holes) 
only using relative positions: 
A point s_0 lies inside a convex polygon with vertices s_1,…,s_k (ordered along the boundary) 
if, for every i=1,…,k, 
the line s_is_i+1 does not separate s_0 
from the remaining vertices {s_1,…,s_k}∖{s_i,s_i+1} (indices modulo k).

To observe that the disjointness of two point sets
can be described solely using triple orientations,
suppose that a line ℓ separates point sets A and B.
Then, for example by rotating ℓ, we can find another 
line ℓ' that contains a point a∈ A and a point b∈ B
and separates A∖{a} and B∖{b}.
In particular,
we have χ_aba'≤ 0 for all a' ∈ A
and χ_abb'≥ 0 for all b' ∈ B, or the other way round.
Figure <ref> gives an illustration.
Altogether, the existence of disjoint holes can be described solely using triple orientations.
 
Note that, even though
there are uncountable possibilities to choose 
n points from the Euclidean plane for fixed n ∈ℕ,
there are only finitely many equivalence classes of point sets 
when point sets inducing the same orientation triples are considered equal.
As introduced by Goodman and Pollack <cit.>,
these equivalence classes 
(sometimes also with unlabeled points) 
are called order types. 

 


 §.§ An Abstraction of Point Sets



Consider a point set S={s_1,…,s_n} 
where s_1,…,s_n have increasing x-coordinates.
Using the unit paraboloid duality transformation,
which maps a point s=(a,b) to the line s^*:y=2ax-b,
we obtain the arrangement of dual lines S^* = {s_1^*,…,s_n^*},
where the dual lines s_1^*,…,s_n^* have increasing slopes.
By the increasing x-coordinates
and the properties of the unit paraboloid duality 
(cf. <cit.> or <cit.>), 
for every three points s_i,s_j,s_k with i<j<k 
the following three statements are equivalent:


  * The points s_i,s_j,s_k are positively oriented.

  * The point s_k lies above the line s_is_j.

  * The intersection-point of the two lines s_i^* and s_j^* lies above the line s_k^*.

Due to Felsner and Weil <cit.> 
(see also Balko, Fulek, and Kynčl <cit.>),
for every four points s_i,s_j,s_k,s_l with i<j<k<l,
the sequence 

    χ_ijk, χ_ijl, χ_ikl, χ_jkl
 
(index-triples are in lexicographic order)
changes its sign at most once. 
These conditions are the signotope axioms.
It is worth mentioning that the signotope axioms were also used 
in the computer-assisted proof for g(6)=17 by Szekeres and Peters <cit.>
and also later by Balko and Valtr <cit.>,
who refuted a natural strengthening of the Erdős–Szekeres conjecture 
introduced by Szekeres and Peters.

The signotope axioms are necessary conditions 
but not sufficient to axiomize point sets:
As described above, 
every point set S induces a mapping χ_S: n  3→{+,-}, 
which fulfills the signotope axioms.
However, there exist mappings χ_S: n  3→{+,-} fulfilling the signotopes axioms
– such mappings are called
signotopes,
abstract point sets,
abstract order types, and
abstract oriented matroids (of rank 3)
–
which are not induced by any point set,
and in fact, deciding
whether an abstract point set has a realizing point set 
is known to be ∃ℝ-complete.
For more information about realizability we refer to <cit.>.





 §.§ Increasing Coordinates and Cyclic Order


In the following, we see why
we can assume 
that in every point set S={s_1,…,s_n} with s_i=(x_i,y_i) the following three conditions hold:


  * the points s_1,…,s_n have increasing x-coordinates (i.e., x_1 ≤…≤ x_n)

  * in particular, s_1 is the leftmost point, and

  * the points s_2,…,s_n are sorted around s_1.


When modeling a computer program,
one can use these constraints (which do not affect the output of the program)
to restrict the search space and to possibly get a speedup. 
This idea, however, is not new and was already used 
for the generation of the order type database, 
which provides a complete list of all order types of up to 11 points <cit.>.





Let S={s_1,…,s_n} 
be a point set where
s_1 is extremal and s_2,…,s_n are sorted around s_1.
Then there is a point set 
S̃={s̃_̃1̃,…,s̃_̃ñ} of the same order type as S
(in particular, s̃_̃2̃,…,s̃_̃ñ are sorted around s̃_̃1̃)
such that the points s̃_̃1̃,…,s̃_̃ñ have increasing x-coordinates.



We can apply an appropriate affine-linear transformation onto S 
so that s_1=(0,0) and x_i,y_i > 0 holds for i ≥ 2:
First we apply a translation so that s_1 lies in the origin,
then we rotate such that all points s_2,…,s_n have positive x-coordinate,
and finally we apply a shearing transformation so that s_2,…,s_n have positive y-coordinate as well.

We have that
x_i/y_i is increasing for i ≥ 2 since  s_2,…,s_n are sorted around s_1.
Since S is in general position, there is an ε > 0 such that
S and S' := {(0,ε)}∪{s_2,…,s_n} are of the same order type.  
We apply the projective transformation

to S' to obtain S̃. 
By the multilinearity of the determinant, we obtain

    [   1   1   1; x_i x_j x_k; y_i y_j y_k;     ]
    =
    y_i · y_j · y_k ·[       1       1       1; x_i/y_i x_j/y_j x_k/y_k;  -1/y_i  -1/y_j  -1/y_k;         ].

Since the points in S' have positive y-coordinates,
S' and S̃ have the same triple orientations.
Moreover, as x̃_̃ĩ=x_i'/y_i' is increasing for i ≥ 1, 
the set S̃ fulfills all desired properties.


It is worth to mention that the transformation
(x,y) ↦ (x/y,-1/y)
is the concatenation of the 
(inverse of the) 
unit paraboloid duality transformation
and
unit circle duality transformation
which – under the given conditions – 
both preserve the triple orientations
(see e.g. <cit.>).






§ SAT MODEL



In this section we describe the SAT model
that we use to prove Theorem <ref>.
The basic idea of the proof is to assume towards a contradiction
that a point set S={s_1,…,s_17} with no two disjoint 5-holes exists.
We formulate a SAT instance, where Boolean variables indicate whether 
triples are positively or negatively oriented
and clauses encode the necessary conditions introduced in Section <ref>.
Using a SAT solver we verify that the SAT instance has no solution
and conclude that the point set S does not exist.
This contradiction then completes the proof of Theorem <ref>.

It is folklore that satisfiability is -hard in general,
thus it is challenging for SAT solvers to 
terminate in reasonable time for certain SAT instances.
We now highlight the
two crucial parts of our SAT model, 
which are indeed necessary for reasonable computation times:
First, due to Lemma <ref>,
we can assume that
the points are sorted from left to right and also around the first point s_1.
Second, we teach the solver that every set of 10 consecutive points 
gives a 5-hole, that is, h(5)=10 <cit.>.
By dropping either of these two constraints 
(which only give additional information to the solver and do not affect the solution space),
none of the tested SAT solvers terminated within days.



In the following, we give a detailed description of our SAT model.
For the sake of readability, we refer to points also by their indices.
Moreover, we use the relation “a<b” simultaneously 
to indicate a larger index, a larger x-coordinate, 
and the later occurence in the cyclic order around s_1.




 §.§ A Detailed Description





  
(1) Alternating axioms

For every triple (a,b,c), we introduce the variable O_a,b,c to indicate
whether the triple (a,b,c) is positively oriented.
Since we have that

    χ_a,b,c = χ_b,c,a = χ_c,a,b = -χ_b,a,c = -χ_a,c,b = -χ_c,b,a,

we formulate clauses to assert

    O_a,b,c =
    O_b,c,a = 
    O_c,a,b≠
    O_b,a,c =
    O_a,c,b =
    O_c,b,a

by using the fact
A = B ⟺ (  A ∨ B) ∧ (  A ∨ B) ,
and
A ≠ B ⟺ ( A ∨ B) ∧ (   A ∨ B).




  
(2) Signotope Axioms

As described in Section <ref>,
for every 4-tuple a<b<c<d,
the sequence 

    χ_abc, χ_abd, χ_acd, χ_bcd

changes its sign at most once.
Formally,
to forbid other sign-patterns (that is, “-+-” and “+-+”),
we add the constraints

         O_a,b,c     ∨     
    O_a,b,d     ∨     
         O_a,c,d 
            O_a,b,c     ∨     
         O_a,b,d     ∨     
    O_a,c,d 


         O_a,b,c     ∨     
    O_a,b,d     ∨     
         O_b,c,d 
            O_a,b,c     ∨     
         O_a,b,d     ∨     
    O_b,c,d 


         O_a,b,c     ∨     
    O_a,c,d     ∨     
         O_b,c,d 
            O_a,b,c     ∨     
         O_a,c,d     ∨     
    O_b,c,d 


         O_a,b,d     ∨     
    O_a,c,d     ∨     
         O_b,c,d 
            O_a,b,d     ∨     
         O_a,c,d     ∨     
    O_b,c,d 







  
(3) Sorted around first point
 
Since the points s_1,…,s_n are sorted from left to right
and also around the first point s_1,
we have that all triples (1,a,b) are positively oriented for indices 1 < a < b.





  
(4) Bounding segments

For a 4-tuple a,b,c,d,
we introduce the auxiliary variable
E_a,b;c,d to indicate whether
the segment ab spanned by a and b 
bounds the convex hull of {a,b,c,d}.
Since the segment ab bounds ({a,b,c,d})
if and only if c and d lie on the same side of the line ab,
we add the constraints

E_a,b;c,d     ∨             O_a,b,c     ∨        O_a,b,d, 

E_a,b;c,d     ∨        O_a,b,c     ∨             O_a,b,d, 

     E_a,b;c,d     ∨             O_a,b,c     ∨             O_a,b,d, 

     E_a,b;c,d     ∨        O_a,b,c     ∨        O_a,b,d .






  
(5) 4-Gons and containments

For every 4-tuple a<b<c<d, we introduce
the auxiliary variable G^4_a,b,c,d
to indicate whether the points {a,b,c,d} form a 4-gon.
Moreover we introduce the auxiliary variable I_i;a,b,c for every 4-tuple a,b,c,i with a<b<c and a<i<c
to indicate whether the point i lies inside the triangular convex hull of {a,b,c}.

Four points a<b<c<d, sorted from left to right,
form a 4-gon if and only if 
both segments ab and cd bound ({a,b,c,d}).
Moreover, if {a,b,c,d} does not form a , 
then either b lie inside the triangular convex hull ({a,c,d}) 
or c lies inside ({a,b,d}).
Pause to note that a and d are the left- and rightmost points, respectively, 
and that not both points b and c can lie in the interior of ({a,b,c,d}).
Formally, we assert 

G^4_a,b,c,d     =          E_a,b;c,d     ∧          E_c,d;a,b,

  I_b;a,c,d     =     E_a,b;c,d     ∧          E_c,d;a,b,

  I_c;a,b,d     =          E_a,b;c,d     ∧     E_c,d;a,b.





  
(6) 3-Holes

For every triple of points a<b<c, we introduce the auxiliary variable
H^3_a,b,c to indicate whether the points {a,b,c} form a 3-hole.
Since three points a<b<c form a 3-hole if and only if 
every other point i with a<i<c lies outside the triangular convex hull ({a,b,c}),
we add the constraint

    H^3_a,b,c = ⋀_i ∈ S ∖{a,b,c} I_i;a,b,c.






  
(7) 5-Holes

For every 5-tuple X={a,b,c,d,e} with a<b<c<d<e, 
we introduce the auxiliary variable H^5_X to indicate
that the points from X form a 5-hole.
It is easy to see that the points from X form a 5-hole if and only if
every 4-tuple Y ∈X  4 forms a 4-gon
and if every triple Y ∈X  3 forms a 3-hole.
Therefore, we add the constraint

    H^5_X = 
    (
     ⋀_Y ∈X  4  G^4_Y )
    ∧(
     ⋀_Y ∈X  3  H^3_Y ).





  
(8) Forbid disjoint 5-holes

If there were two disjoint 5-holes X_1 and X_2 in our point set S,
then – as discussed in Section <ref> –
we could find two points a ∈ X_1 and b ∈ X_2
such that the line ab separates 
X_1 ∖{a} and X_2 ∖{b} (cf. Figure <ref>) – 
and this is what we have to forbid in our SAT model.
Hence, for every pair of two points a,b we introduce the variables

 
  * L_a,b to indicate that
 there exists a 5-hole X containing the point a
 that lies to the left of the directed line ab,
 that is, the triple (a,b,x) is positively oriented for every x ∈ X ∖{a}, and
 
  * R_a,b to indicate that
 there exists a 5-hole X containing the point b 
 that lies to the right of the directed line ab,
 that is, the triple (a,b,x) is negatively oriented for every x ∈ X ∖{b}.

For every 5-tuple X with a ∈ X and b ∉X we assert

    L_a,b ∨  H^5_X 
     ∨ (
     ⋁_c ∈ X ∖{a} O_a,b,c ),

and for every 5-tuple X with a ∉X and b ∈ X we assert

    R_a,b ∨  H^5_X 
     ∨ (
     ⋁_c ∈ X ∖{b} O_a,b,c ).

Now we forbid that there are 5-holes on both sides of the line ab by asserting

    L_a,b∨ R_a,b.





  
(9) Harborth's result

Harborth <cit.> has shown that every set of 10 points 
gives a 5-hole[
h(5)=10 can also be verified by slightly adapting the described SAT model],
that is, h(5)=10.
Since Harborth's result applies to each set of 10 consecutive points of S, 
we can teach the SAT solver that

 
  * for every i=1,…,8, there is a 5-hole X with X ⊂{ i,…, i+9}. 

Moreover, if there is a 5-hole X_1 in the set {1,…,7}, 
then there is another 5-hole X_2 in the set {8,…,17}.
Analogously, if there is a 5-hole X_1 in the set {11,…,17}, 
then there is another 5-hole X_2 in the set {1,…,10}.
Therefore, we can teach the SAT solver that

 
  * there is no 5-hole X with X ⊂{ 1,…, 7}, and 
 
  * there is no 5-hole X with X ⊂{11,…,17}.







We remark that the 
obtained SAT instance has 825 689 constraints in 23 392 variables,
and that the dominating parts is (8).
The source code of our python program
which creates the instance is available as supplemental data and
on our website <cit.>.





 §.§ Unsatisfiability and Verification



Having the satisfiability instance generated, we used the following command 
to create an unsatisfiability certificate:

The certificate cerated by glucose
was then verified using the proof checking tool
drat-trim by the following command:

The execution of each of the two commands (glucose and drat-trim), 
took about 2 hours and 
the certificate used about 3.1 GB of disk space.

 
We have also used picosat to prove unsatisfiability:

This command ran for about 6 hours
and created a certificate of size about 2.1 GB.
The verification of the certificate[
In our experiments, picosat wrote a comment “%RUPD32 ...” as first line in the RUP file. 
This line had to be removed manually to make the file  parsable for drat-trim.
]  using drat-trim took about 9 hours.







§ FINAL REMARKS



In (8), we have introduced the variable
L_a,b to indicate that
there exists a 5-hole X containing the point a
that lies to the left of the directed line ab.
By relaxing this to 
“…there exists a 5-hole X, possibly containing the point a, …”
and analogously for R_a,b, 
the computation time reduces by factor of roughly 2 
while the number of clauses raises by a factor of n.
The solution space, however, remains unaffected.

As pointed out by the anonymous reviewers,
the constraints
H^5_X = 
(
⋀_Y ∈X  4  G^4_Y 
)
∧ 
(
⋀_Y ∈X  3  H^3_Y 
)
from (7) are equivalent to
H^5_X = 
⋀_Y ∈X  3  H^3_Y.
Replacing (7) by this simplified expression
 further makes the auxiliary variables G^4_a,b,c,d and the first part of (5) obsolete.
However, since the described replacement 
did not show any effect on the running time of the solvers
and since we discuss g(6)=17 and the Classical Erdős–Szekeres problem below,
we decided to keep (7), (5), and the auxiliary variables G^4_a,b,c,d.







  
Multi-parametric Values:
To determine multi-parametric values such as h(5,5,5),
one can formulate a SAT instance as follows:
Three 5-holes X_1,X_2,X_3 
are pairwise disjoint if 
there is a line ℓ_ij 
for every pair X_i,X_j 
that separates X_i and X_j. 
By introducing auxiliary variables Y_i,j 
for every pair of 5-tuples X_i,Y_i 
to indicate whether X_i and X_j are disjoint 5-holes,
one can formulate an instance in Θ(n^10) variables with Θ(n^15) constraints.
However, since this formulation is quite space consuming, 
a more compact formulation might be of interest.



  
Interior-disjoint Holes:
Besides disjoint holes, also the variant of interior-disjoint holes 
has been investigated intensively by various groups of researchers
(see e.g. <cit.>).
Two holes X_1,X_2 are called interior-disjoint 
if their respective convex hulls are interior-disjoint.
Figure <ref> gives an illustration.
Interior-disjoint holes are also called compatible in literature.
Note that a pair of interior-disjoint holes can share up to two vertices.

Interior-disjoint holes also play an important role in the study of other geometric objects
such as visibility graphs (see e.g. <cit.>) or
flip graphs of triangulations on point sets (see e.g. <cit.>).
Wagner and Welzl <cit.> quite recently
developed a framework for triangulations on planar point sets
which also allows the investigation of interior-disjoint holes.
Using their tools and results it is, for example, quite easy to derive that 
10 points always give a 4-hole and a 5-hole that are interior-disjoint.
In fact, when comparing the number of researchers working on the respective problems,
the interior-disjoint holes appear to be more of interest.

In a recent article, 
Hosono and Urabe <cit.> 
summarized the current status and presented some new results.
They show that every set of 18 points contains two interior-disjoint 5-holes
and present a set of 13 points which does not contain interior-disjoint 5-holes.
By slightly adapting the SAT model from Section <ref>,
we managed to show that every set of 15 points contains two interior-disjoint 5-holes.
This bound is best possible because
the set of 14 points depicted in Figure <ref> does not contain interior-disjoint 5-holes.
Also this set was found via our framework pyotlib (cf. Section <ref>).




Table <ref> summarizes
the best possible bounds for two interior-disjoint holes <cit.>.
Again it is worth mentioning that all entries of the table (except for two interior-disjoint 5-holes)
can be verified using the order type database  <cit.>
since at most 10 points are involved in the respective arguments.
We remark that, analogously to Section <ref>, 
one could further improve the bounds for three interior-disjoint holes.



To be more specific on the changes of the SAT model for this variant: 
we slighly relaxed the contraints (8)
so that each of the two points a and b, which span a separating line ℓ, 
can be contained in holes from both sides.
The program creating the SAT instance is also available 
as supplemental data and
on our website <cit.>.






  
Classical Erdős–Szekeres:
The computation time for the 
computer assisted proof by Szekeres and Peters <cit.> for g(6)=17 
was about 1500 CPU hours.
By slightly adapting the model from Section <ref>
we have been able to confirm g(6)=17 
using glucose and drat-trim
with about one hour of computation time on a 3GHz CPU.
To be more specific with the adaption of the model from Section <ref>:


 
  * The constraints (6) are removed.
 
 
  * The constraints (7) are adapted to “(7*) 6-Gons”
 simply by testing 6-tuples instead of 5-tuples and 
 by dropping the requirement that “triples form 3-holes”.
 
 
  * The contraints (8) are removed.

Also this program is available as supplemental data and
on our website <cit.>.

An independent verification of g(6)=17 
has been done by Marić <cit.>,
who used a similar SAT framework.
While his program performs
slightly more efficient on verifying g(6)=17,
our model is more compact in size.
In fact, our program can be used to create an instance 
for testing g(7)?=33 which only requires only 1.1 GB of disk space
(which was not possible in <cit.>),
however, for determining whether g(7)=33
further ideas or more advanced SAT solvers seem to be required.
To be more precise about the differences in the two settings:
While Marić assumed that points are indexed 
with respect to their convex hull peeling depth, 
we assumed that points sorted from left-to-right 
to break the symmetries in the search-space of the SAT solver.
Hence, in our model we could axiomize point sets via signotope axioms on 4-tuples
which saves a linear factor in the size of the instance 
compared to the axiomatization via 5-tuples such as used in <cit.>
(cf. Chapters 2.1, 2.2, and 4.3 in   <cit.>).
Unfortunately, we do not see how 
Marić's assumptions on the convex hull layers
can be combined with signotope axioms.






  
Counting 5-Holes:

It is also possible to count occurences of certain substructures using SAT solvers.
For example to find point sets with as few 5-holes as possible,
we have introduced variables X_abcde;k 
indicating whether the indices 1 ≤ a<b<c<d<e ≤ n 
form the k-th 5-hole in lexicographic order.
In particular, using SAT solvers we have been able to show that 
every set of 16 points contains at least 11 5-holes 
(cf. <cit.>).






§ ACKNOWLEDGEMENTS


The author was supported by the DFG Grant FE 340/12-1 and 
by the internal research funding “Post-Doc-Funding” from Technische Universität Berlin.
We thank Stefan Felsner, Linda Kleist, Felix Schröder, Martin Balko, Adrian Dumitrescu, 
and Emo Welzl
for fruitful discussions and helpful comments.
Many thanks goes to Gyula Károlyi for communicating his construction 
for F_5(n) ≤n+1/6, 
which in fact also shows F_6(n) ≤n+1/12 (cf. Section <ref>).
Last but not least, we would also like to thank 
the anonymous reviewers for their valuable comments
which further improved the quality of this article.


alphaabbrv-url



