Regarding swap operation on variables for ROBDD

Question

Can someone let me know, is there any specific method to be followed to perform the swap operation on specific variables by changing the variable ordering of the ROBDD?

Answer 1

versucht man die wahrheitstabelle wieder zu erstellen und dann die variableordnung zu tauschen um den neuen robbd zu machen

Answer 2

If you need to switch variables b and c, you must consider the subtrees starting with b and their subtrees following c. In general, you consider then a subtree

(b ? (c?T11:T10) : (c?T01:T00) )

with four possible subtrees T11, T10, T01 and T00 that are reached when b and c have the corresponding values. If you swap the variables b and c, you simply get

(c ? (b?T11:T01) : (b?T10:T00) )

Hence, T10 and T01 are exchanged as shown on slide 75 of the BDD chapter.

You have to do this operation on all subtrees starting with b.