Differences

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

--- sav08:atomic_diagram_normal_form [2009/05/12 23:33]
vkuncak
+++ sav08:atomic_diagram_normal_form [2009/05/13 10:44]
vkuncak
@@ Line 49: / Line 49: @@
   * $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.
 ===== Atomic Diagram Normal Form =====
@@ Line 74: / Line 75: @@
 $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
+\[
+    x = y \land x \neq z
+\]
+or, if we include all atomic formulas:
+\[
+    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
+\]
+The number of partitions is given by [[wp>Bell number]]s.