Quantifier Elimination Over the Integers
Rui-Juan Jing, Yuzhuo Lei, Christopher Frank Stephan Maligec, Marc Moreno Maza, Chirantan Mukherjee · Journal of Symbolic Computation · 2025
In this paper, we address algebraic issues of the quantifier elimination problem in Presburger arithmetic. First, we revisit, in a unified presentation, different techniques from polyhedral geometry that can support quantifier elimination over the integers. Second, we discuss optimizations for one of these techniques by taking advantages of parametric systems of multivariate linear congruences. Third, we report on a comparative implementation of these different strategies for quantifier elimination in Presburger arithmetic. Fourth, we apply these results and propose a new algorithm for performing parametric integer linear programming and report on its implementation.