LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:qe_for_presburger_arithmetic [2012/03/09 10:44]
vkuncak
sav08:qe_for_presburger_arithmetic [2015/04/21 17:30] (current)
Line 6: Line 6:
  
 Running example: Running example:
-\[+\begin{equation*}
     \exists y. 3 y - 2 x + 1 > - x  \land  2y - 6 < z \land 4 \mid 5y + 1     \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 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*}
 ++++ ++++