Reduced Ordered Binary Decision diagrams (ROBDDs) are nowadays one of the most common dynamic data structures for Boolean functions. Among the many areas of application are verification, model checking, and computer aided design. In the last few years, SAT checkers, based on the CNF representation of Boolean functions are getting more and more attention as an alternative to the ROBDD based methods. We show the difference between the CNF representation and the ROBDD representation in one of the most degenerate cases - random monotone 2CNF formulas. We examine this model and give almost matching lower and upper bounds for the ROBDD size in different cases, and show that as soon as the formulas are non-trivial the ROBDD size becomes exponential, thus showing perhaps one of the most fundamental advantages of SAT solvers over ROBDDs.
CHARME 2003