Speeding up variable reordering of OBDDs

Abstract

The use of Ordered Binary Decision Diagrams (OB-DDs) as a representation of Boolean functions brought essential progress in many different applications. The optimization of the OBDD-size by the choice of the variable ordering is known to be NP-hard. The known heuristics for finding an initial ordering and for reordering still have insufficient performance. Rudell's sifting is one of the most successful reordering algorithms that is application independent and can be used dynamically. In this paper, we propose a method based on some communication complexity considerations that improves the time performance of the sifting. The main idea is to restrict the reordering of variables to blocks that are determined according to readily computable OBDD-measure. Experimental comparison of the proposed block-restricted sifting with the original algorithm shows a speed-up by factor two without any loss in the final size.