Extended resolution simulates binary decision diagrams Original Research Article

We prove that binary decision diagrams [R. Bryant, Symbolic Boolean manipulation with ordered binary decision diagrams, ACM Comput. Surveys 23 (3) (1992)] can be polynomially simulated by the extended resolution rule of [G.S. Tseitin, On the complexity of derivation in propositional calculus, in: A. Slisenko (Ed.), Studies in Constructive Mathematics and Mathe