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 的桶消元的界限

Bounds on BDD-Based Bucket Elimination

Probabilistic inference algorithms for finding the most probable explanation,
the maximum aposteriori hypothesis, and the maximum expected utility and for
updating belief are reformulated as an elimination--type algorithm called
bucket elimination. This emphasizes the principle common to many of the
algorithms appearing in that literature and clarifies their relationship to
nonserial dynamic programming algorithms. We also present a general way of
combining conditioning and elimination within this framework. Bounds on
complexity are given for all the algorithms as a function of the problem's
structure.

通过桶消元算法重新构建概率推理算法，实现寻找最可能解释、后验最大假设和最大期望效用以及更新信仰的功能，并在此框架内提供将条件和消元结合的通用方法。同时，通过问题结构给出了所有算法的复杂度界限。