pith. sign in

arxiv: 2604.20120 · v1 · submitted 2026-04-22 · 🧮 math.CO

Combinatorial Geometry of ErdH{o}s--Szekeres Type Problems: SAT/ASP Modeling and Linear Subreduction

Vitalii Koshelev , Alexey Koshka This is my paper

Pith reviewed 2026-05-10 00:41 UTC · model grok-4.3

classification 🧮 math.CO
keywords Erdős–Szekeres problembicolored pointsmonochromatic quadrilateralSAT/ASP modelinglinear subreductionsignotopesgeneral position
0
0 comments X

The pith

Any bicolored set of 26 points in general position contains an empty monochromatic quadrilateral.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a computational framework that combines SAT and ASP modeling with a linear subreduction technique to solve Erdős–Szekeres type problems involving multicolored point sets and constrained polygons. The approach builds a complete logical model of admissible configurations and linearizes the geometric inequalities by fixing abscissae, which allows a single solver run to search for realizations across all signotopes at once rather than one configuration at a time. Using this method the authors compute several new exact thresholds; the central result is the proof that h_nc(4,0;4,0) equals 26.

Core claim

By integrating the full logical model of the problem with a system of geometric inequalities and then fixing the abscissae to linearize the constraints, the authors prove that h_nc(4,0;4,0)=26: every bicolored set of 26 points in general position must contain four vertices that form an empty monochromatic quadrilateral.

What carries the argument

The linear subreduction method, which combines the complete logical model of admissible signotopes and colorings with geometric inequalities and then fixes the abscissae to produce a system of linear constraints that can be solved simultaneously for all configurations.

If this is right

  • Exact values for several other multicolored Erdős–Szekeres functions become computable by the same unified search.
  • Problems involving convex hexagons with a prescribed number of interior points and polygons whose edges satisfy color constraints are now accessible to the framework.
  • The method replaces sequential examination of individual abstract configurations with a single joint search over the entire space of signotopes.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The linearization step may be reusable for other geometric constraint problems once the combinatorial model is expressed in SAT or ASP.
  • If solver performance continues to improve, the same pipeline could settle open cases for larger numbers of points or additional colors.
  • The separation between the signotope enumeration and the linearized geometric check offers a template for hybrid combinatorial-geometric solvers beyond this specific family of problems.

Load-bearing premise

The linear subreduction correctly captures all admissible signotopes and geometric realizations without missing configurations or introducing solver errors when the abscissae are fixed.

What would settle it

A bicolored set of 26 points in general position that contains no four vertices forming an empty monochromatic quadrilateral, or an admissible signotope that the linearized solver fails to realize when a realization exists.

read the original abstract

This paper investigates several classical and novel variations of the Erd\H{o}s--Szekeres problem, including multicolored point sets, convex hexagons with a given number of interior points, and polygons with constraints on edge colors. We propose a comprehensive computational framework combining combinatorial modeling within the SAT/ASP paradigms with the geometric realization of configurations. To determine point coordinates, we developed the \textbf{linear subreduction method}. The core idea consists of combining the complete logical model of the problem with a system of geometric inequalities, followed by fixing the abscissae to linearize the constraints. This approach enables a simultaneous search for a realization across the entire space of admissible abstract configurations (signotopes) rather than examining them individually, while linearization significantly accelerates the SMT solving process. Using this framework, we established new exact values for several functions; in particular, we proved $h_{nc}(4,0; 4,0)=26$: any bicolored set of 26 points in general position must contain the vertices of an empty monochromatic quadrilateral.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a SAT/ASP modeling framework augmented by a linear subreduction technique (fixing abscissae to convert orientation predicates into linear inequalities over y-coordinates) that searches simultaneously over admissible signotopes and geometric realizations. Using this method the authors establish several new exact values for multicolored Erdős–Szekeres-type functions, most notably proving that h_nc(4,0;4,0)=26: every bicolored point set of 26 points in general position contains the vertices of an empty monochromatic quadrilateral.

Significance. If the computational encoding is complete, the result supplies the first exact determination of a nontrivial multicolored empty convex quadrilateral function, a quantity that has resisted exact evaluation by purely combinatorial or geometric arguments. The linear-subreduction approach itself constitutes a reusable technique for embedding geometric constraints inside SAT/SMT solvers and could accelerate resolution of other open Erdős–Szekeres instances.

