Algebraic Circuits Over Sum and Shift and Existential Presburger Arithmetic with Divisibility
This paper proves that the satisfiability problem of existential Presburger arithmetic extended with divisibility predicates (EPAD) is PP-hard.
First to prove PP-hardness of EPAD satisfiability
Keywords
To understand this paper, make sure you know these concepts first:
- Understanding of mathematical logic systems, specifically Presburger arithmetic and satisfiability problemsfind papers →
Abstract
More Like ThisWe 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)$.