Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:atomic_diagram_normal_form [2009/05/12 23:30] vkuncak |
sav08:atomic_diagram_normal_form [2009/05/12 23:33] vkuncak |
||
---|---|---|---|
Line 73: | Line 73: | ||
$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). | ||