We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧,∃,reordering) algorithms. We prove the first exponential lower bound of OBDD(∧,∃,reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧,∃,reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧,∃,reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHPnn+1 © 2024 Elsevier B.V., All rights reserved.