## On the complexity of linear arithmetic
with divisibility

*Antonia Lechner*,
*Joël
Ouaknine*, and *James Worrell*
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 **Q**_{p}. Here divisibility can be
expressed via the valuation function. The decision problem for
existential sentences over **Q**_{p} 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.

*Proceedings of LICS 15*, 2015. 10 pages.

PDF
© 2015 IEEE Computer Society Press.