Extended resolution simulates binary decision diagrams

AbstractWe 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 Mathematical Logics, 1968]. More precisely, for any unsatisfiable formula φ, there exists an extended resolution refutation of φ where the number of steps is polynomially bounded by the maximal size of the BDDs built from the formulae occurring in φ