On thin Boolean functions and related optimum OBDD ordering

This paper investigates the optimum OBDD representation problem based on two classes of Boolean functions. The first class is defined by OBDDs, in which the number of non-terminal nodes is equal to the number of input variables. We refer to such OBDDs and their corresponding Boolean functions as thin OBDDs and thin Boolean functions. The second class is the thin factored Boolean functions, which is defined by factored forms with each variable appearing exactly once. Many interesting properties of these two classes of functions are presented. Based on which, a revised dynamic shortest cube first OBDD variable ordering algorithm is developed. This algorithm is shown to be optimum for thin factored Boolean functions