Abstract
Dynamic BDD reordering is usually a computationally-demanding process, and may slow down BDD-based applications. We propose a novel algorithm for distributing this process over a number of computers, improving both reordering time and application time. Our algorithm is based on Rudell's popular sifting algorithm, and takes advantage of a few empirical observations we make regarding Rudell's algorithm. Experimental results show the efficiency and scalability of our approach, when applied within an industrial model checker. Copyright 2006 ACM.