Quantifier Elimination for Presburger Arithmetic

(In the language over integers from Definition of Presburger Arithmetic.)

We consider elimination of a quantifier from a conjunction of literals (because QE from Conjunction of Literals Suffices).

Running example:

$\begin{equation*} \exists y. 3 y - 2 x + 1 > - x \land 2y - 6 < z \land 4 \mid 5y + 1 \end{equation*}$

Normalizing Conjunctions of Literals

We first show that we can bring conjunction of literals into a simpler form.

Normal Form of Terms

All terms are built from $K,+,-,K\cdot\_$ , so using standard transformations they can be represented as: K_0 + $\sum_{i=1}^n K_i x_i$

We call such term a linear term.

Normal Form for Literals

Relation symbols: $=$ , $<$ , $K|\_$ .

$\lnot (t_1 < t_2)$ becomes $t_2 < t_1 + 1$

$\lnot (t_1 = t_2)$ becomes $t_1 < t_2 \lor t_2 < t_1$

$t_1 = t_2$ becomes $t_1 < t_2 + 1 \land t_2 < t_1 + 1$

$\lnot (K \mid t)$ becomes $\displaystyle\bigvee_{i=1}^{K-1} K \mid t+i$

$t_1 < t_2$ becomes $0 < t_2 - t_1$

We obtain a disjunction of conjunctions of literals of the form $0 < t$ and $K \mid t$ where $t$ are of the form $K_0 + \sum_{i=1}^n K_i \cdot x_i$

Exposing the Variable to Eliminate

By previous transformations, we are eliminating $y$ from conjunction $F(y)$ of $0 < t$ and $K \mid t$ where $t$ is a linear term.

Coefficient next to $y$ : To eliminate $\exists y$ from such conjunction, we wish to ensure that the coefficient next to $y$ is one or minus one.

Observation: $0 < t$ is equivalent to $0 < c\, t$ and $K \mid t$ is equivalent to $c\, K \mid c\, t$ for $c$ a positive integer.

If $K_1,\ldots,K_n$ are all coefficients next to $y$ in the formula, let $M$ be a positive integer such that $K_i \mid M$ for all $i$ , $1 \le i \le n$ (for example, let $M$ be the least common multiple of $K_1,\ldots,K_n$ ). Multiply each literal where $y$ occurs in subterm $K_i y$ by constant $M/|K_i|$ .

What is the coefficient next to $y$ in the resulting formula? either $M$ or $-M$

We obtain a formula of the form $\exists y. F(M y)$ . Letting $x=My$ , we conclude the formula is equivalent to $\exists x. F(x) \land (M \mid x)$ .

What is the coefficient next to $y$ in the resulting formula? either $1$ or $-1$

Lower and upper bounds: Consider the coefficient next to $x$ in $0 < t$ . If it is $-1$ , move the term to left side. If it is $1$ , move the remaining terms to the left side. We obtain formula $F_1(x)$ of the form

$\begin{equation*} \bigwedge_{i=1}^L a_i < x \land \bigwedge_{j=1}^U x < b_j \land \bigwedge_{i=1}^D K_i \mid (x + t_i) \end{equation*}$

If there are no divisibility constraints ( $D=0$ ), what is the formula equivalent to?

Replacing variable by test terms: There is a an alternative way to express the above condition by replacing $F_1(x)$ with $\bigvee_k F_1(t_k)$ where $t_k$ do not contain $x$ . This is a common technique in quantifier elimination. Note that if $F_1(t_k)$ holds then certainly $\exists x. F_1(x)$ .

What are example terms $t_i$ when $D=0$ and $L > 0$ ? Hint: ensure that at least one of them evaluates to $\max a_i + 1$ .

What if $D > 0$ i.e. we have additional divisibility constraints?

What is $N$ ? least common multiple of $K_1,\ldots,K_D$

Note that if $F_1(u)$ holds then also $F_1(u-N)$ holds.

That's it for $L > 0$ .

What if $L=0$ ?

That's it!

Example

Consider verification condition from Symbolic Execution for Example Integer Program.

How can we prove such verification condition?

The invariant of this code example is : $F = (res + 2i = 2x \wedge i' = i - 1 \wedge res' = res + 2) \rightarrow res' + 2i' = 2x$

We have to find out if $\neg F$ is satisfiable.

$\exists res, res',i, i'. \neg F$

We can eliminate quantifiers with equalities: $i'= i-1$ and $res' = res + 2$

$res' + 2i'$ becomes $res + 2 + 2(i-1)$ , and $\exists i', res'$ can be removed

Finally :

$\exists res, i. \neg (res + 2i = 2x \rightarrow res + 2 + 2(i-1) = 2x)$
$\exists res, i. \neg (res + 2i = 2x \rightarrow res + 2i = 2x)$
$\exists res, i. \neg true$
$false$

Some Improvements

Avoid transforming to conjunctions of literals: work directly on negation-normal form.

the technique is similar to what we described for conjunctive normal form

This is the Cooper's algorithm

Reddy, Loveland: Presburger Arithmetic with Bounded Quantifier Alternation (gives a slight improvement of the original Cooper's algorithm)
Section 7.2 of the Calculus of Computation Textbook

References

The presentation in thes notes follows Appendix of this report, which also contains further references.

See Section 7.2 of the Calculus of Computation Textbook for a description of more efficient Cooper's algorithm.

A practical algorithm for exact array dependence analysis