Differences

This shows you the differences between two versions of the page.

--- sav08:qe_for_presburger_arithmetic [2009/04/23 14:51]
vkuncak
+++ sav08:qe_for_presburger_arithmetic [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== 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]]).
-===== 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
-\[
-   \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)
-\]
-If there are no divisibility constraints ($D=0$), what is the formula equivalent to?
-++++|
-\[
-    \max_i a_i + 1 \le \min_j b_j - 1
-\]
-which is equivalent to
-\[
-    \bigwedge_{ij} a_i + 1 < b_j
-\]
-++++
-**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$.
-++++|
-\[
-   \bigvee_{k=1}^L F_1(a_k + 1)
-\]
-++++
-What if $D > 0$ i.e. we have additional divisibility constraints?
-++++|
-\[
-   \bigvee_{k=1}^L \bigvee_{i=1}^N F_1(a_k + i)
-\]
-++++
-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$?
-++++|
-We first drop all constraints except divisibility, obtaining $F_2(x)$
-\[
-   \bigwedge_{i=1}^D K_i \mid (x + t_i)
-\]
-and then eliminate quantifier as
-\[
-   \bigvee_{i=1}^N F_2(i)
-\]
-++++
-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
-  * {{sav09:reddyloveland78presburgerboundedalternation.pdf|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 [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard04FirstOrderTheorySetsCardinalityConstraintsDecidable.pdf|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.
-[[http://doi.acm.org/10.1145/135226.135233|A practical algorithm for exact array dependence analysis]]