• English only

# 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] (current)
Line 5: Line 5:
We consider elimination of a quantifier from a conjunction of literals (because [[QE from Conjunction of Literals Suffices]]). 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 ===== ===== Normalizing Conjunctions of Literals =====
Line 32: Line 35:

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$ 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 ===== ===== Exposing the Variable to Eliminate =====
Line 55: Line 55:
**Lower and upper bounds:** **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 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_{i=1}^L a_i < x \land ​\bigwedge_{j=1}^U x < b_j \land ​\bigwedge_{j=1}^U x < b_j \land ​\bigwedge_{i=1}^D K_i \mid (x + t_i) ​\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? If there are no divisibility constraints ($D=0$), what is the formula equivalent to?
++++| ++++|
-$+\begin{equation*} \max_i a_i + 1 \le \min_j b_j - 1 \max_i a_i + 1 \le \min_j b_j - 1 -$+\end{equation*}
which is equivalent to which is equivalent to
-$+\begin{equation*} \bigwedge_{ij} a_i + 1 < b_j \bigwedge_{ij} a_i + 1 < b_j -$+\end{equation*}
++++ ++++

Line 76: Line 76:
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 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$.
++++| ++++|
-$+\begin{equation*} ​\bigvee_{k=1}^L F_1(a_k + 1) ​\bigvee_{k=1}^L F_1(a_k + 1) -$+\end{equation*}
++++ ++++

What if $D > 0$ i.e. we have additional divisibility constraints?​ What if $D > 0$ i.e. we have additional divisibility constraints?​
++++| ++++|
-$+\begin{equation*} ​\bigvee_{k=1}^L \bigvee_{i=1}^N F_1(a_k + i) ​\bigvee_{k=1}^L \bigvee_{i=1}^N F_1(a_k + i) -$+\end{equation*}
++++ ++++

Line 97: Line 97:
++++| ++++|
We first drop all constraints except divisibility,​ obtaining $F_2(x)$ We first drop all constraints except divisibility,​ obtaining $F_2(x)$
-$+\begin{equation*} ​\bigwedge_{i=1}^D K_i \mid (x + t_i) ​\bigwedge_{i=1}^D K_i \mid (x + t_i) -$+\end{equation*}
and then eliminate quantifier as and then eliminate quantifier as
-$+\begin{equation*} ​\bigvee_{i=1}^N F_2(i) ​\bigvee_{i=1}^N F_2(i) -$+\end{equation*}
++++ ++++