Document Open Access Logo

An Expansion-Based Approach for Quantified Integer Programming

Authors Michael Hartisch , Leroy Chew

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.12.pdf
  • Filesize: 1.03 MB
  • 26 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.12.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Discrete mathematics
  • Mathematics of computing → Solvers
  • Theory of computation → Discrete optimization
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Algorithm design techniques
  • Applied computing → Operations research
  • Theory of computation → Abstraction
Keywords
  • Quantified Integer Programming
  • Quantified Constraint Satisfaction
  • Robust Discrete Optimization
  • Expansion
  • CEGAR

Metrics

Abstract

Quantified Integer Programming (QIP) bridges multiple domains by extending Quantified Boolean Formulas (QBF) to incorporate general integer variables and linear constraints while also generalizing Integer Programming through variable quantification. As a special case of Quantified Constraint Satisfaction Problems (QCSP), QIP provides a versatile framework for addressing complex decision-making scenarios. Additionally, the inclusion of a linear objective function enables QIP to effectively model multistage robust discrete linear optimization problems, making it a powerful tool for tackling uncertainty in optimization.
While two primary solution paradigms exist for QBF - search-based and expansion-based approaches - only search-based methods have been explored for QIP and QCSP. We introduce an expansion-based approach for QIP using Counterexample-Guided Abstraction Refinement (CEGAR), adapting techniques from QBF. We extend this methodology to tackle multistage robust discrete optimization problems with linear constraints and further embed it in an optimization framework, enhancing its applicability. Our experimental results highlight the advantages of this approach, demonstrating superior performance over existing search-based solvers for QIP in specific instances. Furthermore, the ability to model problems using linear constraints enables notable performance gains over state-of-the-art expansion-based solvers for QBF.

Cite As Get BibTex

Michael Hartisch and Leroy Chew. An Expansion-Based Approach for Quantified Integer Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 12:1-12:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.12

Author Details

Michael Hartisch
  • University of Passau, Germany
  • FAU Erlangen-Nürnberg, Germany
Leroy Chew
  • TU Wien, Austria

Funding

Furthermore, we acknowledge that this research was partially funded by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 534441421 and Austrian Science Fund FWF Project ESP197.
  • Hartisch, Michael: Partially funded by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 534441421.
  • Chew, Leroy: funded by Austrian Science Fund FWF Project ESP197.

Acknowledgements

We thank the three anonymous reviewers for their helpful comments.

Supplementary Materials

