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 09:44]
vkuncak 		sav08:qe_for_presburger_arithmetic [2012/03/09 10:44]
vkuncak
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: 
 +\[ 
 +    \exists y. 3 y - 2 x + 1 > - x  \land  2y - 6 < z \land 4 \mid 5y + 1 
 +\]
  
 ===== 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 97: Line 98:
 We first drop all constraints except divisibility,​ obtaining $F_2(x)$ We first drop all constraints except divisibility,​ obtaining $F_2(x)$
 \[ \[
-   ​\bigwedge_{i=1}^D K_i \mid (x_i + t_i)+   ​\bigwedge_{i=1}^D K_i \mid (x + t_i)
 \] \]
 and then eliminate quantifier as and then eliminate quantifier as
Line 131: Line 132:
 $\exists res, i. \neg true$\\ $\exists res, i. \neg true$\\
 $false$ $false$
 +
 +
  
 ===== Some Improvements ===== ===== Some Improvements =====
  
 Avoid transforming to conjunctions of literals: work directly on negation-normal form. Avoid transforming to conjunctions of literals: work directly on negation-normal form.
 +  * the technique is similar to what we described for conjunctive normal form
  
-See Section 7.2 of the [[Calculus of Computation Textbook]]. +This is the Cooper'​s algorithm 
 +  * {{sav09:​reddyloveland78presburgerboundedalternation.pdf|Reddy,​ Loveland: Presburger Arithmetic with Bounded Quantifier Alternation}} (gives a slight improvement of the original Cooper'​s algorithm) 
 +  * Section 7.2 of the [[Calculus of Computation Textbook]]
  
 ===== References ===== ===== References =====