On the Complexity of Linear Arithmetic with Divisibility

We consider the complexity of deciding the truth of first-order existential sentences of linear arithmetic with divisibility over both the integers and the p-adic numbers. We show that if an existential sentence of Presburger arithmetic with divisibility is satisfiable then the smallest satisfying assignment has size at most exponential in the size of the formula, showing that the decision problem for such sentences is in NEXPTIME. Establishing this upper bound requires subtle adaptations to an existing decidability proof of Lipshitz. We consider also the first-order linear theory of the p-adic numbers. Here divisibility can be expressed via the valuation function. The decision problem for existential sentences over the p-adic numbers is an important component of the decision procedure for existential Presburger arithmetic with divisibility. The problem is known to be NP-hard and in EXPTIME, as a second main contribution, we show that this problem lies in the Counting Hierarchy, and therefore in PSPACE.