One-Parametric Presburger Arithmetic
Has Quantifier Elimination

This paper does not provide a complexity analysis for full $\text{PrA}[t]$. A back-of-the-envelope calculation of the runtime of the procedures in [6] and [15] suggests that the satisfiability problem for $\text{PrA}[t]$ is in elementary time (potentially in 3ExpTime). However, these procedures do not yield an NP upper bound for the existential fragment. In contrast, the procedure we introduce shows $\exists$$\text{PrA}[t]$ in NP, but it may in principle run in non-elementary time on arbitrary formulae. Unifying these procedures into a single “optimal” one seems possible and will be addressed in a forthcoming extended version of this paper. This would also provide an extension to the 3ExpTime quantifier-elimination procedure for almost linear arithmetic proposed by Weispfenning in [30].

Most of the literature on $\text{PrA}[t]$ focuses on computing the function $f(k)≔\mathrm{\#}{⟦\phi ⟧}_k$, as introduced in [6]. Not much is known regarding the complexity of computing this function. To our knowledge, the most significant result in this direction is the one in [5], where Bogart, Goodrick, Nguyen, and Woods show that $f(k)$ can be computed in polynomial time (in the bit-length of $k$ given as part of the input) whenever $\phi$ is a fixed $\text{PrA}[t]$-formula. We believe Theorem 3 to be a good starting point for further research in this direction.

While our work shows that the feasibility problem for integer programs in which a single variable occurs non-linearly is in NP, the paper does not discuss related optimisation problems of minimisation/maximisation. From our quantifier elimination procedure, we can show that if there are optimal solutions to a linear polynomial with coefficients in $\mathbb{Z}[t]$ subject to a formula in $\exists$$\text{PrA}[t]$, then one is of polynomial bit size. Generalising this result to other non-convex objectives is an interesting avenue for future research.

As discussed in Section 1, the paper concerns the extension of the first-order theory of $⟨\mathbb{Z};\mathrm{\hspace{0.17em}0},\mathrm{\hspace{0.17em}1},+,x\mapsto t\cdot x,\le ⟩$ by all integer division functions $x\mapsto \lfloor \frac{x}{\left|f\right|}\rfloor$, where $f\in \mathbb{Z}[t]$. However, in the context of our quantifier elimination procedure, it is more natural to work within the (equivalent) first-order theory of the structure:

where:

• $\mathrm{■}$

  The integer division $x\mapsto \lfloor \frac{x}{t^d}\rfloor$ is only defined for $t\ne 0$, with the obvious interpretation.

• $\mathrm{■}$

  The integer remainder function $x\mapsto (xmodf(t))$ is defined following the equivalence

  $$(xmodf(t)=y)\iff (f(t)=0\wedge y=x)\vee (f(t)\ne 0\wedge y=x-\left|f(t)\right|\cdot \lfloor \frac{x}{\left|f(t)\right|}\rfloor ).$$

  We remark that whenever $f(t)\ne 0$ the result of $(xmodf(t))$ belongs to $[0,\left|f(t)\right|-1]$.

  (Also note that the absolute value function $|.|$ is easily definable in Presburger arithmetic.)

• $\mathrm{■}$

  The divisibility relation $f(t)|x$ is a unary relation, and is defined following the equivalence

  $$(f(t)|x)\iff (f(t)=0\wedge x=0)\vee (f(t)\ne 0\wedge (xmodf(t)=0)).$$

  We remark that the divisibility relations and integer remainder functions are defined to satisfy the equivalence $f(t)|x\iff f(t)|(xmodf(t))$ also when $f(t)$ evaluates to $0$.

For simplicity, we still denote this first-order theory with $\text{<em class="ltx\_emph ltx\_font\_upright">PrA</em>}[t]$. Observe that we have ultimately defined $(f(t)|\cdot )$ and $x\mapsto (xmodf(t))$ in terms of $x\mapsto \lfloor \frac{x}{\left|f\right|}\rfloor$. As a result, every formula in this first-order theory can be translated into a formula from the theory in Theorem 2. This translation can be performed in polynomial time by introducing new existential quantifiers, or in exponential time without adding quantifiers (the blow-up is only due to the disjunctions in the definitions of $(f(t)|\cdot )$ and $x\mapsto (xmodf(t))$).

The terms of $\text{PrA}[t]$ are built from the constants $0,1$, integer variables, and the functions of the structure. Without loss of generality, we restrict ourselves to (finite) terms of the form

where all $f_i$ and $g_i$ belong to $\mathbb{Z}[t]$, all $d_i$ belong to $\mathbb{N}$, and each ${\tau }_i$ is another term of this form. The term $\tau$ is said to be linear, if $f_i(t)=0$ for $i\in [n+1,k]$ (i.e., it does not contain integer division, nor integer remainder functions), and non-shifted whenever $f_0(t)=0$. Above, the terms $\lfloor \frac{{\tau }_i}{t^{d_i}}\rfloor$ and $({\tau }_{i}mod{g}_i(t))$ are linear occurrences of the integer division functions and integer remainder functions, and are said to occur linearly in $\tau$. When every $f_i$ is an integer (a degree $0$ polynomial), we define $1$-norm of $\tau$ as ${\parallel \tau \parallel }_1≔{\sum }_{i=0}^k\left|f_i\right|$.

Moving to the atomic formulae of the theory, it is easy to see that equalities, inequalities and divisibility relations can be rewritten (in polynomial time) to be of the form $\tau =0$, $\tau \le 0$ and $f(t)|\tau$, respectively, where $\tau$ is a term of the form given in Equation 1. Syntactically, we will only work with atomic formulae of these forms, which we call $\text{PrA}[t]$ constraints. However, for readability, we will still sometimes write (in)equalities featuring non-zero terms on both sides (i.e., ${\tau }_1\le {\tau }_2$), and strict inequalities and ${\tau }_2>{\tau }_1$; both are short for ${\tau }_1-{\tau }_2+1\le 0$. A $\text{PrA}[t]$ constraint is said to be linear if the term $\tau$ featured in it is linear.

We restrict ourselves to formulae in prenex normal form $\exists {𝒙}_1\forall {𝒙}_2\mathrm{\dots }\exists {𝒙}_n:\phi$ where $\phi$ is a positive Boolean combination of $\text{PrA}[t]$ constraints; that is, the only Boolean connectives featured in $\phi$ are conjunctions $\wedge$ and disjunctions $\vee$. This restriction is without loss of generality, as De Morgan’s laws allow to push all negations at the level of literals, which can then be removed with the equivalences ,  $\neg (\tau \le 0)\iff \tau >0$ and .

For two terms ${\tau }_1$ and ${\tau }_2$, we write $[{\tau }_2/{\tau }_1]$ for a term substitution. We see these substitutions as functions from terms to terms or from formulae to formulae: $\tau [{\tau }_2/{\tau }_1]$ is the term obtained by replacing, in the term $\tau$, every occurrence of ${\tau }_1$ with ${\tau }_2$. Analogously, $\phi [{\tau }_2/{\tau }_1]$ is the formula obtained from $\phi$ by replacing the term $\tau$ with $\tau [{\tau }_2/{\tau }_1]$ in every atomic formula $\tau =0$, $\tau \le 0$, or $f(t)|\tau$. In Section 4 we will also need a stronger notion of substitution, called vigorous substitution in [11]; we defer its definition to that section.

These lines remove all occurrences of the integer division functions $x\mapsto \lfloor \frac{x}{t^d}\rfloor$ and of the integer remainder functions $x\mapsto (xmodf(t))$, at the expense of adding new existentially quantified variables that are later eliminated. After this step, the formula is a positive Boolean combination of linear constraints. For the integer division function, the algorithm simply adds to the sequence of variables $𝒙$ to be eliminated a fresh variable $x$ to proxy a term $\lfloor \frac{\tau }{t^d}\rfloor$ (line 2). It then relies on the equivalence to replace $\lfloor \frac{\tau }{t^d}\rfloor$ with $x$ (line 3). The removal of integer remainder functions is performed differently. First, let us observe that the following equivalence holds:

The formula $f(t)=0\wedge y=\tau$ on the right-hand side of the equivalence is considered in line 8. This line is executed conditionally to a non-deterministic branching (line 6). If it is not executed, then lines 9–11 are executed instead; these correspond to the formula . The interesting property of this formula is that the variable $y$ appears bounded by $0$ from below, and by either $f(t)-1$ or $-f(t)-1$ from above (following the sign of $f(t)$). Instead of quantifying $y$ using standard existential quantifiers (as done for the variables replacing $\lfloor \frac{\tau }{t^d}\rfloor$), in line 10 we use a bounded quantifier:

Let us write ${𝒙}_{\beta },{𝒚}_{\beta },B_{\beta }$ and ${\phi }_{\beta }$ for the values taken by $𝒙$, $𝒚$, $B$ and $\phi$ in the non-deterministic branch $\beta$, when the control flow of the program reaches line 12. The following equivalence holds, where the disjunction ${\bigvee }_{\beta }$ ranges across all non-deterministic branches:

Once reaching line 12, the algorithm proceeds by calling the procedure BoundedQE. We will discuss this procedure in Section 4. In a nutshell, its role is to replace the quantifiers $\exists {𝒙}_{\beta }$ on the right-hand side of Equation 2 with bounded quantifiers, that are merged with the already existing block of bounded quantifiers $\exists {𝒚}_{\beta }\le B_{\beta }$. The formal specification of BoundedQE is given in the next lemma.

As stated, the lemma above is also proved by Goodrick in [15], who introduced the first bounded quantifier elimination procedure specifically for $\text{PrA}[t]$. When applied to existential formulae, that procedure requires doubly-exponential time, making it unsuitable for establishing Theorem 3. In contrast, BoundedQE runs in non-deterministic polynomial time. Due to this difference, we cannot rely directly on [15] and must thus re-establish Lemma 5.

BoundedQE introduces divisibility constraints $f(t)|\tau$. The next step, detailed in Algorithm 2 (ElimDiv), eliminates all divisibility constraints in favour, once more, of bounded quantifiers.

The idea behind Algorithm 2 is as follows. Let $f(t)|\sigma (𝒘)+\tau (𝒛)$ be a constraint from the input formula, where $𝒘$ are the variables in the block of bounded quantifiers (these correspond to the variables ${𝒚}_{\beta }$ from Equation 2 and those introduced by BoundedQE), and $𝒛$ are the free variables. Notice that this constraint is equivalent to $f(t)|\sigma (𝒘)+(\tau (𝒛)modf(t))$, which is in turn equivalent to the existential formula $\exists y:f(t)\cdot y+\sigma (𝒘)+(\tau (𝒛)modf(t))=0$, where $y$ is a fresh variable ranging over $\mathbb{Z}$. Since $𝒘$ is constrained by bounded quantifiers, we can upper-bound the number of digits in the base $t$ encoding of the linear term $\sigma (𝒘)$ (recall: $t\ge 2$). When $f(t)\ne 0$, the same applies to $(\tau (𝒛)modf(t))$, which ranges between $0$ and $f(t)-1$; and this in turn imposes a bound on the base $t$ representation of $y$. When $f(t)=0$ instead, the truth of $f(t)\cdot y+\sigma (𝒘)+(\tau (𝒛)modf(t))=0$ only depends on whether $\sigma (𝒘)+(\tau (𝒛)modf(t))=0$, and we can thus restrict $y$ to any non-empty interval. This allows us to replace the quantifier $\exists y$ with a bounded quantifier (lines 3 and 4). Since $y$ ranges over $\mathbb{Z}$, whereas bounded quantifiers use non-negative ranges, the algorithm explicitly guesses the sign of $y$ in line 5, allowing $y$ to only range over $\mathbb{N}$ instead. Formalising these arguments yields the following lemma.

From the output of ElimDiv, the final operation by $\text{PrA}[t]$-QE is a call to ElimBounded, which removes all bounded quantifiers. This algorithm is detailed in Section 5. Its specification is given in the next lemma.

Together, Equation 2 and Lemmas 5, 6, and 7 show that $\text{PrA}[t]$-QE meets its specification; thus showing Theorem 2 conditionally to the correctness of BoundedQE and ElimBounded.

Problems arise when looking at the complexity of the procedure outlined above. To understand this point, consider the inequality $b\cdot (\tau +s)\le a\cdot \rho$, which was derived by substituting $\frac{\tau +s}{a}$ for $x$ in $b\cdot x\le \rho$, and suppose $\tau =c\cdot y+{\tau }^{\prime }$ and $\rho =d\cdot y+{\rho }^{\prime }$, for some variable $y$. This inequality can be rewritten as $(b\cdot c-a\cdot d)\cdot y+b\cdot {\tau }^{\prime }-a\cdot {\rho }^{\prime }+b\cdot s\le 0$. When looking at the coefficient $(b\cdot c-a\cdot d)$ of $y$ one deduces that, if quantifier elimination is performed carelessly on a block $\exists 𝒙$ of multiple existential quantifiers, the coefficients of the variables in the formula will grow quadratically with each eliminated variable. Then, by the end of the procedure, their binary bit size will be exponential in the number of variables in $𝒙$. However, this explosion can be avoided by noticing that coefficients are updated following the same pattern as in Bareiss’ polynomial-time Gaussian elimination procedure [1]. This insight was highlighted in [11], building upon an earlier observation from [31]. In Bareiss’ algorithm, the key to keeping coefficients polynomially bounded is given by the Desnanot–Jacobi identity. Consider an $m\times d$ matrix $A$. Let us write $A[i_1,\mathrm{\dots },i_r;j_1,\mathrm{\dots },j_{\mathrm{\ell }}]$ for the $r\times \mathrm{\ell }$ sub-matrix of $A$ made of the rows with indices $i_1,\mathrm{\dots },i_r\in [1,m]$ and columns with indices $j_1,\mathrm{\dots },j_{\mathrm{\ell }}\in [1,d]$. For $i,j,\mathrm{\ell }\in \mathbb{N}$ with $0\le \mathrm{\ell }\le \min (m,d)$, $1\le i\le m$ and $1\le j\le d$, we define $a_{i,j}^{(\mathrm{\ell })}≔detA[1,\mathrm{\dots },\mathrm{\ell },i;1,\mathrm{\dots },\mathrm{\ell },j]$.

The Desnanot–Jacobi identity is true for all matrices with entries over an integral domain (a non-zero commutative ring in which the product of non-zero elements is non-zero), and therefore we can take the entries of $A$ to be polynomials in $\mathbb{Z}[t]$.

Returning to our informal discussion, we now see that the coefficient $(b\cdot c-a\cdot d)$ of $y$ is oddly similar to the left-hand side of the Desnanot–Jacobi identity. Suppose that the elements $a_{i,j}^{(\mathrm{\ell }-1)}$ are the coefficients of the variables in the formula currently being processed by the quantifier elimination procedure, and we are eliminating the $\mathrm{\ell }$-th quantifier. Proposition 8 tells us that all coefficients produced by the naïve elimination (left-hand side of the identity) have $a_{\mathrm{\ell },\mathrm{\ell }}^{(\mathrm{\ell }-2)}$ as a common factor. By dividing through by this common factor, we obtain smaller coefficients for the next step of variable elimination – namely, $a_{i,j}^{(\mathrm{\ell })}$. When eliminating the first variable ($\mathrm{\ell }=1$), the common factor is $1$. Otherwise, it is the coefficient $a$ that the $(\mathrm{\ell }-1)$-th eliminated variable $x$ has in the equality $a\cdot x=\tau +s$ used for the elimination. In Algorithm 3, the lines marked in blue implement Bareiss’ optimisation: line 8 initialises the common factor $\mathrm{\ell }(t)$ and its sign, line 15 updates it, and line 22 performs the division.

Lines 1–4 handle the divisibility constraints $f(t)|\tau$ with the divisor $f(t)$ equal to $0$. Such constraints are equalities in disguise, and the procedure replaces them with $\tau =0$. When the procedure reaches line 5, all divisors in the divisibility constraints are assumed non-zero. Following the example from the previous paragraph, recall that the shifts $s$ belong to intervals that depend on these divisors; when multiple divisors occur, the procedure for PrA takes their $\mathrm{lcm}$ (instead of just $m$ as in our example). For simplicity, instead of $\mathrm{lcm}$, BoundedQE considers the absolute value $m(t)$ of their product (line 6). After guessing the sign $\pm$ of this product, the procedure enforces $m(t)>0$ in line 7. This information is stored in the formula $\chi$, which accumulates all sign guesses made by the algorithm; these are conjoined to $\phi$ when the procedure returns.

Line 9 replaces all inequalities with equalities by introducing slack variables ranging over $\mathbb{N}$. (This step is inherited from [11].) Slack variables represent the shifts $s$ from the quantifier elimination procedure for PrA. Line 12 covers the corner cases of $x$ not appearing in equalities, or $t$ being such that all the coefficients $f(t)$ of $x$ evaluate to zero. After guessing an equality $f(t)\cdot x+\tau =0$ to perform the substitution (line 14), line 19 checks whether $\tau$ features a slack variable $y$ (i.e., the equality was originally an inequality). If so, the procedure generates a bounded quantifier for $y$. The elimination of $x$ (line 21) is performed with the vigorous substitution $\phi [[\frac{-\tau }{f(t)}/x]]$ which works as follows: 1: Replace every equality $\rho =0$ with $f(t)\cdot \rho =0$, and every divisibility $g(t)|\rho$ with $f(t)\cdot g(t)|f(t)\cdot \rho$; this is done also for constraints where $x$ does not occur. 2: Replace every occurrence of $f(t)\cdot x$ with $\tau$ (from step 1, each coefficient of $x$ in the system can be factored as $f(t)\cdot h(t)$ for some $h\in \mathbb{Z}[t]$).

After applying the vigorous substitution, the procedure divides all coefficients of the inequalities and divisibility constraints in $\phi$ by the common factor of the Bareiss’ optimisation (line 22). In the case of divisibility constraints, divisors are also affected. Proposition 8 ensures that these divisions are all without remainder. In practice, the traditional Euclidean algorithm for polynomial division can be used to construct the quotient in polynomial time. As a result of these divisions, throughout the procedure all polynomials $f(t)$ guessed in line 14 have polynomial bit sizes in the size of the input formula.

After the foreach loop of line 10 completes, all variables from $𝒙$ have been eliminated (line 21) or bounded (line 12). A benefit of translating inequalities into equalities in line 9 is that $x$ can be eliminated independently of the sign of its coefficient $f(t)$; inequalities would need to flip for $f(t)$ negative instead. The final step (lines 24 and 25) drops all slack variables for which no bound was assigned in line 20, reintroducing the inequalities (the sign stored in $\pm$ tells us the direction of these inequalities). This step is also inherited from [11].

By fully developing the arguments above, one shows that BoundedQE is correct:

This lemma implies Lemma 5. In the sequel we will also need the next lemma, discussing properties of the outputs of BoundedQE for “Presburger-arithmetic-like” inputs.

Following the semantics of bounded quantifiers, line 1 adds to $\phi$ the bounds $0\le w\wedge w\le B(w)$, for each bounded variable $w$. The subsequent lines “bit blast” $w$ into its $t$-ary expansion $t^M\cdot y_M+\mathrm{\cdots }+t\cdot y_1+y_0$, where $M$ is the largest bit size of the bounds in $B$ (line 2). All added variables $𝒚$ are $t$-digits, i.e., they range in $[0,t-1]$.

This step is defined by the while loop of line 7, whose goal is to transform the formula ${\phi }_{\mathrm{\varnothing }}$ into an equivalent positive Boolean combination of equalities and inequalities in which all coefficients of $𝒚$ are integers.

The while loop guesses some integers in line 11. Let $R_i$ be the (finite) set of all sequences $𝒔$ of guesses from the first $i$ iterations of the loop (so, $𝒔$ has length $i$), and let ${\phi }_{𝒔}$ be the unique formula obtained from ${\phi }_{\mathrm{\varnothing }}$ after iterating the loop $i$ times, using $𝒔$ as the sequence of guesses. (The subscript $\mathrm{\varnothing }$ corresponds to the empty sequence of guesses; the only element in $R_0$.)

Together with proving that the while loop preserves formula equivalence (across non-deterministic branches), the critical parameter to track during the execution of the loop is the degrees of all coefficients of the $t$-digits $𝒚$. Showing that this parameter reaches $0$ implies loop termination, and correctness of this step of the procedure. More formally, we inductively define the $𝒚$-degree $\mathrm{deg}(𝒚,\phi )$ of a positive Boolean combination of $\text{PrA}[t]$ constraints $\phi (𝒚,𝒛)$, where the variables $𝒚=(y_1,\mathrm{\dots },y_{\mathrm{\ell }})$ occur only linearly, as follows (below, $\sim \in \{\le ,=\}$):

• $\mathrm{■}$

  $\mathrm{deg}(𝒚,\phi )=\max \{\mathrm{deg}(f_i):i\in [1,\mathrm{\ell }]\}$

  if $\phi$ is an (in)equality ${\sum }_{i=1}^{\mathrm{\ell }}{f}_i(t)\cdot y_i+\tau (𝒛)\sim 0$;

• $\mathrm{■}$

  $\mathrm{deg}(𝒚,\phi )=\mathrm{deg}(𝒚,{\phi }_1)+\mathrm{deg}(𝒚,{\phi }_2)$

  if $\phi$ is either $({\phi }_1\wedge {\phi }_2)$ or $({\phi }_1\vee {\phi }_2)$.

Then, the defining property of the while loop of line 7 can be stated as follows:

The while loop considers an (in)equality $\eta \sim 0$ from ${\phi }_{𝒔}$ (line 7); inequalities are transformed into strict inequalities in line 8, as in this case the latter are easier to work with. Line 9 represents the term of the (in)equality as $\sigma (𝒚)\cdot t+\rho (𝒚)+\tau (𝒛)$, where $\sigma$ is linear, $\rho$ is a linear term with coefficients in $\mathbb{Z}$, and $\tau (𝒛)$ is non-shifted.

Let us define ${\eta }^{\prime }=\sigma (𝒚)+\lfloor \frac{\tau (𝒛)}{t^{k+1}}\rfloor$ and ${\rho }^{\prime }=\rho (𝒚)+\left(\lfloor \frac{\tau (𝒛)}{t^k}\rfloor modt\right)$, so that the term in Equation 3 is then equal to ${\eta }^{\prime }\cdot t+{\rho }^{\prime }$. (Note: ${\rho }^{\prime }$ is exactly the term in line 10.) We are now ready to perform the symbolic division by $t$. Indeed, since all variables in $𝒚$, as well as the term $\left(\lfloor \frac{\tau (𝒛)}{t^k}\rfloor modt\right)$, belong to $[0,t-1]$, we conclude that ${\rho }^{\prime }\in [-t\cdot N,t\cdot N]$ where $N≔{\parallel {\rho }^{\prime }\parallel }_1$. Line 11 guesses an integer $r$ from the segment $[-N,N]$, which stands for the quotient of the division of ${\rho }^{\prime }$ by $t$. Each guess corresponds to a disjunct from the following two equivalences:

These equivalences “perform” the symbolic division by $t$. In line 17, the algorithm substitutes the constraint $\eta \sim 0$ with the result of the division, that is, the conjunction of the quotient and the remaining part that is stored the formula $\gamma$ (lines 12–16). Observe a key property of $\gamma$: in it, all the coefficients of the $t$-digits $𝒚$ only have integer coefficients, i.e., $\mathrm{deg}(𝒚,\gamma )=0$.

Let ${\chi }_r$ be the formula obtained from $\phi$ by performing the replacement in line 17. This formula belongs to $R_{i+1}$ and, moreover, ${\phi }_{𝒔}\iff {\bigvee }_{r=-N}^N{\chi }_r$. We have $G=\{𝒔r:r\in [-N,N]\}$, and Item 14 is proved. To prove Item 14, observe that

$◀$

By inductively applying Lemma 14, we deduce that the while loop performs at most $\mathrm{deg}(𝒚,{\phi }_{\mathrm{\varnothing }})$ iterations, and that the disjunction (over all non-deterministic branches) of formulae ${\phi }_{𝒓}$ obtained at the end of this loop is equivalent to ${\phi }_{\mathrm{\varnothing }}$. The constraints in each ${\phi }_{𝒓}$ are (in)equalities $f(t)+\tau (𝒛)+{\sum }_{i=1}^{\mathrm{\ell }}{a}_i\cdot y_i\sim 0$, where $a_1,\mathrm{\dots },a_{\mathrm{\ell }}\in \mathbb{Z}$, $f\in \mathbb{Z}[t]$, all $y_1,\mathrm{\dots },y_{\mathrm{\ell }}$ are $t$-digits, and $\tau$ is a non-shifted term of $\text{PrA}[t]$.