An improved data parallel algorithm for Boolean function manipulation using BDDs

This paper describes a data-parallel algorithm for boolean function manipulation. The algorithm adopts Binary Decision Diagrams (BDDs), which are the state-of-the-art approach for representing and handling boolean functions. The algorithm is well suited for SIMD architectures and is based on distributing BDD nodes among the available Processing Elements and traversing BDDs in a breadth-first manner. An improved version of the same algorithm is also presented, which does not use virtual processors. A prototypical package has been implemented and its behavior has been studied with two different applications. In both cases the results show that the approach exploits well the parallel hardware by effectively, distributing the load; thanks to the limited CPU time required and to the great amount of memory available, it can solve problems that can not be faced with by conventional architectures