One-Parametric Presburger Arithmetic has Quantifier Elimination
Authors:
Alessio Mansutti,
Mikhail R. Starchak
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…
▽ More
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.
△ Less
Submitted 30 June, 2025;
originally announced June 2025.
Integer Linear-Exponential Programming in NP by Quantifier Elimination
Authors:
Dmitry Chistikov,
Alessio Mansutti,
Mikhail R. Starchak
Abstract:
This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms $2^x$ and remainder terms ${(x \bmod 2^y)}$. Our result implies that the existential theory of the structure $(\mathbb{N},0,1,+,2^{(\cdot)},V_2(\cdot,\cdot),\leq)$ has an NP-complete sa…
▽ More
This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms $2^x$ and remainder terms ${(x \bmod 2^y)}$. Our result implies that the existential theory of the structure $(\mathbb{N},0,1,+,2^{(\cdot)},V_2(\cdot,\cdot),\leq)$ has an NP-complete satisfiability problem, thus improving upon a recent EXPSPACE upper bound. This theory extends the existential fragment of Presburger arithmetic with the exponentiation function $x \mapsto 2^x$ and the binary predicate $V_2(x,y)$ that is true whenever $y \geq 1$ is the largest power of $2$ dividing $x$.
Our procedure for solving linear-exponential systems uses the method of quantifier elimination. As a by-product, we modify the classical Gaussian variable elimination into a non-deterministic polynomial-time procedure for integer linear programming (or: existential Presburger arithmetic).
△ Less
Submitted 9 July, 2024;
originally announced July 2024.
