Differences
This shows you the differences between two versions of the page.
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*} |
++++ | ++++ | ||