{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T18:17:38Z","timestamp":1769969858653,"version":"3.49.0"},"reference-count":39,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1016\/j.jsc.2025.102543","type":"journal-article","created":{"date-parts":[[2025,12,29]],"date-time":"2025-12-29T16:22:36Z","timestamp":1767025356000},"page":"102543","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Satisfiability modulo theories for verifying MILP certificates"],"prefix":"10.1016","volume":"135","author":[{"given":"Kenan","family":"Wood","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Runtian","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haoze","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hammurabi","family":"Mendes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonad","family":"Pulaj","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/j.jsc.2025.102543_br0050","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/j.orl.2008.09.006","article-title":"Certification of an optimal tsp tour through 85,900 cities","volume":"37","author":"Applegate","year":"2009","journal-title":"Oper. Res. Lett."},{"key":"10.1016\/j.jsc.2025.102543_br0060","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"415","article-title":"cvc5: a versatile and industrial-strength smt solver","author":"Barbosa","year":"2022"},{"key":"10.1016\/j.jsc.2025.102543_br0070","first-page":"107","article-title":"A brief history of linear and mixed-integer programming computation","volume":"2012","author":"Bixby","year":"2012","journal-title":"Doc. Math."},{"key":"10.1016\/j.jsc.2025.102543_br0080","series-title":"Proceedings of the First International Workshop on Intermediate Verification Languages","first-page":"53","article-title":"Why3: Shepherd your herd of provers","author":"Bobot","year":"2011"},{"key":"10.1016\/j.jsc.2025.102543_br0090","series-title":"Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings 5","first-page":"107","article-title":"Sledgehammer: judgement day","author":"B\u00f6hme","year":"2010"},{"key":"10.1016\/j.jsc.2025.102543_br0100","series-title":"SMT","first-page":"62","article-title":"Verifying models with dolmen","author":"Bury","year":"2023"},{"key":"10.1016\/j.jsc.2025.102543_br0110","series-title":"European Symposium on Programming","first-page":"148","article-title":"An automated deductive verification framework for circuit-building quantum programs","author":"Chareton","year":"2021"},{"issue":"1","key":"10.1016\/j.jsc.2025.102543_br0120","article-title":"Certificates of optimality for mixed integer linear programming using generalized subadditive generator functions","volume":"2016","author":"Cheung","year":"2016","journal-title":"Adv. Oper. Res."},{"key":"10.1016\/j.jsc.2025.102543_br0130","series-title":"Integer Programming and Combinatorial Optimization: 19th International Conference, IPCO 2017, Waterloo, ON, Canada, June 26-28, 2017, Proceedings 19","first-page":"148","article-title":"Verifying integer programming results","author":"Cheung","year":"2017"},{"key":"10.1016\/j.jsc.2025.102543_br0140","series-title":"Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"93","article-title":"The mathsat5 smt solver","author":"Cimatti","year":"2013"},{"issue":"POPL","key":"10.1016\/j.jsc.2025.102543_br0150","doi-asserted-by":"crossref","DOI":"10.1145\/3632902","article-title":"A formalization of core why3 in coq","volume":"8","author":"Cohen","year":"2024","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jsc.2025.102543_br0160","series-title":"Integer Programming and Combinatorial Optimization: 15th International Conference, IPCO 2011, New York, NY, USA, June 15-17, 2011. Proceedings 15","first-page":"104","article-title":"An exact rational mixed-integer programming solver","author":"Cook","year":"2011"},{"issue":"53","key":"10.1016\/j.jsc.2025.102543_br0170","first-page":"157","article-title":"V12. 1: user's manual for cplex","volume":"46","author":"IBM ILOG Cplex","year":"2009","journal-title":"Int. Bus. Mach. Corp."},{"key":"10.1016\/j.jsc.2025.102543_br0180","author":"da Horta"},{"key":"10.1016\/j.jsc.2025.102543_br0190","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"337","article-title":"Z3: an efficient smt solver","author":"De Moura","year":"2008"},{"key":"10.1016\/j.jsc.2025.102543_br0200","series-title":"Brazilian Symposium on Formal Methods","first-page":"23","article-title":"Satisfiability modulo theories: an appetizer","author":"De Moura","year":"2009"},{"key":"10.1016\/j.jsc.2025.102543_br0210","series-title":"Pseudo-boolean reasoning about states and transitions to certify dynamic programming and decision diagram algorithms","author":"Demirovi\u0107","year":"2024"},{"issue":"1","key":"10.1016\/j.jsc.2025.102543_br0220","doi-asserted-by":"crossref","first-page":"742","DOI":"10.1137\/23M156046X","article-title":"Safe and verified Gomory mixed-integer cuts in a rational mixed-integer program framework","volume":"34","author":"Eifler","year":"2024","journal-title":"SIAM J. Optim."},{"issue":"2","key":"10.1016\/j.jsc.2025.102543_br0230","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3485630","article-title":"A safe computational framework for integer programming applied to Chv\u00e1tal's conjecture","volume":"48","author":"Eifler","year":"2022","journal-title":"ACM Trans. Math. Softw."},{"key":"10.1016\/j.jsc.2025.102543_br0240","series-title":"Computer Ai\u00e5ded Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II 30","first-page":"126","article-title":"Smtcoq: a plug-in for integrating smt solvers into coq","author":"Ekici","year":"2017"},{"key":"10.1016\/j.jsc.2025.102543_br0020","author":"Gleixner"},{"key":"10.1016\/j.jsc.2025.102543_br0250","series-title":"An auditable constraint programming solver","author":"Gocht","year":"2022"},{"key":"10.1016\/j.jsc.2025.102543_br0260","series-title":"Gurobi Optimizer Reference Manual","author":"Gurobi Optimization, LLC","year":"2022"},{"key":"10.1016\/j.jsc.2025.102543_br0270","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","article-title":"A proof of the Kepler conjecture","author":"Hales","year":"2005","journal-title":"Ann. Math."},{"key":"10.1016\/j.jsc.2025.102543_br0280","series-title":"Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32","article-title":"Schur number five","author":"Heule","year":"2018"},{"key":"10.1016\/j.jsc.2025.102543_br0290","series-title":"International Conference on Theory and Applications of Satisfiability Testing","first-page":"228","article-title":"Solving and verifying the boolean pythagorean triples problem via cube-and-conquer","author":"Heule","year":"2016"},{"key":"10.1016\/j.jsc.2025.102543_br0300","series-title":"International Conference on Combinatorial Optimization and Applications","first-page":"681","article-title":"Integer-programming bounds on pebbling numbers of cartesian-product graphs","author":"Kenter","year":"2018"},{"key":"10.1016\/j.jsc.2025.102543_br0310","doi-asserted-by":"crossref","DOI":"10.1016\/j.ejco.2022.100031","article-title":"Progress in mathematical programming solvers from 2001 to 2020","volume":"10","author":"Koch","year":"2022","journal-title":"EURO J. Comput. Optim."},{"key":"10.1016\/j.jsc.2025.102543_br0320","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","article-title":"Computer-aided proof of Erd\u0151s discrepancy properties","volume":"224","author":"Konev","year":"2015","journal-title":"Artif. Intell."},{"key":"10.1016\/j.jsc.2025.102543_br0330","series-title":"International Conference on Mathematical Optimization Theory and Operations Research","first-page":"69","article-title":"Using integer programming to search for counterexamples: a case study","author":"Lancia","year":"2020"},{"key":"10.1016\/j.jsc.2025.102543_br0040","author":"Mendes"},{"key":"10.1016\/j.jsc.2025.102543_br0010","author":"Mohamed"},{"key":"10.1016\/j.jsc.2025.102543_br0340","series-title":"Isabelle\/HOL: a Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"issue":"322","key":"10.1016\/j.jsc.2025.102543_br0350","doi-asserted-by":"crossref","first-page":"829","DOI":"10.1090\/mcom\/3461","article-title":"Cutting planes for families implying Frankl's conjecture","volume":"89","author":"Pulaj","year":"2020","journal-title":"Math. Comput."},{"issue":"2","key":"10.1016\/j.jsc.2025.102543_br0360","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1080\/10586458.2021.1927254","article-title":"Characterizing 3-sets in union-closed families","volume":"32","author":"Pulaj","year":"2023","journal-title":"Exp. Math."},{"key":"10.1016\/j.jsc.2025.102543_br0030","author":"Pulaj"},{"key":"10.1016\/j.jsc.2025.102543_br0370","first-page":"1","article-title":"Local configurations in union-closed families","author":"Pulaj","year":"2024","journal-title":"Exp. Math."},{"key":"10.1016\/j.jsc.2025.102543_br0380","series-title":"Theory of Linear and Integer Programming","author":"Schrijver","year":"1986"},{"key":"10.1016\/j.jsc.2025.102543_br0390","series-title":"A linear programming approach to the Manickam-Miklos-Singhi conjecture","author":"Stolee","year":"2013"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717125001257?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717125001257?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T12:42:30Z","timestamp":1769604150000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717125001257"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":39,"alternative-id":["S0747717125001257"],"URL":"https:\/\/doi.org\/10.1016\/j.jsc.2025.102543","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[2026,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Satisfiability modulo theories for verifying MILP certificates","name":"articletitle","label":"Article Title"},{"value":"Journal of Symbolic Computation","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jsc.2025.102543","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2025 Published by Elsevier Ltd.","name":"copyright","label":"Copyright"}],"article-number":"102543"}}