2025/06/04 by Michael Hartisch, Hartisch, Michael, Leroy Chew +1
Computer Science · #Advanced Multi-Objective Optimization Algorithms #Artificial Intelligence (cs.AI) #Constraint Satisfaction and Optimization #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2506.04452
openalex publication_date 2025/06/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.