Exact minimisation of path-related objective functions for binary decision diagrams

Reduced ordered binary decision diagrams (BDDs) are a data structure for efficient representation and manipulation of Boolean functions. They are frequently used in logic synthesis and formal verification. In recent practical applications, BDDs are optimised with respect to new objective functions. The exact optimisation of BDDs with respect to path-related objective functions is investigated. First, the path-related criteria are studied in terms of sensitivity to variable ordering. Second, a deeper understanding of the computational effort of exact methods targeting the new objective functions is aimed at. This is achieved by an approach based on dynamic programming that generalises the framework of Friedman and Supowit. A prime reason for the computational complexity can be identified using this framework. For the first time, experimental results give the minimal expected path length of BDDs for benchmark functions. They have been obtained by an exact branch and bound method that can be derived from the general framework. The exact solutions are used to evaluate a heuristic approach. Apart from a few exceptions, the results prove the high quality of the heuristic solutions.