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)$.

翻译：我们研究了扩展了可除性谓词的存在Presburger算术（EPAD）。其可满足性问题长期以来已知为NP难问题，且常被预期属于NP。我们证明它是PP难的，从而排除了这一预期，除非NP=PP。这也蕴含了单词方程与长度约束的正布尔组合的可满足性问题的PP难性。该下界与Lipshitz型强简化形式相容。我们定义了一个多项式时间可识别的片段，称为\MergeAbs，在其中可重复使用通常的有限商替换可除性原子，直至无可除性原子剩余。尽管如此，EPAD的可满足性在此完全可简化片段上已是PP难的。该归约始于一类仅使用加法与移位的算术电路的阈值系数问题。归约中使用的同一系统也揭示了归一化的局限性。一个由$j$索引的多项式大小缩放族强制了端点关系$v=(2^{2^j}+1)u$，而自然的有限商简化将其记录为具有互质系数的单一方程，其最大系数的比特大小为$Θ(2^j)$。