  We study BDD-based bucket elimination, an approach to satisfiability testing
using variable elimination which has seen several practical implementations in
the past. We prove that it allows solving the standard pigeonhole principle
formulas efficiently, when allowing different orders for variable elimination
and BDD-representations, a variant of bucket elimination that was recently
introduced. Furthermore, we show that this upper bound is somewhat brittle as
for formulas which we get from the pigeonhole principle by restriction, i.e.,
fixing some of the variables, the same approach with the same variable orders
has exponential runtime. We also show that the more common implementation of
bucket elimination using the same order for variable elimination and the BDDs
has exponential runtime for the pigeonhole principle when using either of the
two orders from our upper bound, which suggests that the combination of both is
the key to efficiency in the setting.
