• 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) Both sides previous revision Previous revision 2012/03/09 10:44 vkuncak 2009/04/23 14:51 vkuncak 2009/04/23 09:57 vkuncak 2009/04/23 09:55 vkuncak 2009/04/23 09:44 vkuncak 2009/04/23 09:44 vkuncak 2009/04/23 09:27 vkuncak 2009/04/21 19:41 vkuncak 2009/04/21 19:39 vkuncak 2009/04/21 19:38 vkuncak 2008/04/21 21:51 david 2008/04/21 21:49 david 2008/04/21 21:46 david 2008/04/21 21:45 david 2008/04/21 21:43 david 2008/04/17 10:42 david 2008/04/16 18:20 vkuncak 2008/04/16 10:43 vkuncak 2008/04/16 10:43 vkuncak 2008/04/16 10:24 vkuncak 2008/04/16 10:23 vkuncak 2008/04/16 10:19 vkuncak 2008/04/16 10:18 vkuncak 2008/04/16 00:06 vkuncak 2008/04/15 23:51 vkuncak 2008/04/15 23:51 vkuncak 2008/04/15 23:51 vkuncak Next revision Previous revision 2012/03/09 10:44 vkuncak 2009/04/23 14:51 vkuncak 2009/04/23 09:57 vkuncak 2009/04/23 09:55 vkuncak 2009/04/23 09:44 vkuncak 2009/04/23 09:44 vkuncak 2009/04/23 09:27 vkuncak 2009/04/21 19:41 vkuncak 2009/04/21 19:39 vkuncak 2009/04/21 19:38 vkuncak 2008/04/21 21:51 david 2008/04/21 21:49 david 2008/04/21 21:46 david 2008/04/21 21:45 david 2008/04/21 21:43 david 2008/04/17 10:42 david 2008/04/16 18:20 vkuncak 2008/04/16 10:43 vkuncak 2008/04/16 10:43 vkuncak 2008/04/16 10:24 vkuncak 2008/04/16 10:23 vkuncak 2008/04/16 10:19 vkuncak 2008/04/16 10:18 vkuncak 2008/04/16 00:06 vkuncak 2008/04/15 23:51 vkuncak 2008/04/15 23:51 vkuncak 2008/04/15 23:51 vkuncak 2008/04/15 23:21 vkuncak 2008/04/15 23:21 vkuncak 2008/04/15 22:38 vkuncak 2008/04/15 22:27 vkuncak 2008/04/15 21:49 vkuncak 2008/04/15 21:48 vkuncak 2008/04/15 21:48 vkuncak 2008/04/15 21:44 vkuncak 2008/04/15 20:55 vkuncak 2008/04/15 20:50 vkuncak created 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*} ++++ ++++