{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:26:18Z","timestamp":1767831978520,"version":"3.49.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,5,26]],"date-time":"2022-05-26T00:00:00Z","timestamp":1653523200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"German Federal Ministry of Education and Research","award":["05M14ZAM, 05M20ZBM"],"award-info":[{"award-number":["05M14ZAM, 05M20ZBM"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Math. Softw."],"published-print":{"date-parts":[[2022,6,30]]},"abstract":"<jats:p>We describe a general and safe computational framework that provides integer programming results with the degree of certainty that is required for machine-assisted proofs of mathematical theorems. At its core, the framework relies on a rational branch-and-bound certificate produced by an exact integer programming solver, SCIP, in order to circumvent floating-point round-off errors present in most state-of-the-art solvers for mixed-integer programs. The resulting certificates are self-contained and checker software exists that can verify their correctness independently of the integer programming solver used to produce the certificate. This acts as a safeguard against programming errors that may be present in complex solver software. The viability of this approach is tested by applying it to finite cases of Chv\u00e1tal\u2019s conjecture, a long-standing open question in extremal combinatorics. We take particular care to verify also the correctness of the input for this specific problem, using the Coq formal proof assistant. As a result, we are able to provide the first machine-assisted proof that Chv\u00e1tal\u2019s conjecture holds for all downsets whose union of sets contains seven elements or less.<\/jats:p>","DOI":"10.1145\/3485630","type":"journal-article","created":{"date-parts":[[2022,3,4]],"date-time":"2022-03-04T22:28:24Z","timestamp":1646432904000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A Safe Computational Framework for Integer Programming Applied to Chv\u00e1tal\u2019s Conjecture"],"prefix":"10.1145","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0245-9344","authenticated-orcid":false,"given":"Leon","family":"Eifler","sequence":"first","affiliation":[{"name":"Zuse Institute Berlin (ZIB), Berlin, Germany"}]},{"given":"Ambros","family":"Gleixner","sequence":"additional","affiliation":[{"name":"HTW Berlin and Zuse Institute Berlin (ZIB), Berlin, Germany"}]},{"given":"Jonad","family":"Pulaj","sequence":"additional","affiliation":[{"name":"Davidson College and Zuse Institute Berlin (ZIB), Davidson, NC, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,5,26]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38189-8_18"},{"key":"e_1_3_1_3_2","volume-title":"Combinatorics of Finite Sets","author":"Anderson Ian","year":"2002","unstructured":"Ian Anderson. 2002. Combinatorics of Finite Sets. Courier Corporation."},{"key":"e_1_3_1_4_2","unstructured":"David Applegate Ribert Bixby Vasek Chvatal and William Cook. 2006. The traveling salesman problem: A Computational Study. Princeton University Press Princeton \u00b7 Zbl 1130.90036."},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2006.12.010"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s12532-016-0104-z"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0894-0347-07-00589-9"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_1_9_2","first-page":"35","volume-title":"Proceedings of the 5th British Combinatorial Conference (Univ. Aberdeen, Aberdeen)","author":"Berge Claude","year":"1976","unstructured":"Claude Berge. 1976. A theorem related to the Chv\u00e1tal conjecture. In Proceedings of the 5th British Combinatorial Conference (Univ. Aberdeen, Aberdeen). Congressus Numerantium, No. XV, Utilitas Math., Winnipeg, Man., 35\u201340."},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejc.2010.07.002"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59250-3_13"},{"key":"e_1_3_1_12_2","article-title":"A conjecture in extremal combinatorics","author":"Chv\u00e1tal Va\u0161ek","unstructured":"Va\u0161ek Chv\u00e1tal. [n.d.]. A conjecture in extremal combinatorics. Retrieved September 18, 2020 from http:\/\/users.encs.concordia.ca\/ chvatal\/conjecture.html.","journal-title":"http:\/\/users.encs.concordia.ca\/ chvatal\/conjecture.html."},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BFb0066179","volume-title":"Hypergraph Seminar","author":"Chv\u00e1tal Va\u0161ek","year":"1974","unstructured":"Va\u0161ek Chv\u00e1tal. 1974. Intersecting families of edges in hypergraphs having the hereditary property. In Hypergraph Seminar. Springer, 61\u201366."},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s12532-013-0055-6"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.1219885"},{"key":"e_1_3_1_16_2","unstructured":"Eva Czabarka Glenn Hurlbert and Vikram Kamat. 2017. Chv\u00e1atal\u2019s conjecture for downsets of small rank. arxiv:math.CO\/1703.00494."},{"key":"e_1_3_1_17_2","article-title":"Integer programming proofs for Chv\u00e1tal\u2019s conjecture over finite ground sets","author":"Eifler Leon","unstructured":"Leon Eifler. [n.d.]. Integer programming proofs for Chv\u00e1tal\u2019s conjecture over finite ground sets. Retrieved September 9, 2020 from https:\/\/github.com\/leoneifler\/chvatalip.","journal-title":"https:\/\/github.com\/leoneifler\/chvatalip."},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579174"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1137\/1030133"},{"key":"e_1_3_1_20_2","volume-title":"The SCIP Optimization Suite 6.0","author":"Gleixner Ambros","year":"2018","unstructured":"Ambros Gleixner, Michael Bastubbe, Leon Eifler, Tristan Gally, Gerald Gamrath, Robert Lion Gottwald, Gregor Hendel, Christopher Hojny, Thorsten Koch, Marco E. L\u00fcbbecke, Stephen J. Maher, Matthias Miltenberger, Benjamin M\u00fcller, Marc E. Pfetsch, Christian Puchert, Daniel Rehfeldt, Franziska Schl\u00f6sser, Christoph Schubert, Felipe Serrano, Yuji Shinano, Jan Merlin Viernickel, Matthias Walter, Fabian Wegscheider, Jonas T. Witt, and Jakob Witzig. 2018. The SCIP Optimization Suite 6.0. Technical Report 18\u201326. ZIB, Takustr. 7, 14195 Berlin."},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","first-page":"681","DOI":"10.1007\/978-3-030-04651-4_46","volume-title":"Combinatorial Optimization and Applications","author":"Kenter Franklin","year":"2018","unstructured":"Franklin Kenter and Daphne Skipper. 2018. Integer-programming bounds on pebbling numbers of Cartesian-product graphs. In Combinatorial Optimization and Applications, Donghyun Kim, R. N. Uma, and Alexander Zelikovsky (Eds.). Springer International Publishing, Cham, 681\u2013695."},{"key":"e_1_3_1_24_2","article-title":"On the number of latent subsets of intersecting collections","author":"Kleitman Daniel J.","year":"1972","unstructured":"Daniel J. Kleitman and Thomas L. Magnanti. 1972. On the number of latent subsets of intersecting collections. Operations Research Center Working Papers (1972). http:\/\/hdl.handle.net\/1721.1\/5343.","journal-title":"Operations Research Center Working Papers"},{"key":"e_1_3_1_25_2","volume-title":"Rapid Mathematical Prototyping","author":"Koch Thorsten","year":"2004","unstructured":"Thorsten Koch. 2004. Rapid Mathematical Prototyping. Ph.D. Dissertation. Technische Universit\u00e4t Berlin."},{"key":"e_1_3_1_26_2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-3-030-49988-4_5","volume-title":"Mathematical Optimization Theory and Operations Research","author":"Lancia Giuseppe","year":"2020","unstructured":"Giuseppe Lancia, Eleonora Pippia, and Franca Rinaldi. 2020. Using integer programming to search for counterexamples: A case study. In Mathematical Optimization Theory and Operations Research, Alexander Kononov, Michael Khachay, Valery A. Kalyagin, and Panos Pardalos (Eds.). Springer International Publishing, Cham, 69\u201384."},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(84)90135-3"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2019.04.011"},{"key":"e_1_3_1_29_2","volume-title":"Cutting Planes for Union-Closed Families","author":"Pulaj Jonad","year":"2017","unstructured":"Jonad Pulaj. 2017. Cutting Planes for Union-Closed Families. Ph.D. Dissertation. Technische Universit\u00e4t Berlin."},{"key":"e_1_3_1_30_2","first-page":"537","volume-title":"Proceedings of the 5th British Combinatorial Conference (Univ. Aberdeen, Aberdeen, 1975)","author":"Sch\u00f6nheim Jochanan","year":"1975","unstructured":"Jochanan Sch\u00f6nheim. 1975. Hereditary systems and Chv\u00e1tal\u2019s conjecture. In Proceedings of the 5th British Combinatorial Conference (Univ. Aberdeen, Aberdeen, 1975). 537\u2013539."},{"key":"e_1_3_1_31_2","article-title":"Variations on Chv\u00e1tal\u2019s Conjecture (2009)","author":"Snevily Hunter","unstructured":"Hunter Snevily. [n.d.]. Variations on Chv\u00e1tal\u2019s Conjecture (2009). Retrieved September 1, 2020 from https:\/\/faculty.math.illinois.edu\/ west\/regs\/chvatal.html.","journal-title":"https:\/\/faculty.math.illinois.edu\/ west\/regs\/chvatal.html."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(83)90025-0"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066190"},{"key":"e_1_3_1_34_2","first-page":"422","volume-title":"Theory and Applications of Satisfiability Testing (SAT\u201914)","author":"Wetzler Nathan","year":"2014","unstructured":"Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. 2014. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing (SAT\u201914), Carsten Sinz and Uwe Egly (Eds.). Springer International Publishing, Cham, 422\u2013429."}],"container-title":["ACM Transactions on Mathematical Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485630","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485630","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485630"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,26]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,6,30]]}},"alternative-id":["10.1145\/3485630"],"URL":"https:\/\/doi.org\/10.1145\/3485630","relation":{},"ISSN":["0098-3500","1557-7295"],"issn-type":[{"value":"0098-3500","type":"print"},{"value":"1557-7295","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,26]]},"assertion":[{"value":"2020-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-05-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}