Document Open Access Logo

From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc

Authors Philipp Danzinger , Nysret Musliu

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.17.pdf
  • Filesize: 0.86 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Software and its engineering → Formal software verification
Keywords
  • Redundant constraints
  • constraint programming
  • MiniZinc
  • formal verification
  • Lean 4
  • large language models
  • automated theorem proving

Metrics

Abstract

The performance of constraint models strongly depends on the formulation used. Redundant constraints, which are logically implied by the model, can strengthen propagation and speed up solving, but finding effective ones requires substantial expertise. Recent work has shown that Large Language Models (LLMs) can generate performance-improving constraints for MiniZinc models. However, such approaches offer no soundness guarantees and the generated constraints may exclude optimal solutions or render instances infeasible.
We present a pipeline that combines LLM-based constraint generation with empirical evaluation and formal verification. At its core is a novel formalization of a supported MiniZinc subset for verifying redundancy of a constraint schema over all instances by translating MiniZinc models to Lean 4 theorems. We handle MiniZinc’s partial semantics by requiring the base model to be safe and separately proving that the proposed constraint is well-defined for all instances and solutions of the base model.
We evaluate the approach on three constraint optimization problems from the literature, starting from published expert-crafted models. The augmented models show a clear improvement on one problem, improved MiniZinc Challenge scores with metric trade-offs on another, and small but non-significant changes on the third.

Cite As Get BibTex

Philipp Danzinger and Nysret Musliu. From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.17

Author Details

Philipp Danzinger
  • Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Vienna, Austria
Nysret Musliu
  • Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Vienna, Austria

Funding

This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/COE12

Supplementary Materials

