Different BDD equivalent

Question

One way is to find phi1 and phi2 and make SNF. But it will be time consuming to make SNf for both.

And I can't really understand how to reduce the formula, is there any other method to solve further after getting phi1 and phi2 formula?

Answer 1

Well, there are a lot of ways how to check the equivalence of formulas, and each one of them can be used here, once you read the Boolean functions from the two BDDs. An alternative would be to apply the swap operation to swap variables x1 and x2 in the ordering that must convert one BDD into the other one. 

However, the simplest way would be to compare the high- and low-subtrees of the root node. As high-subtrees, you find x2&!x1 | !x2 and !x1 | x1&!x2 which are same which you can see by a Shannon decomposition of both:

• x2&!x1 | !x2 = (x1 => !x2 | 1)
• !x1 | x1&!x2 = (x1 => !x2 | 1)

Same way, the low-trees are x2&x1 in both cases, and therefore trivially the same.

Comments

Thank you so much.