# An Expansion-Based Approach for Quantified Integer Programming

arXiv: https://arxiv.org/abs/2506.04452 · HTML: https://mlsanity.com/paper/2506.04452/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 65 references that are in the map.
- First posted on arXiv 4 Jun 2025.

## Builds on (most cited first, 10 of 10)

- [Theoretical challenges towards cutting-plane selection](https://mlsanity.com/paper/1805.02782/) (2018)
- [Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs](https://mlsanity.com/paper/2209.12185/) (2022)
- [DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL](https://mlsanity.com/paper/1702.08256/) (2017)
- [Evaluating QBF Solvers: Quantifier Alternations Matter](https://mlsanity.com/paper/1701.06612/) (2017)
- [Min-Max-Min Robustness for Combinatorial Problems with Discrete Budgeted Uncertainty](https://mlsanity.com/paper/1910.12608/) (2019)
- [Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction](https://mlsanity.com/paper/1403.0222/) (2014)
- [The computational complexity of integer programming with alternations](https://mlsanity.com/paper/1702.08662/) (2017)
- [Adaptive Relaxations for Multistage Robust Optimization](https://mlsanity.com/paper/2106.12858/) (2021)
- [Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution](https://mlsanity.com/paper/2109.04862/) (2021)
- [A general model-and-run solver for multistage robust discrete linear optimization](https://mlsanity.com/paper/2210.11132/) (2022)

## Abstract (arXiv)

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.