Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:deciding_boolean_algebra_with_presburger_arithmetic [2011/04/11 10:48] vkuncak |
sav08:deciding_boolean_algebra_with_presburger_arithmetic [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 13: | Line 13: | ||
See [[http://lara.epfl.ch/~kuncak/papers/KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.pdf|Figure 3 on page 5 of the paper]] and compare to its special cases: BA and PA. | See [[http://lara.epfl.ch/~kuncak/papers/KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.pdf|Figure 3 on page 5 of the paper]] and compare to its special cases: BA and PA. | ||
- | \[ | + | \begin{equation*} |
\begin{array}{rcl} | \begin{array}{rcl} | ||
F & ::= & A \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid \lnot F \mid | F & ::= & A \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid \lnot F \mid | ||
Line 25: | Line 25: | ||
K & ::= & \ldots {-2} \mid -1 \mid 0 \mid 1 \mid 2 \ldots | K & ::= & \ldots {-2} \mid -1 \mid 0 \mid 1 \mid 2 \ldots | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
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 44: | Line 44: | ||
Eliminate the quantifier $X$ from the following formula: | Eliminate the quantifier $X$ from the following formula: | ||
- | \[ | + | \begin{equation*} |
\exists X. A \subseteq X \land X \cup B = B \land |X \cap A| = 2 |A| + 1 | \exists X. A \subseteq X \land X \cup B = B \land |X \cap A| = 2 |A| + 1 | ||
- | \] | + | \end{equation*} |
++++ | | ++++ | | ||
- | \[ | + | \begin{equation*} |
A \subseteq X \Rightarrow |A \cap X^c| = 0 | A \subseteq X \Rightarrow |A \cap X^c| = 0 | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
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 | ||
- | \] | + | \end{equation*} |
The starting point after transformation to cardinality constraints is: \\ | The starting point after transformation to cardinality constraints is: \\ | ||
<latex> | <latex> | ||
Line 81: | Line 81: | ||
Transform $b$ into union of disjoint Venn regions. Let $s_1,\ldots,s_m$ be all set variables. Venn regions are connected regions in the Venn diagram, and are analogous to conjunctive normal form: | Transform $b$ into union of disjoint Venn regions. Let $s_1,\ldots,s_m$ be all set variables. Venn regions are connected regions in the Venn diagram, and are analogous to conjunctive normal form: | ||
- | \[ | + | \begin{equation*} |
\bigcup_{i=1}^m x_i^{\alpha_i} | \bigcup_{i=1}^m x_i^{\alpha_i} | ||
- | \] | + | \end{equation*} |
where $x^\alpha$ is either $x$ or $x^c$ (complement of $x$). | where $x^\alpha$ is either $x$ or $x^c$ (complement of $x$). | ||
Line 89: | Line 89: | ||
Then use | Then use | ||
- | \[ | + | \begin{equation*} |
|b| = |s_{i_1}| + \ldots + |s_{i_k}| | |b| = |s_{i_1}| + \ldots + |s_{i_k}| | ||
- | \] | + | \end{equation*} |
We therefore assume that the only occurence of sets and set operators is within $|s|$ where $s$ is a Venn region. | We therefore assume that the only occurence of sets and set operators is within $|s|$ where $s$ is a Venn region. | ||
Line 98: | Line 98: | ||
Transform formula to prenex form | Transform formula to prenex form | ||
- | \[ | + | \begin{equation*} |
Q_p v_p. \dots Q_1 v_1. G_1(|s_1|,\ldots,|s_n|) | Q_p v_p. \dots Q_1 v_1. G_1(|s_1|,\ldots,|s_n|) | ||
- | \] | + | \end{equation*} |
where $F$ is quantifier-free. | where $F$ is quantifier-free. | ||
For each expression $|s_i|$ in $G_1(|s_1|,\ldots,|s_n|)$ introduce a fresh variable $l_i$ that denotes the value $|s_i|$. We obtain | For each expression $|s_i|$ in $G_1(|s_1|,\ldots,|s_n|)$ introduce a fresh variable $l_i$ that denotes the value $|s_i|$. We obtain | ||
- | \[ | + | \begin{equation*} |
Q_p v_p. \dots Q_1 v_1. \exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,\ldots,l_q) | Q_p v_p. \dots Q_1 v_1. \exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,\ldots,l_q) | ||
- | \] | + | \end{equation*} |
Note that $G_1(l_1,\ldots,l_q)$ is a quantifier-free PA formula. | Note that $G_1(l_1,\ldots,l_q)$ is a quantifier-free PA formula. | ||
Line 112: | Line 112: | ||
We will eliminate integer and set quantifiers from the entire subformula $Q_p v_p. \dots Q_1 v_1$ | We will eliminate integer and set quantifiers from the entire subformula $Q_p v_p. \dots Q_1 v_1$ | ||
- | \[ | + | \begin{equation*} |
\exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,\ldots,l_q) | \exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,\ldots,l_q) | ||
- | \] | + | \end{equation*} |
Indeed, we can always transform this formula to a quantifier-free formula by substituting $|s_i|$ back into $G_1$. | Indeed, we can always transform this formula to a quantifier-free formula by substituting $|s_i|$ back into $G_1$. | ||