@inproceedings{Jarvisalo:CP2011,
 author = {Matti J\"arvisalo},
 title = {On the Relative Efficiency of {DPLL} and {OBDD}s with Axiom and Join},
 booktitle = {Proceedings of the 17th International Conference on 
	  Principles and Practice of Constraint Programming (CP 2011)},
 editor = {Jimmy Lee},
 series = {Lecture Notes in Computer Science},
 volume = {6876},
 pages = {429--437},
 year = {2011},
}

Abstract:

This paper studies the relative efficiency of ordered binary decision diagrams
(OBDDs) and the Davis-Putnam-Logemann-Loveland procedure (DPLL),
two of the main approaches to solving Boolean satisfiability instances. 
Especially, we show that OBDDs, even when constructed using only the rather 
weak axiom and join rules, can be exponentially more efficient than DPLL or, 
equivalently, tree-like resolution. Additionally, by strengthening via simple 
arguments a recent result—stating that such OBDDs do not polynomially simulate
unrestricted resolution—we also show that the opposite holds: there are cases 
in which DPLL is exponentially more efficient out of the two considered 
systems. Hence DPLL and OBDDs constructed using only the axiom and join rules 
are polynomially incomparable. This further highlights differences between 
search-based and compilation-based approaches to Boolean satisfiability.