Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/597
DC FieldValueLanguage
dc.contributor.authorMarić, Filipen_US
dc.date.accessioned2022-08-13T15:50:04Z-
dc.date.available2022-08-13T15:50:04Z-
dc.date.issued2019-03-15-
dc.identifier.issn01687433en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/597-
dc.description.abstractA 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≥ 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≤ 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.en
dc.relation.ispartofJournal of Automated Reasoningen
dc.subjectConvex polygonsen
dc.subjectErdős–Szekeres conjectureen
dc.subjectHappy ending problemen
dc.subjectInteractive theorem provingen
dc.subjectIsabelle/HOLen
dc.subjectSAT solvingen
dc.titleFast Formal Proof of the Erdős–Szekeres Conjecture for Convex Polygons with at Most 6 Pointsen_US
dc.typeArticleen_US
dc.identifier.doi10.1007/s10817-017-9423-7-
dc.identifier.scopus2-s2.0-85028958354-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/85028958354-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage301en
dc.relation.lastpage329en
dc.relation.volume62en
dc.relation.issue3en
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeArticle-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-7219-6960-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

10
checked on Dec 24, 2024

Page view(s)

16
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.