Linear sifting of decision diagrams

Abstract

We propose a new algorithm, called linear sifting, for theoptimization of decision diagrams that combines the efficiency of sifting and the power of linear transformations. We show that the new algorithm is applicable to large examples, and that inmany cases it leads to substantiallymore compact diagrams when compared to simple variablereordering. We show inwhat sense linear transformationscomplement variable reordering, and we discuss applications of the new technique to synthesis and verification.