major comments (2)
  1. [linear subreduction method (description of fixing abscissae and conversion of orientation predicates)] The manuscript provides no independent argument or certification that fixing the abscissae and linearizing the orientation predicates preserves every realizable chirotope; it is therefore unclear whether the combined logical-geometric clause set is exhaustive. This completeness question is load-bearing for the claim that no 26-point configuration avoids an empty monochromatic quadrilateral.
  2. [computational results establishing h_nc(4,0;4,0)=26] No solver certificates, timeout logs, or post-processing verification are supplied to confirm that the SMT search actually enumerated all admissible signotopes up to the 26-point threshold; without such evidence the non-existence result at 26 points rests on an unverified computational run.
minor comments (2)
  1. [Introduction] The introduction would benefit from an explicit comparison table listing previously known bounds for h_nc(k,l;m,n) alongside the new exact values.
  2. [Section 1] Notation for the multicolored functions (h_nc, etc.) is introduced only in the abstract; a formal definition should appear in the first section.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive evaluation of the significance of our results and for highlighting the need for greater clarity on the soundness of the linear subreduction technique and on the verifiability of the computational claims. We address each major comment below with additional justification and commit to revisions that make the completeness argument explicit and supply verification artifacts.

read point-by-point responses

  1. Referee: The manuscript provides no independent argument or certification that fixing the abscissae and linearizing the orientation predicates preserves every realizable chirotope; it is therefore unclear whether the combined logical-geometric clause set is exhaustive. This completeness question is load-bearing for the claim that no 26-point configuration avoids an empty monochromatic quadrilateral.

    Authors: Any realizable chirotope admits a geometric realization in general position. By a small perturbation we may assume all x-coordinates are distinct; an orientation-preserving affine transformation then maps these x-coordinates exactly to 1,2,...,n while leaving the sign of every triple orientation unchanged. With x-coordinates fixed, the orientation predicate for any triple becomes the sign of a linear form in the three y-coordinates (the standard 3x3 determinant). Consequently the SMT inequalities are necessary and sufficient for geometric realizability of that signotope. The combined SAT/ASP + SMT encoding therefore enumerates precisely the realizable signotopes. We will insert a short dedicated subsection (with the above argument) in the revised manuscript to make this completeness explicit. revision: yes

  2. Referee: No solver certificates, timeout logs, or post-processing verification are supplied to confirm that the SMT search actually enumerated all admissible signotopes up to the 26-point threshold; without such evidence the non-existence result at 26 points rests on an unverified computational run.

    Authors: We agree that independent verification strengthens the result. The 26-point instance was solved with Z3 (version 4.12.2) under a 48-hour timeout on a standard workstation; the solver returned UNSAT, confirming no satisfying assignment exists. In the revision we will (i) state the exact solver version, parameters and hardware, (ii) supply the SMT-LIB input file for the 26-point case as supplementary material, (iii) include a one-page summary of the run log showing the UNSAT outcome and resource usage, and (iv) describe the post-processing script that cross-checks the generated clauses against the combinatorial and geometric constraints. These artifacts will allow any reader to reproduce or independently verify the non-existence claim. revision: yes

Circularity Check

0 steps flagged

No circularity: result obtained by exhaustive computational search over encoded model

full rationale

The paper derives h_nc(4,0;4,0)=26 by constructing a SAT/ASP logical model of admissible signotopes, linearizing orientation constraints via fixed abscissae, and using SMT solving to confirm absence of counterexamples. This is a direct verification procedure rather than a mathematical derivation whose output is forced by redefinition or by feeding fitted values back as predictions. No equations or steps in the provided description reduce the claimed bound to an input by construction, and no load-bearing self-citation or ansatz smuggling is exhibited. The method's completeness is an external modeling assumption, not a self-referential loop.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard assumptions of general position and the soundness of SAT/SMT solvers for the encoded constraints; no free parameters, ad-hoc constants, or new postulated entities are introduced in the abstract description.

axioms (1)
  • domain assumption Points are placed in general position (no three collinear).
    Invoked to ensure all configurations are non-degenerate and to simplify the geometric inequalities.

pith-pipeline@v0.9.0 · 5494 in / 1273 out tokens · 28582 ms · 2026-05-10T00:41:10.698169+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages

  1. [1]

    Erd˝ os, G

    P. Erd˝ os, G. Szekeres,A combinatorial problem in geometry, Compositio Math., 2 (1935), 463–470

    work page 1935

  2. [2]

    Erd˝ os, G

    P. Erd˝ os, G. Szekeres,On some extremum problems in elementary geometry, Ann. Univ. Sci. Budapest E¨ otv¨ os Sect. Math., 3–4 (1961), 53–62

    work page 1961

  3. [3]

    Erd˝ os,Some more problems in elementary geometry, Austral

    P. Erd˝ os,Some more problems in elementary geometry, Austral. Math. Soc. Gaz., 5 (1978), 52–54

    work page 1978

  4. [4]

    Morris, V

    W. Morris, V. Soltan,The Erd˝ os–Szekeres problem on points in convex position, Bulletin of the Amer. Math. Soc., 37 (2000), N4, 437–458

    work page 2000

  5. [5]

    F. P. Ramsey,On a problem of formal logic, Proc. London Math. Soc. Ser. 2, 30 (1930), 264–286

    work page 1930

  6. [6]

    R. L. Graham, B. L. Rothschild, J. H. Spencer,Ramsey Theory, 2nd ed., John Wiley & Sons, NY, 1990

    work page 1990

  7. [7]

    Hall, Jr.,Combinatorial Theory, Blaisdell, Waltham, Mass

    M. Hall, Jr.,Combinatorial Theory, Blaisdell, Waltham, Mass. 1967; Mir, Moscow, 1970

    work page 1967

  8. [8]

    Devillers, F

    O. Devillers, F. Hurtado, G. K´ arolyi, C. Seara,Chromatic variants of the Erd˝ os–Szekeres theorem, Comput. Geom., 26 (2003), 193–208

    work page 2003

  9. [9]

    Szekeres, L

    G. Szekeres, L. Peters,Computer solution to the 17-point Erd˝ os–Szekeres problem, ANZIAM J., 48 (2006), 151–164

    work page 2006

  10. [10]

    Mari´ c,Fast formal proof of the Erd˝ os–Szekeres conjecture for convex polygons with at most 6 points, J

    F. Mari´ c,Fast formal proof of the Erd˝ os–Szekeres conjecture for convex polygons with at most 6 points, J. Autom. Reason., 62 (2019), 301–329

    work page 2019

  11. [11]

    Scheucher,Points, Lines, and Circles

    M. Scheucher,Points, Lines, and Circles. Some Contributions to Combinatorial Geometry, Ph.D. thesis, TU Berlin, 2020

    work page 2020

  12. [12]

    F. R. K. Chung, R. L. Graham,Forced convexn-gons in the plane, Discrete Comput. Geom., 19(3) (1998), 367–371

    work page 1998

  13. [13]

    Kleitman, L

    D. Kleitman, L. Pachter,Finding convex sets among points in the plane, Discrete Comput. Geom., 19(3) (1998), 405–410

    work page 1998

  14. [14]

    T´ oth, P

    G. T´ oth, P. Valtr,Note on the Erd˝ os–Szekeres theorem, Discrete Comput. Geom., 19(3) (1998), 457–459

    work page 1998

  15. [15]

    T´ oth, P

    G. T´ oth, P. Valtr,The Erd˝ os–Szekeres theorem: upper bounds and related results, Combinatorial and Computational Geometry, MSRI Publications, 52 (2005), 557–568

    work page 2005

  16. [16]

    Vlachos,On a conjecture of Erd˝ os and Szekeres, arXiv:1505.07549 [math.CO], 2015

    G. Vlachos,On a conjecture of Erd˝ os and Szekeres, arXiv:1505.07549 [math.CO], 2015

    work page arXiv 2015

  17. [17]

    H. N. Mojarrad, G. Vlachos,An improved upper bound for the Erd˝ os–Szekeres theorem, arXiv:1510.06255 [math.CO], 2015

    work page arXiv 2015

  18. [18]

    Norin, Y

    S. Norin, Y. Yuditsky,Erd˝ os–Szekeres without induction, Discrete Comput. Geom., 55 (2016), 963–971

    work page 2016

  19. [19]

    Suk,On the Erd˝ os–Szekeres convex polygon problem, J

    A. Suk,On the Erd˝ os–Szekeres convex polygon problem, J. Amer. Math. Soc., 30(4) (2017), 1047– 1053

    work page 2017

  20. [20]

    A. F. Holmsen, H. Mojarrad, J. Pach, G. Tardos,Two extensions of the Erd˝ os–Szekeres theorem, J. Combin. Theory Ser. A, 170 (2020), 105132

    work page 2020

  21. [21]

    Harborth,Konvexe F¨ unfecke in ebenen Punktmengen, Elem

    H. Harborth,Konvexe F¨ unfecke in ebenen Punktmengen, Elem. Math., 33 (1978), 116–118. 29

    work page 1978

  22. [22]

    Overmars, B

    M. Overmars, B. Scholten, I. Vincent,Sets without empty convex 6-gons, Bull. EATCS, 7 (1989), 160–168

    work page 1989

  23. [23]

    Overmars,Finding sets of points without empty convex 6-gons, Discrete Comput

    M. Overmars,Finding sets of points without empty convex 6-gons, Discrete Comput. Geom., 29 (2003), 153–158

    work page 2003

  24. [24]

    Nicolas,The empty hexagon theorem, Discrete Comput

    C. Nicolas,The empty hexagon theorem, Discrete Comput. Geom., 38(2) (2007), 389–397

    work page 2007

  25. [25]

    Gerken,On empty convex hexagons in planar point sets, Discrete Comput

    T. Gerken,On empty convex hexagons in planar point sets, Discrete Comput. Geom., 39 (2008), 239–272

    work page 2008

  26. [26]

    Valtr,On the empty hexagons, Manuscript, 2006

    P. Valtr,On the empty hexagons, Manuscript, 2006. URL: http://cuni.cz

    work page 2006

  27. [27]

    V. A. Koshelev,The Erd˝ os–Szekeres problem on empty hexagons in the plane, Modeling and Anal- ysis of Information Systems, 16:2 (2009), 22–74 (in Russian)

    work page 2009

  28. [28]

    M. J. H. Heule, M. Scheucher,Happy ending: An empty hexagon in every set of 30 points, arXiv:2403.00737 [math.CO], 2024

    work page arXiv 2024

  29. [29]

    Biere, K

    A. Biere, K. Fazekas, M. Fleury, N. Heisinger,CaDiCaL, Kissat, Paracooba at the SAT Competition 2020, SAT Competition (2020), 51–53

    work page 2020

  30. [30]

    Subercaseaux, W

    B. Subercaseaux, W. Nawrocki, J. Gallicchio, C. Codel, M. Carneiro, M. J. H. Heule,Formal Verification of the Empty Hexagon Number, arXiv:2403.17370 [cs.LO], 2024

    work page arXiv 2024

  31. [31]

    J. D. Horton,Sets with no empty 7-gons, Canad. Math. Bull., 26 (1983), 482–484

    work page 1983

  32. [32]

    Sendov,Compulsory configurations of points in the plane, Fundam

    Bl. Sendov,Compulsory configurations of points in the plane, Fundam. Appl. Math., 1:2 (1995), 491–516 (in Russian)

    work page 1995

  33. [33]

    Nyklova,Almost empty polygons, Studia Sci

    H. Nyklova,Almost empty polygons, Studia Sci. Math. Hungar., 40(3) (2003), 269–286

    work page 2003

  34. [34]

    V. A. Koshelev,Interior Points in the Erd˝ os–Szekeres Theorems, Math. Notes, 91:4 (2012), 542–557

    work page 2012

  35. [35]

    V. A. Koshelev,Almost empty hexagons, J. Math. Sci., 164:1 (2010), 60–81

    work page 2010

  36. [36]

    V. A. Koshelev,Computer Solution of the Almost Empty Hexagon Problem, Math. Notes, 89:3 (2011), 455–458

    work page 2011

  37. [37]

    Brass,Empty monochromatic fourgons in two-colored point sets, Geombinatorics, 14(2) (2004), 5–7

    P. Brass,Empty monochromatic fourgons in two-colored point sets, Geombinatorics, 14(2) (2004), 5–7

    work page 2004

  38. [38]

    Friedman,30 two-colored points with no empty monochromatic convex fourgons, Geombinatorics, 14(2) (2004), 53–54

    E. Friedman,30 two-colored points with no empty monochromatic convex fourgons, Geombinatorics, 14(2) (2004), 53–54

    work page 2004

  39. [39]

    Van Gulik,32 two-colored points with no empty monochromatic convex fourgons, Geombina- torics, 15(1) (2005), 32–33

    R. Van Gulik,32 two-colored points with no empty monochromatic convex fourgons, Geombina- torics, 15(1) (2005), 32–33

    work page 2005

  40. [40]

    Huemer, C

    C. Huemer, C. Seara,36 two-colored points with no empty monochromatic convex fourgons, Geom- binatorics, 19(1) (2009), 5–6

    work page 2009

  41. [41]

    Koshelev,On Erd˝ os–Szekeres problem and related problems, 2009,https://arxiv.org/abs/ 0910.2700

    V. Koshelev,On Erd˝ os–Szekeres problem and related problems, 2009,https://arxiv.org/abs/ 0910.2700

    work page arXiv 2009

  42. [42]

    D. Basu, K. Basu, B. B. Bhattacharya, S. Das,Almost empty monochromatic triangles in planar point sets, Discrete Appl. Math., 210 (2016), 207–213. 30

    work page 2016

  43. [43]

    Cravioto-Lagos, A

    J. Cravioto-Lagos, A. C. Gonz´ alez-Mart´ ınez, T. Sakai, J. Urrutia,On almost empty monochromatic triangles and convex quadrilaterals in colored point sets, Graphs Combin., 35 (2019), 1475–1493

    work page 2019

  44. [44]

    Aichholzer, T

    O. Aichholzer, T. Hackl, C. Huemer, F. Hurtado, B. Vogtenhuber,Large bichromatic point sets admit empty monochromatic 4-gons, SIAM J. Discrete Math., 23(4):2147–2155, 2010

    work page 2010

  45. [45]

    L. Liu, Y. Zhang,Almost empty monochromatic quadrilaterals in planar point sets, Math. Notes, 103:3 (2018), 415–429

    work page 2018

  46. [46]

    de Moura, N

    L. de Moura, N. Bjørner,Z3: An efficient SMT solver, Proc. TACAS (2008), 337–340

    work page 2008

  47. [47]

    Gebser, R

    M. Gebser, R. Kaminski, B. Schaub, M. Ostrowski,Clingo = ASP + Control, Technical Report, Univ. Potsdam, 2024

    work page 2024

  48. [48]

    E´ en, N

    N. E´ en, N. S¨ orensson,An extensible SAT-solver, Proc. SAT (2003), 502–518

    work page 2003

  49. [49]

    Audemard, L

    G. Audemard, L. Simon,Predicting learnt clauses quality in modern SAT solvers, Proc. IJCAI (2009), 399–404

    work page 2009

  50. [50]

    Biere,Kissat at the SAT Competition 2020, SAT Competition (2020), 54

    A. Biere,Kissat at the SAT Competition 2020, SAT Competition (2020), 54

    work page 2020

  51. [51]

    Dehnhardt,Leere konvexe Vielecke in ebenen Punktmengen, Ph.D

    H. Dehnhardt,Leere konvexe Vielecke in ebenen Punktmengen, Ph.D. Thesis, TU Braunschweig, 1987

    work page 1987

  52. [52]

    Aichholzer, F

    O. Aichholzer, F. Aurenhammer, H. Krasser,On the dual span of the order types, Discrete Comput. Geom., 28 (2002), 467–484

    work page 2002

  53. [53]

    Aichholzer,The order type database, http://tugraz.at, 2013

    O. Aichholzer,The order type database, http://tugraz.at, 2013

    work page 2013

  54. [54]

    Bialostocki, P

    A. Bialostocki, P. Dierker, B. Voxman,Some notes on the Erd˝ os–Szekeres theorem, Discrete Math- ematics, Vol. 91, No. 3, pp. 231–238, 1991

    work page 1991

  55. [55]

    Caro,On the generalized Erd˝ os–Szekeres conjecture — a new upper bound, Discrete Mathemat- ics, Vol

    Y. Caro,On the generalized Erd˝ os–Szekeres conjecture — a new upper bound, Discrete Mathemat- ics, Vol. 160, No. 1-3, pp. 229–233, 1996

    work page 1996

  56. [56]

    K´ arolyi, J

    G. K´ arolyi, J. Pach, G. T´ oth.A modular version of the Erd˝ os–Szekeres theorem, Studia Scientiarum Mathematicarum Hungarica, Vol. 38, pp. 245–259, 2001

    work page 2001

  57. [57]

    V. A. Koshelev,The Erd˝ os–Szekeres Theorem and Congruences, Math. Notes, 87:4 (2010), 537–542

    work page 2010

  58. [58]

    B´ ar´ any, G

    I. B´ ar´ any, G. K´ arolyi,Problems and results around the Erd˝ os–Szekeres theorem, Discrete and Com- putational Geometry, Japanese Conference (JCDCG 2000), Lecture Notes in Computer Science, Vol. 2098, pp. 199–205, 2001

    work page 2000

  59. [59]

    Bautista-Santiago, J

    C. Bautista-Santiago, J. Cano, R. Fabila-Monroy, C. Hidalgo Toscano, C. Huemer, J. Lea˜ nos, T. Sakai, J. Urrutia,Ramsey numbers for empty convex polygons, EuroCG. Ljubljana, Slovenia, March 16–18, 2015

    work page 2015

  60. [60]

    K´ arolyi, J

    Gy. K´ arolyi, J. Pach, G. T´ oth, P. Valtr,Ramsey-type results for geometric graphs, II, Discrete Comput. Geom. 20(3) (1998), 375–388

    work page 1998

  61. [61]

    Balko, J

    M. Balko, J. Cibulka, K. Kr´ al, J. Kynˇ cl.Ramsey numbers of ordered graphs, Electron. J. Combin., 27:P1.16, 2020. 31

    work page 2020