Lab for Automated Reasoning and Analysis 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*}
 ++++ ++++
  
 
sav08/qe_for_presburger_arithmetic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice