Regarding Exercise Sheet 2: Reading Shannon Form from the VRS Online Tools

Question

Hello everybody,

in order to check whether my solutions are right I would like to use the vrs online tool for getting Shannon Normal Form, however I can not really see how to read them. As example I have the given formula a & (a->b) from the lecture. With transforming we get (a => (b=>1|0) | 0). And I see that.

The online tool gives me

(b ? (a ? true
            : false)
       : false)

and I additionally have the Shannon graph showing up. Would some one mind helping me out with this?

Answer 1

Well, it is just another syntax which is the one typically used in programming languages. Your example is (b => (a => 1|0) | 0).

The Shannon graph is not that useful for generating the SNF, since it is just a BDD which is neither ordered nor reduced. However, you may use the BDD instead (best let the tool print both leaf nodes).

Comments

For my understandings, we just switch the order of the variables but maintain of course the semantics. With this we can read this like a BDD but from the bottom up, in terms of variable? With the example formula, starting now in with b and then a?

---

Well. b is outside in this SNF, a is inside. So b has the higher variable ordering. If we draw a BDD, we draw it top to bottom while reading the SNF from the outside.

You can change the variable ordering. Then you'd start with a. (a => … | 0) Then you'd continue for the remaining formula (1 & (1->b)) and variable b. This would yield (a => (b => 1|0) | 0).

---

Thank you very much for clarifying this.