References

  1. Andrea Baggio, Margarida Carvalho, Andrea Lodi, and Andrea Tramontani. Multilevel approaches for the critical node problem. Operations Research, 69(2):486-508, 2021. URL: https://doi.org/10.1287/opre.2020.2014.
  2. Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett. Extending SMT solvers to higher-order logic. In Automated Deduction-CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings 27, pages 35-54. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_3.
  3. Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. Handbook of model checking, pages 305-343, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_11.
  4. Marco Benedetti, Arnaud Lallouet, and Jérémie Vautard. Quantified constraint optimization. In International Conference on Principles and Practice of Constraint Programming, pages 463-477. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85958-1_31.
  5. Dimitris Bertsimas and Iain Dunning. Multistage robust mixed-integer optimization with adaptive partitions. Operations Research, 64(4):980-998, 2016. URL: https://doi.org/10.1287/opre.2016.1515.
  6. Dimitris Bertsimas and Angelos Georghiou. Binary decision rules for multistage adaptive mixed-integer optimization. Mathematical Programming, 167:395-433, 2018. URL: https://doi.org/10.1007/s10107-017-1135-6.
  7. Dimitris Bertsimas and Melvyn Sim. Robust discrete optimization and network flows. Mathematical programming, 98(1):49-71, 2003. URL: https://doi.org/10.1007/s10107-003-0396-4.
  8. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. In James R. Lee, editor, 12th Innovations in Theoretical Computer Science Conference, ITCS 2021, January 6-8, 2021, Virtual Conference, volume 185 of LIPIcs, pages 12:1-12:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITCS.2021.12.
  9. Olaf Beyersdorff, Leroy Chew, Judith Clymo, and Meena Mahajan. Short proofs in QBF expansion. In Theory and Applications of Satisfiability Testing-SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings 22, pages 19-35. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_2.
  10. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory, 11(4):26:1-26:42, 2019. URL: https://doi.org/10.1145/3352155.
  11. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  12. Nikolaj Bjørner, Mikolás Janota, and William Klieber. On conflicts and strategies in QBF. In LPAR (short papers), pages 28-41, 2015. URL: https://doi.org/10.29007/4sk1.
  13. Nikolaj S Bjørner and Mikolás Janota. Playing with quantified satisfaction. LPAR (short papers), 35:15-27, 2015. URL: https://doi.org/10.29007/vv21.
  14. Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF resolution: Further insights. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 4:1-4:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.4.
  15. Hubie Chen. Beyond Q-resolution and prenex form: A proof system for quantified constraint satisfaction. Logical Methods in Computer Science, 10, 2014. URL: https://doi.org/10.2168/LMCS-10(4:14)2014.
  16. Hubie Chen and Martin Pál. Optimization, games, and quantified constraint satisfaction. In International Symposium on Mathematical Foundations of Computer Science, pages 239-250. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28629-5_16.
  17. Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, and Stefan Szeider. Hardness of random reordered encodings of parity for resolution and CDCL. Proceedings of the AAAI Conference on Artificial Intelligence, 38(8):7978-7986, March 2024. URL: https://doi.org/10.1609/aaai.v38i8.28635.
  18. Leroy Chew and Marijn J. H. Heule. Sorting parity encodings by reusing variables. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 1-10. Springer, Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_1.
  19. Dmitry Chistikov and Christoph Haase. On the complexity of quantified integer programming. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 94:1-94:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.94.
  20. Abhimanyu Choudhury and Meena Mahajan. Dependency schemes in CDCL-based QBF solving: A proof-theoretic study. J. Autom. Reason., 68(3):16, 2024. URL: https://doi.org/10.1007/s10817-024-09707-4.
  21. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  22. Santanu S Dey and Marco Molinaro. Theoretical challenges towards cutting-plane selection. Mathematical Programming, 170:237-266, 2018. URL: https://doi.org/10.1007/s10107-018-1302-4.
  23. Thorsten Ederer, Michael Hartisch, Ulf Lorenz, Thomas Opfer, and Jan Wolf. Yasol: an open source solver for quantified mixed integer programs. In Advances in Computer Games: 15th International Conferences, ACG 2017, Leiden, The Netherlands, July 3-5, 2017, Revised Selected Papers 15, pages 224-233. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-71649-7_19.
  24. Pavlos Eirinakis, Salvatore Ruggieri, K Subramani, and Piotr Wojciechowski. On quantified linear implications. Annals of Mathematics and Artificial Intelligence, 71(4):301-325, 2014. URL: https://doi.org/10.1007/s10472-013-9332-3.
  25. Alex Ferguson and Barry O’Sullivan. Relaxations and explanations for quantified constraint satisfaction problems. In International Conference on Principles and Practice of Constraint Programming, pages 690-694. Springer, 2006. URL: https://doi.org/10.1007/11889205_52.
  26. Ian P Gent, Peter Nightingale, Andrew Rowley, and Kostas Stergiou. Solving quantified constraint satisfaction problems. Artificial Intelligence, 172(6-7):738-771, 2008. URL: https://doi.org/10.1016/j.artint.2007.11.003.
  27. Richard Gerber, William Pugh, and Manas Saksena. Parametric dispatching of hard real-time tasks. IEEE transactions on computers, 44(3):471-479, 1995. URL: https://doi.org/10.1109/12.372041.
  28. Fred Glover. Surrogate constraints. Operations Research, 16(4):741-749, 1968. URL: https://doi.org/10.1287/opre.16.4.741.
  29. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-Boolean proofs. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5):3768-3777, 2021. URL: https://doi.org/10.1609/aaai.v35i5.16494.
  30. Marc Goerigk and Michael Hartisch. Multistage robust discrete optimization via quantified integer programming. Computers & Operations Research, 135:105434, 2021. URL: https://doi.org/10.1016/j.cor.2021.105434.
  31. Marc Goerigk and Michael Hartisch. An introduction to robust combinatorial optimization. International Series in Operations Research and Management Science, 2024. URL: https://doi.org/10.1007/978-3-031-61261-9.
  32. Marc Goerigk, Jannis Kurtz, and Michael Poss. Min-max-min robustness for combinatorial problems with discrete budgeted uncertainty. Discrete Applied Mathematics, 285:707-725, 2020. URL: https://doi.org/10.1016/j.dam.2020.07.011.
  33. Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2024. URL: https://www.gurobi.com.
  34. Michael Hartisch. Quantified integer programming with polyhedral and decision-dependent uncertainty. PhD thesis, University of Siegen, Germany, 2020. URL: https://doi.org/10.25819/ubsi/4841.
  35. Michael Hartisch. Adaptive relaxations for multistage robust optimization. In Pacific Rim International Conference on Artificial Intelligence, pages 485-499. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-89188-6_36.
  36. Michael Hartisch and Leroy Chew. MichaelHartisch/EQuIPS. Software, DFG-534441421, FWF Project ESP197, (visited on 2025-07-23). URL: https://github.com/MichaelHartisch/EQuIPS
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24095
  37. Michael Hartisch, Thorsten Ederer, Ulf Lorenz, and Jan Wolf. Quantified integer programs with polyhedral uncertainty set. In Computers and Games: 9th International Conference, CG 2016, Leiden, The Netherlands, June 29-July 1, 2016, Revised Selected Papers 9, pages 156-166. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-50935-8_15.
  38. Michael Hartisch and Ulf Lorenz. Mastering uncertainty: towards robust multistage optimization with decision dependent uncertainty. In PRICAI 2019: Trends in Artificial Intelligence: 16th Pacific Rim International Conference on Artificial Intelligence, Cuvu, Yanuca Island, Fiji, August 26-30, 2019, Proceedings, Part I 16, pages 446-458. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29908-8_36.
  39. Michael Hartisch and Ulf Lorenz. A novel application for game tree search-exploiting pruning mechanisms for quantified integer programs. In Advances in Computer Games: 16th International Conference, ACG 2019, Macao, China, August 11-13, 2019, Revised Selected Papers 16, pages 66-78. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-65883-0_6.
  40. Michael Hartisch and Ulf Lorenz. A general model-and-run solver for multistage robust discrete linear optimization. arXiv preprint arXiv:2210.11132, 2022. URL: https://doi.org/10.48550/arXiv.2210.11132.
  41. Alexey Ignatiev, Mikoláš Janota, and Joao Marques-Silva. Quantified maximum satisfiability. Constraints, 21:277-302, 2016. URL: https://doi.org/10.1007/s10601-015-9195-9.
  42. Mikoláš Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. In Alessandro Cimatti and Roberto Sebastiani, editors, Proc. 15th International Conference on Theory and Applications of Satisfiability Testing, volume 7317, pages 114-128. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_10.
  43. Mikoláš Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. URL: https://doi.org/10.1016/j.tcs.2015.01.048.
  44. Mikoláš Janota. Towards generalization in QBF solving via machine learning. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1):6607-6614, April 2018. URL: https://doi.org/10.1609/aaai.v32i1.12208.
  45. Florian Lonsing and Uwe Egly. Depqbf 6.0: A search-based QBF solver beyond traditional QCDCL. In Automated Deduction-CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pages 371-384. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_23.
  46. Florian Lonsing and Uwe Egly. Evaluating QBF solvers: Quantifier alternations matter. In John Hooker, editor, Principles and Practice of Constraint Programming, pages 276-294, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-98334-9_19.
  47. Ulf Lorenz and Jan Wolf. Solving multistage quantified linear optimization problems with the alpha-beta nested benders decomposition. EURO Journal on Computational Optimization, 3:349-370, 2015. URL: https://doi.org/10.1007/s13675-015-0038-7.
  48. Francesca Maggioni, Fabrizio Dabbene, and Georg Ch. Pflug. Sampling methods for multi-stage robust optimization problems. Ann. Oper. Res., 347(3):1385-1423, 2025. URL: https://doi.org/10.1007/s10479-025-06545-4.
  49. Nikos Mamoulis and Kostas Stergiou. Algorithms for quantified constraint satisfaction problems. In International Conference on Principles and Practice of Constraint Programming, pages 752-756. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30201-8_60.
  50. Hugues Marchand and Laurence A Wolsey. Aggregation and mixed integer rounding to solve MIPs. Operations research, 49(3):363-371, 2001. URL: https://doi.org/10.1287/opre.49.3.363.11211.
  51. Toshihiro Matsui, Hiroshi Matsuo, Marius Calin Silaghi, Katsutoshi Hirayama, Makoto Yokoo, and Satomi Baba. A quantified distributed constraint optimization problem. In Proc. 9th Int'l. Conf. on Autonomous Agents and Multiagent Systems (AAMAS2010), volume 1, pages 1023-1030. Nagoya Institute of Technology, 2010. URL: https://dl.acm.org/citation.cfm?id=1838344.
  52. George L. Nemhauser and Laurence A. Wolsey. Integer and Combinatorial Optimization. Wiley interscience series in discrete mathematics and optimization. Wiley, 1988. URL: https://doi.org/10.1002/9781118627372.
  53. Danny Nguyen and Igor Pak. The computational complexity of integer programming with alternations. Mathematics of Operations Research, 45(1):191-204, 2020. URL: https://doi.org/10.1287/moor.2018.0988.
  54. Peter Nightingale. Non-binary quantified CSP: algorithms and modelling. Constraints, 14:539-581, 2009. URL: https://doi.org/10.1007/s10601-009-9068-1.
  55. Jérémy Omer, Michael Poss, and Maxime Rougier. Combinatorial robust optimization with decision-dependent information discovery and polyhedral uncertainty. Open Journal of Mathematical Optimization, 5:1-25, 2024. URL: https://doi.org/10.5802/ojmo.33.
  56. Michael Poss. Robust combinatorial optimization with variable cost uncertainty. European Journal of Operational Research, 237(3):836-845, 2014. URL: https://doi.org/10.1016/j.ejor.2014.02.060.
  57. Krzysztof Postek and Dick den Hertog. Multistage adjustable robust mixed-integer optimization via iterative splitting of the uncertainty set. INFORMS Journal on Computing, 28(3):553-574, 2016. URL: https://doi.org/10.1287/ijoc.2016.0696.
  58. Andrew Reynolds, Tim King, and Viktor Kuncak. Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods in System Design, 51:500-532, 2017. URL: https://doi.org/10.1007/s10703-017-0290-y.
  59. Alexander Schrijver. Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. Wiley, 1999. Google Scholar
  60. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending sat solvers to cryptographic problems. In International Conference on Theory and Applications of Satisfiability Testing, pages 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  61. Kostas Stergiou. Repair-based methods for quantified CSPs. In International Conference on Principles and Practice of Constraint Programming, pages 652-666. Springer, 2005. URL: https://doi.org/10.1007/11564751_48.
  62. K Subramani. Analyzing selected quantified integer programs. In International Joint Conference on Automated Reasoning, pages 342-356. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-25984-8_26.
  63. Kerian Thuillier, Anne Siegel, and Loïc Paulevé. CEGAR-based approach for solving combinatorial optimization modulo quantified linear arithmetics problems. Proceedings of the AAAI Conference on Artificial Intelligence, 38(8):8146-8153, March 2024. URL: https://doi.org/10.1609/aaai.v38i8.28654.
  64. Phebe Vayanos, Daniel Kuhn, and Berç Rustem. A constraint sampling approach for multi-stage robust optimization. Automatica, 48(3):459-471, 2012. URL: https://doi.org/10.1016/j.automatica.2011.12.002.
  65. Guillaume Verger and Christian Bessiere. Guiding search in QCSP+ with back-propagation. In International Conference on Principles and Practice of Constraint Programming, pages 175-189. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85958-1_12.
  66. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In ICCAD, pages 442-449, 2002. URL: https://doi.org/10.1145/774572.774637.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact