Variable ordering for BDDs has been extensively investigated. Recently, sampling based ordering techniques have been proposed to overcome problems with structure based static ordering methods and sifting based dynamic reordering techniques. However, existing sampling techniques can lead to an unacceptably large deviation in the size of the final BDD. In this paper, we propose a new technique based on abstract BDDs (aBDDs) that does not suffer from this problem. This new technique, easy to implement and automate, consistently creates high quality variable orderings for both combinational as well as sequential functions. Experimental results show that for many applications our approach is significantly superior to existing techniques.
Yuan Lu, Jawahar Jain, Edmund M. Clarke, Masahiro