An Expansion-Based Approach for Quantified Integer Programming

Hartisch M, Chew L (2025)

Publication Type: Conference contribution

Publication year: 2025

Journal

LIPIcs : Leibniz International Proceedings in Informatics Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 340

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Glasgow, GBR

ISBN: 9783959773805

DOI: 10.4230/LIPIcs.CP.2025.12

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.

Involved external institutions

Universität Passau DE Germany (DE) Technische Universität Wien / Vienna University of Technology AT Austria (AT)

How to cite

APA:

Hartisch, M., & Chew, L. (2025). An Expansion-Based Approach for Quantified Integer Programming. In Maria Garcia de la Banda (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Glasgow, GBR: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Hartisch, Michael, and Leroy Chew. "An Expansion-Based Approach for Quantified Integer Programming." Proceedings of the 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, GBR Ed. Maria Garcia de la Banda, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2025.

BibTeX: Download