Resolution and binary decision diagrams cannot simulate each other polynomially

There are many dierent ways of proving formulas in proposition logic. Many of these can easily be characterized as forms of resolution (e.g. [12] and [9]). Others use so-called binary decision diagrams (BDDs) [2, 10]. Experimental evidence suggests that BDDs and resolution based techniques are fundamentally dierent, in the sense that their performance can dier very much on benchmarks [14]. In this paper we conrm these ndings by mathematical proof. We provide examples that are easy for BDDs and exponentially hard for any form of resolution, and vice versa, examples that are easy for resolution and exponentially hard for BDDs.