Lab for Automated Reasoning and Analysis LARA

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:

We call such term a linear term.

Normal Form for Literals

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

$\lnot (t_1 < t_2)$ becomes

$\lnot (t_1 = t_2)$ becomes

$t_1 = t_2$ becomes

$\lnot (K \mid t)$ becomes

$t_1 < t_2$ becomes

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?

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?

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$?

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

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

 
sav08/qe_for_presburger_arithmetic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice