# Differences

This shows you the differences between two versions of the page.

 sav08:deciding_boolean_algebra_with_presburger_arithmetic [2010/05/10 18:16]evka sav08:deciding_boolean_algebra_with_presburger_arithmetic [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2011/04/11 10:48 vkuncak 2010/05/10 18:16 evka 2010/05/10 18:16 evka 2010/05/10 18:16 evka 2010/05/10 18:15 evka 2010/05/10 18:15 evka 2010/05/10 18:14 evka 2010/05/10 18:13 evka 2010/05/10 18:13 evka 2010/05/10 18:07 evka 2010/05/10 13:04 vkuncak 2010/05/10 13:03 vkuncak 2010/05/10 13:02 vkuncak 2010/05/03 13:34 vkuncak 2010/05/03 12:01 vkuncak 2010/04/23 09:52 vkuncak 2009/04/23 10:51 vkuncak 2008/04/17 18:24 pedagand 2008/04/17 18:22 pedagand 2008/04/17 18:22 pedagand 2008/04/17 12:12 vkuncak 2008/04/17 12:10 vkuncak 2008/04/17 12:10 vkuncak 2008/04/17 12:10 vkuncak 2008/04/17 12:05 vkuncak 2008/04/17 12:01 vkuncak 2008/04/17 11:58 vkuncak Next revision Previous revision 2011/04/11 10:48 vkuncak 2010/05/10 18:16 evka 2010/05/10 18:16 evka 2010/05/10 18:16 evka 2010/05/10 18:15 evka 2010/05/10 18:15 evka 2010/05/10 18:14 evka 2010/05/10 18:13 evka 2010/05/10 18:13 evka 2010/05/10 18:07 evka 2010/05/10 13:04 vkuncak 2010/05/10 13:03 vkuncak 2010/05/10 13:02 vkuncak 2010/05/03 13:34 vkuncak 2010/05/03 12:01 vkuncak 2010/04/23 09:52 vkuncak 2009/04/23 10:51 vkuncak 2008/04/17 18:24 pedagand 2008/04/17 18:22 pedagand 2008/04/17 18:22 pedagand 2008/04/17 12:12 vkuncak 2008/04/17 12:10 vkuncak 2008/04/17 12:10 vkuncak 2008/04/17 12:10 vkuncak 2008/04/17 12:05 vkuncak 2008/04/17 12:01 vkuncak 2008/04/17 11:58 vkuncak 2008/04/17 11:56 vkuncak 2008/04/17 11:56 vkuncak 2008/04/16 22:47 vkuncak 2008/04/16 10:58 vkuncak created 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 43: 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 resulting formula ​is then: \\ + The starting point after transformation to cardinality constraints ​is: \\ <​latex>​ <​latex>​ k_1 = |A| \land \\ k_1 = |A| \land \\ Line 66: Line 67: k_5 = 0 k_5 = 0 ​ - ++++ ++++ 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$.