子句包含算法

问：

自动定理证明的一个重要部分是通过弄清楚一个子句何时包含另一个子句来减少冗余。

直观地说，一个子句（CNF 中的一阶逻辑公式）C 包含另一个子句 D，当它至少是一般的。具体的定义是，必须用变量替换项，将 C 变成 D 的子多集（不是子集;这将让子句包含它自己的因子，这将破坏一些最佳饱和演算的完整性，例如叠加。

有一些索引技术可以大大减少必须进行的包含尝试次数，但即便如此，包含也会消耗大量的 CPU 时间，因此对其进行优化非常重要。显然，在一般情况下，它是已知的NP困难，但使大多数特定情况快速运行仍然是可能的，也是必要的。

以下伪代码正确但效率低下。（在实践中，否定和正文字必须分开处理，然后会出现一些问题，例如尝试双向方程，但在这里我只考虑匹配两袋文字的核心算法。

def match_clauses(c, d, map):
    if c == {}:
        return true
    for ci in c:
        for di in d:
            if match_terms(ci, di, map):
                if match_clauses(c - ci, d - di, map):
                    return true
    return false

为什么效率低下？考虑两个子句和 .上面的算法会先匹配成功，然后匹配成功，然后注意不匹配。好的，但是接下来它会以相反的方式尝试：首先成功匹配，然后成功匹配，然后再次通知不匹配。如果有 N 个文字匹配，则浪费的工作将是 N 阶乘的，在某些实际情况下，效率低下。p(x) | q(y) | r(42)p(x) | q(y) | r(54)p(x)q(y)r(42)r(54)q(y)p(x)r(42)r(54)

如果有足够的时间，我无疑可以想出一个更好的算法，但其他人一定在我之前做过，所以似乎值得一问：最著名的算法是什么？