References

  1. Ozgur Akgun, Ian Miguel, Chris Jefferson, Alan Frisch, and Brahim Hnich. Extensible automated constraint modelling. Proceedings of the AAAI Conference on Artificial Intelligence, 25(1):4-11, August 2011. URL: https://doi.org/10.1609/aaai.v25i1.7820.
  2. Bernardo F. Almeida, Isabel Correia, and Francisco Saldanha da Gama. Priority-based heuristics for the multi-skill resource constrained project scheduling problem. Expert Systems with Applications, 57:91-103, 2016. URL: https://doi.org/10.1016/j.eswa.2016.03.017.
  3. Christian Bessiere, Emmanuel Hebrard, George Katsirelos, Zeynep Kiziltan, Nina Narodytska, and Toby Walsh. Reasoning about constraint models. In Duc-Nghia Pham and Seong-Bae Park, editors, PRICAI 2014: Trends in Artificial Intelligence, pages 795-808, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-13560-1_63.
  4. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning, 51(1):109-128, 2013. URL: https://doi.org/10.1007/s10817-013-9278-5.
  5. John Charnley, Simon Colton, and Ian Miguel. Automatic generation of implied constraints. In Proceedings of the 2006 Conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 - September 1, 2006, Riva Del Garda, Italy, pages 73-77, NLD, 2006. IOS Press. URL: http://www.booksonline.iospress.nl/Content/View.aspx?piid=1649.
  6. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, and Thomas Hanwen Zhu. Seed-prover: Deep and broad reasoning for automated theorem proving, 2025. URL: https://doi.org/10.48550/arXiv.2507.23726.
  7. Philipp Danzinger and Nysret Musliu. From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc (Software Artifact). Software, This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/COE12, (visited on 2026-06-30). URL: https://github.com/pdanzinger/cp2026-minizinc-lean/releases/tag/cp2026-artifact
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26941
  8. Alan M. Frisch, Warwick Harvey, Chris Jefferson, Bernadette Martínez-Hernández, and Ian Miguel. Essence: A constraint language for specifying combinatorial problems. Constraints, 13(3):268-306, 2008. URL: https://doi.org/10.1007/s10601-008-9047-y.
  9. Alan M. Frisch, Ian Miguel, and Toby Walsh. Cgrass: a system for transforming constraint satisfaction problems. In Proceedings of the 2002 Joint ERCIM/CologNet International Conference on Constraint Solving and Constraint Logic Programming, ERCIM'02/CologNet'02, pages 15-30, Berlin, Heidelberg, 2002. Springer-Verlag. URL: https://doi.org/10.1007/3-540-36607-5_2.
  10. Alan M.Frisch and Peter J.Stuckey. The proper treatment of undefinedness in constraint languages. In Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pages 367-382, Switzerland, 2009. Springer. International Conference on Principles and Practice of Constraint Programming 2009, CP 2009 ; Conference date: 22-09-2009 Through 24-09-2009. URL: https://doi.org/10.1007/978-3-642-04244-7_30.
  11. Carla Gomes and Meinolf Sellmann. Streamlined constraint reasoning. In Mark Wallace, editor, Principles and Practice of Constraint Programming - CP 2004, pages 274-289, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-30201-8_22.
  12. Marie-Louise Lackner, Christoph Mrkvicka, Nysret Musliu, Daniel Walkiewicz, and Felix Winter. Benchmark instances and models for the oven scheduling problem. Zenodo, December 2022. Dataset. URL: https://doi.org/10.5281/zenodo.7456938.
  13. Marie-Louise Lackner, Christoph Mrkvicka, Nysret Musliu, Daniel Walkiewicz, and Felix Winter. Exact methods for the Oven Scheduling Problem. Constraints, 28(2):320-361, 2023. URL: https://doi.org/10.1007/s10601-023-09347-2.
  14. Edward Lam, Graeme Gange, Peter J. Stuckey, Pascal Van Hentenryck, and Jip J. Dekker. Nutmeg: a MIP and CP hybrid solver using branch-and-check. SN Operations Research Forum, 1(3):22, 2020. URL: https://doi.org/10.1007/s43069-020-00023-2.
  15. Edward Lam and Pascal Van Hentenryck. A branch-and-price-and-check model for the vehicle routing problem with location congestion. Constraints, 21(3):394-412, 2016. URL: https://doi.org/10.1007/s10601-016-9241-2.
  16. Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 253-266, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575671.
  17. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: A frontier model for open-source automated theorem proving, 2025. URL: https://doi.org/10.48550/arXiv.2502.07640.
  18. Fei Liu, Tong Xialiang, Mingxuan Yuan, Xi Lin, Fu Luo, Zhenkun Wang, Zhichao Lu, and Qingfu Zhang. Evolution of heuristics: Towards efficient automatic algorithm design using large language model. In Ruslan Salakhutdinov, Zico Kolter, Katherine Heller, Adrian Weller, Nuria Oliver, Jonathan Scarlett, and Felix Berkenkamp, editors, Proceedings of the 41st International Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research, pages 32201-32223. PMLR, 21-27 July 2024. URL: https://proceedings.mlr.press/v235/liu24bs.html.
  19. Kostis Michailidis, Dimos Tsouros, and Tias Guns. Constraint Modelling with LLMs Using In-Context Learning. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024), volume 307 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:27, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2024.20.
  20. Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett. lean-smt: An smt tactic for discharging proof goals in lean. In Ruzica Piskac and Zvonimir Rakamarić, editors, Computer Aided Verification, pages 197-212, Cham, 2025. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-98682-6_11.
  21. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction - CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, pages 625-635, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  22. Emmanuel Néron. Lower bounds for the multi-skill project scheduling problem. In Proceedings of the 8th International Workshop on Project Management and Scheduling (PMS 2002), pages 274-277, Valencia, Spain, 2002. Google Scholar
  23. Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. Minizinc: towards a standard cp modelling language. In Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming, CP'07, pages 529-543, Berlin, Heidelberg, 2007. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-74970-7_38.
  24. Peter Nightingale, Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Patrick Spracklen. Automatically improving constraint models in savile row. Artificial Intelligence, 251:35-61, 2017. URL: https://doi.org/10.1016/j.artint.2017.07.001.
  25. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  26. Alexander Novikov, Ngân Vũ, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. Alphaevolve: A coding agent for scientific and algorithmic discovery, 2025. URL: https://doi.org/10.48550/arXiv.2506.13131.
  27. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025. URL: https://doi.org/10.48550/arXiv.2504.21801.
  28. Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with large language models. Nature, 625(7995):468-475, January 2024. URL: https://doi.org/10.1038/s41586-023-06924-6.
  29. Weichun Shi, Minghao Liu, Wanting Zhang, Langchen Shi, Fuqi Jia, Feifei Ma, and Jian Zhang. ConstraintLLM: A neuro-symbolic framework for industrial-level constraint programming. In Christos Christodoulopoulos, Tanmoy Chakraborty, Carolyn Rose, and Violet Peng, editors, Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pages 15999-16019, Suzhou, China, 2025. Association for Computational Linguistics. URL: https://doi.org/10.18653/v1/2025.emnlp-main.809.
  30. Barbara M. Smith. Modelling. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, Handbook of Constraint Programming, volume 2 of Foundations of Artificial Intelligence, chapter 11, pages 377-406. Elsevier, 2006. URL: https://doi.org/10.1016/S1574-6526(06)80013-1.
  31. Yuliang Song and Eldan Cohen. Do llms understand constraint programming? zero-shot constraint programming model generation using llms. In Learning and Intelligent Optimization: 19th International Conference, LION 19, Prague, Czech Republic, June 15–19, 2025, Proceedings, Part I, pages 16-31, Berlin, Heidelberg, 2026. Springer-Verlag. URL: https://doi.org/10.1007/978-3-032-09156-7_2.
  32. Patrick Spracklen, Nguyen Dang, Özgür Akgün, and Ian Miguel. Towards portfolios of streamlined constraint models: A case study with the balanced academic curriculum problem, 2020. URL: https://arxiv.org/abs/2009.10152.
  33. Patrick Spracklen, Nguyen Dang, Özgür Akgün, and Ian Miguel. Automated streamliner portfolios for constraint satisfaction problems. Artificial Intelligence, 319:103915, 2023. URL: https://doi.org/10.1016/j.artint.2023.103915.
  34. Niki van Stein and Thomas Bäck. Llamea: A large language model evolutionary algorithm for automatically generating metaheuristics. IEEE Transactions on Evolutionary Computation, 29(2):331-345, 2025. URL: https://doi.org/10.1109/TEVC.2024.3497793.
  35. Peter J. Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer. The minizinc challenge 2008–2013. AI Magazine, 35(2):55-60, 2014. URL: https://doi.org/10.1609/aimag.v35i2.2539.
  36. Peter J. Stuckey, Kim Marriott, and Guido Tack. The MiniZinc Handbook. Monash University, 2026. Version 2.9.4. URL: https://docs.minizinc.dev/en/2.9.4/index.html.
  37. The Rocq Development Team. The rocq prover (version 9.0), April 2025. URL: https://doi.org/10.5281/zenodo.15149629.
  38. Dimos Tsouros, Hélène Verhaeghe, Serdar Kadıoğlu, and Tias Guns. Holy grail 2.0: From natural language to constraint models, 2023. URL: https://doi.org/10.48550/arXiv.2308.01589.
  39. Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, and Stefan Szeider. Generating streamlining constraints with large language models. Journal of Artificial Intelligence Research, 84:16:1-16:20, October 2025. URL: https://doi.org/10.1613/jair.1.18965.
  40. Milad Yazdani, Mahdi Mostajabdaveh, Samin Aref, and Zirui Zhou. Evocut: Strengthening integer programs via evolution-guided language models. arXiv preprint arXiv:2508.11850, 2025. URL: https://doi.org/10.48550/arXiv.2508.11850.
  41. Kenneth D. Young, Thibaut Feydy, and Andreas Schutt. Constraint programming applied to the multi-skill project scheduling problem. In J. Christopher Beck, editor, Principles and Practice of Constraint Programming, pages 308-317, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-66158-2_20.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact