Abductive forgetting is removing variables from a logical formula while
maintaining its abductive explanations. It is defined in either of two ways,
depending on its intended application. Both differ from the usual forgetting,
which maintains consequences rather than explanations. Differently from that,
abductive forgetting from a propositional formula may not be expressed by any
propositional formula. A necessary and sufficient condition tells when it is.
Checking this condition is ¶{3}-complete, and is in ¶{4} if minimality of
explanations is required. A way to guarantee expressibility of abductive
forgetting is to switch from propositional to default logic. Another is to
introduce new variables.

该论文探讨了如何在维持其缩略模式的同时从逻辑公式中移除变量，其中，传统的遗忘方式维护的是后果而非解释。它提出了两种定义方式并确定了其表述的必要和充分条件，同时提出了两种切换途径以保证遗忘的表述性，即从命题逻辑切换到默认逻辑和引入新变量。

推理性遗忘

Abductive forgetting

We consider three graphs, $G_{7,3}$, $G_{7,4}$, and $G_{7,6}$, related to
Keller's conjecture in dimension 7. The conjecture is false for this dimension
if and only if at least one of the graphs contains a clique of size $2^7 =
128$. We present an automated method to solve this conjecture by encoding the
existence of such a clique as a propositional formula. We apply satisfiability
solving combined with symmetry-breaking techniques to determine that no such
clique exists. This result implies that every unit cube tiling of
$\mathbb{R}^7$ contains a facesharing pair of cubes. Since a faceshare-free
unit cube tiling of $\mathbb{R}^8$ exists (which we also verify), this
completely resolves Keller's conjecture.

本文利用命题公式编码和可满足性求解技术证明了 Keller 猜想在 7 维空间中成立，这意味着任何 7 维的单位立方体铺砌都存在面共享的对立方体，进一步解决该问题。

Keller 猜想的证明

The Resolution of Keller's Conjecture

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 问题，已有多项研究验证了其性能优势。