Binary Decision Diagrams - A Representation of Boolean Functions

Programs, are a graphic representation of Boolean functions. They are
considered in complexity theory and in applications like hardware
design and verification. In complexity theory the goal of the
investigation of BDDs is the proof of lower bounds on the BDD size for
explicitly defined functions because such lower bounds imply lower
bounds on the sequential space complexity of those functions.
However, good lower bound methods are only known for restricted
variants of BDDs. In applications restricted BDDs are used as a data
structure for the representation and manipulation of Boolean
functions. The goal is the design of efficient algorithms for
operations on Boolean functions represented by BDDs or the proof that
such algorithms are unlikely to exist. The results from complexity
theory complement the results from applications. Lower bound proofs
help to judge which BDD variant is a suitable data structure for which
kind of functions. On the other hand, applications of BDDs motivate
the research on new BDD variants.

In the talk a short introduction to BDDs is given. Afterwards, two
results are presented as examples of current research on BDDs: When
using BDDs as a data structure, it is important to minimize the size
of the representation of the considered function. It is shown that
for the minimization of OBDDs (Ordered BDDs), there is no polynomial
time approximation algorithm with any constant performance ratio
unless P=NP. Hence, only heuristics for OBDD minimization can be used
in practice. As an example of a result concerning lower bound methods
the proof of exponential lower bounds for so-called linearly
transformed OBDDs (LTOBDDs) is considered. Finally, some open
questions and directions for future research are discussed.