LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:atomic_diagram_normal_form [2009/05/12 23:33]
vkuncak
sav08:atomic_diagram_normal_form [2015/04/21 17:30] (current)
Line 7: Line 7:
  
 By introducing fresh variables, each conjunction of literals can be represented as an equisatisfiable conjunction of only "flat literals",​ which are flat atomic formulas or their negation, where flat atomic formula is By introducing fresh variables, each conjunction of literals can be represented as an equisatisfiable conjunction of only "flat literals",​ which are flat atomic formulas or their negation, where flat atomic formula is
-\[+\begin{equation*}
    ​R(y_1,​\ldots,​y_n)    ​R(y_1,​\ldots,​y_n)
-\] +\end{equation*} 
-\[+\begin{equation*}
     x = y     x = y
-\] +\end{equation*} 
-\[+\begin{equation*}
     x = f(y_1,​\ldots,​y_n)     x = f(y_1,​\ldots,​y_n)
-\]+\end{equation*}
 We call this "flat form" of the conjunction of literals. ​ (We can also eliminate $x \neq f(y_1,​\ldots,​y_n)$ if needed.) We call this "flat form" of the conjunction of literals. ​ (We can also eliminate $x \neq f(y_1,​\ldots,​y_n)$ if needed.)
  
 Rewrite rule that describes this transformation:​ Rewrite rule that describes this transformation:​
-\[+\begin{equation*}
     C[t] \ \ \leadsto \ \ (x=t) \land C[x]     C[t] \ \ \leadsto \ \ (x=t) \land C[x]
-\]+\end{equation*}
  
 **Example:​** Represent ​ $f(x)+y < z$ as **Example:​** Represent ​ $f(x)+y < z$ as
-\[+\begin{equation*}
     x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z     x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z
-\]+\end{equation*}
  
  
Line 49: Line 49:
   * $x<x$, $y<y$, $z<z$, $x<y$, $y<x$, $x<z$, $z<x$, $y<z$, $z<y$   * $x<x$, $y<y$, $z<z$, $x<y$, $y<x$, $x<z$, $z<x$, $y<z$, $z<y$
 and there are 3^2+3^2=18 atomic formulas. and there are 3^2+3^2=18 atomic formulas.
 +
  
 ===== Atomic Diagram Normal Form ===== ===== Atomic Diagram Normal Form =====
Line 61: Line 62:
  
 Note: if we simply guess all possible conjunctions of literals and negations, some of them will be unsatisfiable in the theory. ​ Those are useless and we should eliminate them.  For example, if we consider equality literals, then  Note: if we simply guess all possible conjunctions of literals and negations, some of them will be unsatisfiable in the theory. ​ Those are useless and we should eliminate them.  For example, if we consider equality literals, then 
-\[+\begin{equation*}
     x \neq z \land y = z \land x = y     x \neq z \land y = z \land x = y
-\]+\end{equation*}
 is unsatisfiable. ​ Only those conjunctions of equality literals can be satisfiable that correspond to an equivalence relations on variables. ​ Such conjunction of literals that corresponds to an equivalence relation is called **arrangement** in the context of combination techniques. is unsatisfiable. ​ Only those conjunctions of equality literals can be satisfiable that correspond to an equivalence relations on variables. ​ Such conjunction of literals that corresponds to an equivalence relation is called **arrangement** in the context of combination techniques.
  
Line 74: Line 75:
 $C \leadsto \bigvee_i C \land Ar_i$ $C \leadsto \bigvee_i C \land Ar_i$
  
-**Example:​** In last example, there are $2^{18}$ disjuncts to consider. If relations have special properties many cases are unsatisfiable and can be ignored. Nevertheless,​ the number of satisfiable atomic diagram formulas is typically exponential. For example, if we have only equality symbol, each partition of the set of variables gives one satisfiable formula (asserting that elements in same partition are equal, in different partitions disequal).+**Example:​** In last example, there are $2^{18}$ disjuncts to consider. If relations have special properties many cases are unsatisfiable and can be ignored. Nevertheless,​ the number of satisfiable atomic diagram formulas is typically exponential. ​ 
 + 
 +For example, if we have only equality symbol, each partition of the set of variables gives one satisfiable formula (asserting that elements in same partition are equal, in different partitions disequal). Partition $\{\{x,​y\},​\{z\}\}$ gives formula 
 +\begin{equation*} 
 +    x = y \land x \neq z 
 +\end{equation*} 
 +or, if we include all atomic formulas: 
 +\begin{equation*} 
 +    x = y \land y = x \land  
 +    x \neq z \land z \neq x \land y \neq z \land z \neq y \land 
 +    x = x \land  y = y \land z=z 
 +\end{equation*} 
 +The number of partitions is given by [[wp>​Bell number]]s.