Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

05.09.2017 | Ausgabe 3/2019

Journal of Automated Reasoning 3/2019

Fast Formal Proof of the Erdős–Szekeres Conjecture for Convex Polygons with at Most 6 Points

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 3/2019
Autor:
Filip Marić
Wichtige Hinweise
This work has been partially supported by the Grant 174021 of the Ministry of Science of Serbia.

Abstract

A conjecture originally made by Klein and Szekeres in 1932 (now commonly known as “Erdős–Szekeres” or “Happy Ending” conjecture) claims that for every \(m \ge 3\), every set of \(2^{m-2}+1\) points in a general position (none three different points are collinear) contains a convex m-gon. The conjecture has been verified for \(m \le 6\). The case \(m=6\) was solved by Szekeres and Peters and required a huge computer enumeration that took “more than 3000 GHz hours”. In this paper we improve the solution in several directions. By changing the problem representation, by employing symmetry-breaking and by using modern SAT solvers, we reduce the proving time to around only a half of an hour on an ordinary PC computer (i.e., our proof requires only around 1 GHz hour). Also, we formalize the proof within the Isabelle/HOL proof assistant, making it significantly more reliable.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Maschinenbau + Werkstoffe​​​​​​​​​​​​​​

Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Premium Partner

    Bildnachweise