An Expansion-Based Approach for Quantified Integer Programming
This work addresses complex decision-making and optimization under uncertainty for researchers and practitioners in fields like operations research and AI, representing an incremental advancement by adapting QBF techniques to QIP.
The paper tackled the problem of solving Quantified Integer Programming (QIP) by introducing an expansion-based approach using Counterexample-Guided Abstraction Refinement (CEGAR), which demonstrated superior performance over existing search-based solvers for QIP in specific instances and notable gains over state-of-the-art expansion-based solvers for QBF.
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.