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:deciding_boolean_algebra_with_presburger_arithmetic [2010/05/10 18:15]
evka 		sav08:deciding_boolean_algebra_with_presburger_arithmetic [2011/04/11 10:48]
vkuncak
Line 28: Line 28:
  
 Semantics: we consider the theory of models where integers are interpreted as integers and sets are interpreted as subsets of some finite set.  For each finite set we have one interpretation. ​ (If we prove a valid formula, it will hold for arbitrarily large finite universes.) ​ $\mathbf{0},​\mathbf{1}$ are empty and universal set.  We interpret constant $maxc$ as $|\mathbf{1}|$. Semantics: we consider the theory of models where integers are interpreted as integers and sets are interpreted as subsets of some finite set.  For each finite set we have one interpretation. ​ (If we prove a valid formula, it will hold for arbitrarily large finite universes.) ​ $\mathbf{0},​\mathbf{1}$ are empty and universal set.  We interpret constant $maxc$ as $|\mathbf{1}|$.
 +
 +
 +
 +
 +
  
  
Line 50: Line 55:
 X \cup B = B \Rightarrow |(X \cup B) \cap B^c| = 0 \land |B \cap (X \cup B)^c| = 0 X \cup B = B \Rightarrow |(X \cup B) \cap B^c| = 0 \land |B \cap (X \cup B)^c| = 0
 \] \]
 +The starting point after transformation to cardinality constraints is: \\
 <​latex>​ <​latex>​
 k_1 = |A| \land \\ k_1 = |A| \land \\
-k_2 = |X \cap A| \land  +k_2 = |X \cap A| \land \\ 
-k_3 = |A \cap X^c| \land  +k_3 = |A \cap X^c| \land \\ 
-k_4 = |(X \cup B) \cap B^c| \land  +k_4 = |(X \cup B) \cap B^c| \land \\ 
-k_5 = |B \cap (X \cup B)^c| \land +k_5 = |B \cap (X \cup B)^c| \land \\
 k_2 = 2 k_1 + 1 \land  k_2 = 2 k_1 + 1 \land 
 k_3 = 0 \land  k_3 = 0 \land 
Line 61: Line 67:
 k_5 = 0 k_5 = 0
 </​latex>​ </​latex>​
- 
  
 ++++ ++++