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的桶消除法——一种使用变量消除的可满足性检验方法，该方法在过去已有若干实际实现。我们证明，在允许变量消除与BDD表示采用不同顺序这一近期提出的桶消除变体时，该方法能够高效求解标准鸽巢原理公式。此外，我们表明这一上界具有一定的脆弱性：对于通过限制（即固定部分变量）从鸽巢原理导出的公式，即使采用相同变量顺序的同一方法也会产生指数级运行时间。我们还证明，当采用上界中两种顺序中的任一种时，使用变量消除与BDD相同顺序的更为常见的桶消除实现对于鸽巢原理具有指数级运行时间，这表明两者的结合是该场景下高效性的关键。