Four algorithms for propositional forgetting are compared. The first performs
all possible resolutions and deletes the clauses containing a variable to
forget. The second forgets a variable at time by resolving and then deleting
all clauses that resolve on that variable. The third outputs the result of all
possible linear resolutions on the variables to forget. The fourth generates a
clause from the points of contradiction during a backtracking search. The
latter emerges as the winner, with the second and first having some role in
specific cases. The linear resolution algorithm performs poorly in this
implementation.

本文比较了四种命题遗忘算法的性能表现，其中通过回溯搜索方法生成矛盾点的算法获得最佳效果，第二种和第一种算法在特定情况下有所作用，而线性分辨算法的表现较差。

命题遗忘的四种算法

Four algorithms for propositional forgetting

Inference in Bayes Nets (BAYES) is an important problem with numerous
applications in probabilistic reasoning. Counting the number of satisfying
assignments of a propositional formula (#SAT) is a closely related problem of
fundamental theoretical importance. Both these problems, and others, are
members of the class of sum-of-products (SUMPROD) problems. In this paper we
show that standard backtracking search when augmented with a simple memoization
scheme (caching) can solve any sum-of-products problem with time complexity
that is at least as good any other state-of-the-art exact algorithm, and that
it can also achieve the best known time-space tradeoff. Furthermore,
backtracking's ability to utilize more flexible variable orderings allows us to
prove that it can achieve an exponential speedup over other standard algorithms
for SUMPROD on some instances.
The ideas presented here have been utilized in a number of solvers that have
been applied to various types of sum-of-product problems. These system's have
exploited the fact that backtracking can naturally exploit more of the
problem's structure to achieve improved performance on a range of
probleminstances. Empirical evidence of this performance gain has appeared in
published works describing these solvers, and we provide references to these
works.

使用简单的记忆化方案可以将标准回溯搜索与最先进的精确算法相混合，以更好的时间复杂度解决任何 sum-of-products 问题，并且具有最佳的时间空间权衡，并且这种方法可以实现其他标准算法的指数加速，适用于各种类型的 sum-of-product 问题，已有多项研究验证了其性能优势。