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:16] 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 53: | 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 resulting formula is then: \\ | + | The starting point after transformation to cardinality constraints is: \\ |
| <latex> | <latex> | ||
| k_1 = |A| \land \\ | k_1 = |A| \land \\ | ||
| Line 65: | Line 67: | ||
| k_5 = 0 | k_5 = 0 | ||
| </latex> | </latex> | ||
| - | |||
| ++++ | ++++ | ||