NEXP-Completeness of Existential Presburger Arithmetic with Divisibility

Abstract

We prove that satisfiability for existential Presburger arithmetic with divisibility (EPAD) is NEXP-hard. Together with the known NEXP upper bound, this establishes NEXP-completeness. The lower bound is obtained by encoding succinct Boolean formulas whose satisfying assignments may have exponential length. A central difficulty is to represent, within a polynomial-size EPAD formula, the exponentially long integers arising in this encoding. To address this difficulty, we introduce fixed-width arithmetic logic circuits (ALCs), whose gates perform addition, multiplication, and bit shifts. We show that polynomial-size uniform ALC families compute exactly the functions in FPSPACE, while their succinct exponential-size counterpart computes exactly the functions in FEXP. In both cases, the computed functions admit polynomial-size functional definitions in EPAD. This provides the compressed arithmetic needed for the lower-bound reduction. The same construction yields NEXP-hardness for nonerasing word equations with Presburger length constraints over a fixed two-letter alphabet. We also study the elimination of divisibility constraints by enumerating their possible quotients. Earlier work identified an NP fragment in which the variables can be ordered so that divisibility dependencies always move forward through the order. We introduce a different fragment, called merge-absorptive, in which bounded-quotient divisibilities can successively connect all variable components. This fragment is polynomial-time recognizable and admits complete finite-quotient elimination, yet its satisfiability problem remains NEXP-complete. Finally, we show that the elimination process may necessarily produce equations with exponentially large coefficients.