Algebraic Circuits Over Sum and Shift and Existential Presburger Arithmetic with Divisibility
For researchers in computational complexity and logic, this result establishes a new lower bound for a fundamental decision problem, showing it is harder than previously believed.
The paper proves that satisfiability for existential Presburger arithmetic with divisibility (EPAD) is PP-hard, ruling out the long-held expectation that it lies in NP unless NP=PP. This also implies PP-hardness for positive Boolean combinations of word equations and length constraints.
We study existential Presburger arithmetic extended with divisibility predicates (EPAD). Its satisfiability problem has long been known to be NP-hard, and has often been expected to lie in NP. We prove that it is PP-hard, ruling out this expectation unless NP=PP. This also implies \PP-hardness of satisfiability for positive Boolean combinations of word equations and length constraints. The lower bound is compatible with a strong form of Lipshitz-style simplification. We define a polynomial-time recognizable fragment, called \MergeAbs, in which the usual finite-quotient replacement of divisibility atoms can be repeated until no divisibility atom remains. Nevertheless, EPAD satisfiability is already PP-hard on this fully simplifiable fragment. The reduction starts from a threshold coefficient problem for a class of arithmetic circuits using only addition and shifts. The same systems used in the reduction also expose a limitation of normalization. A polynomial-size scaling family, indexed by $j$, forces an endpoint relation $v=(2^{2^j}+1)u$, and the natural finite-quotient simplification records it as one equation with coprime coefficients whose largest coefficient has bit-size $Θ(2^j)$.