@inbook{2fe775c121834105a6a0d98ea59bc8b5,
title = "The ROBDD size of simple CNF formulas",
abstract = "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.",
author = "Michael Langberg and Amir Pnueli and Yoav Rodeh",
year = "2003",
doi = "10.1007/978-3-540-39724-3_32",
language = "אנגלית",
isbn = "354020363X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "363--377",
editor = "Daniel Geist and Enrico Tronci",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "גרמניה",
}