ROBDD variable ordering

Question

Hello,

In problem 1.c page 7 of the 2021.02.17 VRS sheet solution, we see in the previous page the ROBDD are symmetric therefore the variable ordering doesn't impact or cause any different changes. But what if we get a function that is not symmetric? In this case, how should the variable ordering be? Should we choose an ordering and construct the ROBDD again?

Thank You.

Answer 1

In the worst case, yes, you may have to compute for the Boolean function a new BDD with the new variable ordering. However, you may do that incrementally using the swap operation that exchanges to neighboring variables in the variable order, and you may consider "local symmetries" like a&b -> c where a and b are symmetric in a certain sense.