An Expansion-Based Approach for Quantified Integer Programming

TL;DR

This paper introduces an expansion-based solution method for Quantified Integer Programming (QIP) using CEGAR, demonstrating improved performance over existing search-based solvers and enabling modeling of complex optimization problems.

Contribution

It presents the first expansion-based approach for QIP utilizing CEGAR, extending techniques from QBF and applying them to multistage robust optimization.

Findings

Superior performance over search-based QIP solvers in specific instances

Effective modeling of multistage robust discrete linear optimization problems

Notable performance gains over state-of-the-art expansion-based QBF solvers

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.