• English only

# 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)
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
</​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$.