Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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$.
  
 
sav08/deciding_boolean_algebra_with_presburger_arithmetic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice