Algorithms and Data Structures

The technique proposed in this chapter cannot exclusively be attributed to a single step in the design flow. Instead, the underlying techniques for Boolean function manipulation are adjusted to particular subsequent needs. Binary Decision Diagrams (BDDs) [Bry86] and solvers for the Boolean Satisfiability (SAT) problem [DP60, Coo71] are state of the art for Boolean function manipulation. Both approaches have individual advantages. In the past, many researchers have proposed techniques to improve the efficiency of these algorithms, e.g. in [MS96, BRB90, MMZ⁺01, Som01b, ES04].