{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,15]],"date-time":"2026-10-15T13:29:17Z","timestamp":1792070957825,"version":"4.4.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572456","type":"print"},{"value":"9783031572463","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Satisfiability solving has been used to tackle a range of long-standing open math problems in recent years. We add another success by solving a geometry problem that originated a century ago. In the 1930s, Esther Klein\u2019s exploration of unavoidable shapes in planar point sets in general position showed that every set of five points includes four points in convex position. For a long time, it was open if an empty hexagon, i.e., six points in convex position without a point inside, can be avoided. In 2006, Gerken and Nicol\u00e1s independently proved that the answer is no. We establish the exact bound: Every 30-point set in the plane in general position contains an empty hexagon. Our key contributions include an effective, compact encoding and a search-space partitioning strategy enabling linear-time speedups even when using thousands of cores.\n<\/jats:p>","DOI":"10.1007\/978-3-031-57246-3_5","type":"book-chapter","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:03:43Z","timestamp":1712153023000},"page":"61-80","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Happy Ending: An Empty Hexagon in\u00a0Every\u00a0Set\u00a0of\u00a030\u00a0Points"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1657-9796","authenticated-orcid":false,"given":"Manfred","family":"Scheucher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"key":"5_CR1","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020), http:\/\/hdl.handle.net\/10138\/318754"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336. IOS Press, second edn. (2021), https:\/\/www.iospress.com\/catalog\/books\/handbook-of-satisfiability-2","DOI":"10.3233\/FAIA336"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rner, A., Las Vergnas, M., White, N., Sturmfels, B., Ziegler, G.M.: Oriented Matroids, Encyclopedia of Mathematics and its Applications, vol.\u00a046. Cambridge University Press, 2 edn. (1999). 10\/bhb4rn","DOI":"10.1017\/CBO9780511586507"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Brakensiek, J., Heule, M.J.H., Mackey, J., Narv\u00e1ez, D.E.: The resolution of keller\u2019s conjecture. Journal of Automated Reasoning 66(3), 277\u2013300 (2022). https:\/\/doi.org\/10.1007\/S10817-022-09623-5","DOI":"10.1007\/S10817-022-09623-5"},{"key":"5_CR5","unstructured":"Buss, S., Thapen, N.: DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science 17(2) (2021). 10\/mbdx"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201\u2013215 (1960). 10\/bw9h55","DOI":"10.1145\/321033.321034"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Theory and Applications of Satisfiability Testing. pp. 502\u2013518. Springer (2004)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"5_CR8","unstructured":"Erd\u0151s, P., Szekeres, G.: A combinatorial problem in geometry. Compositio Mathematica 2, 463\u2013470 (1935), http:\/\/www.renyi.hu\/~p_erdos\/1935-01.pdf"},{"key":"5_CR9","unstructured":"Erd\u0151s, P., Szekeres, G.: On some extremum problems in elementary geometry. Annales Universitatis Scientiarium Budapestinensis de Rolando E\u00f6tv\u00f6s Nominatae, Sectio Mathematica 3\u20134, 53\u201363 (1960), https:\/\/www.renyi.hu\/~p_erdos\/1960-09.pdf"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Felsner, S., Weil, H.: Sweeps, arrangements and signotopes. Discrete Applied Mathematics 109(1), 67\u201394 (2001). 10\/dc4tb4","DOI":"10.1016\/S0166-218X(00)00232-8"},{"key":"5_CR11","unstructured":"Gent, I.P.: Arc consistency in SAT. In: European Conference on Artificial Intelligence (ECAI 2002). FAIA, vol.\u00a077, pp. 121\u2013125. IOS Press (2002), https:\/\/frontiersinai.com\/ecai\/ecai2002\/pdf\/p0121.pdf"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Gerken, T.: Empty Convex Hexagons in Planar Point Sets. Discrete & Computational Geometry 39(1), 239\u2013272 (2008). 10\/c4kn3s","DOI":"10.1007\/s00454-007-9018-x"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Haberlandt, A., Green, H., Heule, M.J.H.: Effective Auxiliary Variables via Structured Reencoding. In: International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0271, pp. 11:1\u201311:19. Dagstuhl, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.11","DOI":"10.4230\/LIPIcs.SAT.2023.11"},{"key":"5_CR14","unstructured":"Harborth, H.: Konvexe F\u00fcnfecke in ebenen Punktmengen. Elemente der Mathematik 33, 116\u2013118 (1978), http:\/\/www.digizeitschriften.de\/dms\/img\/?PID=GDZPPN002079801"},{"key":"5_CR15","unstructured":"Heule, M.J.H.: The DRAT format and DRAT-trim checker (2016), arXiv:1610.06229"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence. AAAI\u201918, AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Theory and Applications of Satisfiability Testing (SAT 2016). LNCS, vol.\u00a09710, pp. 228\u2013245. Springer (2016). 10\/gkkscn","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In: Hardware and Software: Verification and Testing. pp. 50\u201365. Springer (2012). 10\/f3ss29","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"5_CR19","unstructured":"Heule, M.J.H., Scheucher, M.: Happy Ending: An Empty Hexagon in Every Set of 30 Points (Extended Version) (2024), https:\/\/arxiv.org\/abs\/2403.00737"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Holmsen, A.F., Mojarrad, H.N., Pach, J., Tardos, G.: Two extensions of the Erd\u0151s\u2013Szekeres problem. Journal of the European Mathematical Society pp. 3981\u20133995 (2020). 10\/gsjw4m","DOI":"10.4171\/jems\/1000"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Horton, J.: Sets with no empty convex $$7$$-gons. Canadian Mathematical Bulletin 26, 482\u2013484 (1983). 10\/chf6dk","DOI":"10.4153\/CMB-1983-077-8"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 129\u2013144. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"5_CR23","unstructured":"Kalbfleisch, J., Kalbfleisch, J., Stanton, R.: A combinatorial problem on convex regions. In: Proc. Louisiana Conf. Combinatorics, Graph Theory and Computing, Congressus Numerantium, vol. 1, Baton Rouge, La.: Louisiana State Univ. pp. 180\u2013188 (1970)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Knuth, D.E.: Axioms and Hulls, LNCS, vol.\u00a0606. Springer (1992). 10\/bwfnz9","DOI":"10.1007\/3-540-55611-7"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Mari\u0107, F.: Fast formal proof of the Erd\u0151s\u2013Szekeres conjecture for convex polygons with at most 6 points. Journal of Automated Reasoning 62, 301\u2013329 (2019). 10\/gsjw4r","DOI":"10.1007\/s10817-017-9423-7"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Nicol\u00e1s, M.C.: The Empty Hexagon Theorem. Discrete & Computational Geometry 38(2), 389\u2013397 (2007). 10\/bw3hnd","DOI":"10.1007\/s00454-007-1343-6"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Overmars, M.: Finding Sets of Points without Empty Convex 6-Gons. Discrete & Computational Geometry 29(1), 153\u2013158 (2002). 10\/cnqmr4","DOI":"10.1007\/s00454-002-2829-x"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Scheucher, M.: Two disjoint 5-holes in point sets. Computational Geometry 91, 101670 (2020). 10\/gsjw2z","DOI":"10.1016\/j.comgeo.2020.101670"},{"key":"5_CR29","unstructured":"Scheucher, M.: A SAT Attack on Erd\u0151s\u2013Szekeres Numbers in $$\\mathbb{R}^d$$ and the Empty Hexagon Theorem. Computing in Geometry and Topology 2(1), 2:1\u20132:13 (2023). 10\/gsjw22"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Suk, A.: On the Erd\u0151s\u2013Szekeres convex polygon problem. Journal of the AMS 30, 1047\u20131053 (2017). 10\/gsjw44","DOI":"10.1090\/jams\/869"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Szekeres, G., Peters, L.: Computer solution to the 17-point Erd\u0151s\u2013Szekeres problem. Australia and New Zealand Industrial and Applied Mathematics 48(2), 151\u2013164 (2006). 10\/dkb9j3","DOI":"10.1017\/S144618110000300X"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: Verified propagation redundancy and compositional UNSAT checking in cakeml. International Journal on Software Tools for Technology 25(2), 167\u2013184 (2023). 10\/grw7wm","DOI":"10.1007\/s10009-022-00690-y"},{"key":"5_CR33","unstructured":"T\u00f3th, G., Valtr, P.: The Erd\u0151s\u2013Szekeres theorem: Upper Bounds and Related Results. In: Combinatorial and Computational Geometry. vol.\u00a052, pp. 557\u2013568. MSRI Publications, Cambridge Univ. Press (2005), http:\/\/www.ams.org\/mathscinet-getitem?mr=2178339"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Wieringa, S., Niemenmaa, M., Heljanko, K.: Tarmo: A framework for parallelized bounded model checking. In: International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2009. EPTCS, vol.\u00a014, pp. 62\u201376 (2009). https:\/\/doi.org\/10.4204\/EPTCS.14.5","DOI":"10.4204\/EPTCS.14.5"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57246-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:05:32Z","timestamp":1712153132000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57246-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572456","9783031572463"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57246-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}