Differences
This shows you the differences between two versions of the page.
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 51: | 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 \\ | ||
Line 62: | Line 67: | ||
k_5 = 0 | k_5 = 0 | ||
</latex> | </latex> | ||
- | |||
++++ | ++++ |