LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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*}
 ++++ ++++