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.

本文研究了基于BDD的bucket elimination方法，证明该方法能高效地解决常见数学原理公式，但其时间复杂度对于该公式的某种变种（即通过限制一些变量得到的公式）是指数级的。同时，我们还发现通常版本的bucket elimination对于pigeonhole原理具有指数级运行时间，而不同顺序的变量消元和BDD-representations的组合是提高效率的关键。

基于BDD的桶消元的界限