One-Parametric Presburger Arithmetic has Quantifier Elimination

TL;DR

This paper presents a quantifier elimination procedure for one-parametric Presburger arithmetic, extending classical Presburger arithmetic with a parameterized multiplication function, resolving an open problem and enabling efficient decision procedures.

Contribution

It introduces a novel quantifier elimination algorithm for one-parametric Presburger arithmetic, including all integer division functions, and analyzes its complexity and implications for satisfiability.

Findings

Quantifier elimination is achievable for the extended structure with all integer division functions.

The satisfiability problem for the existential fragment is in NP.

Smallest solutions in this fragment have polynomial bit size.

Abstract

We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function $x \mapsto t \cdot x$, where $t$ is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al., Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions $x \mapsto \lfloor{\frac{x}{f(t)}}\rfloor$, one for each integer polynomial $f$. Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring $\mathbb{Z}[t]$ of univariate polynomials. The second is reminiscent of the so-called "base $t$ division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size.