Efficient algorithms for the transformation between different types of binary decision diagrams

Abstract

The problem of transforming an FBDD (free binary decision diagram) P or a π′ OBDD (ordered binary decision diagram with respect to the variable ordering π′) P for the Boolean function f into the reduced π OBDD Q for f is considered. The algorithms run in time O(|P| |Q|log|Q|) (where, e.g., |P| is the size of P) and need space O(|P| +n·|Q|), if P may be an FBDD, or O(|P|+|Q|), if P is known to be an OBDD. The problem is important for the improvement of given variable orderings, e.g., by simulated annealing or genetic algorithms, and in the situation where incompatible representations of functions have to be made compatible.