子句包含算法

Question

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

直观地讲，子句（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

为什么效率低下？考虑两个子句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)。如果有N个文字确实匹配，那么浪费的工作将是N个阶乘，在某些实际情况下会严重降低效率。

如果有足够的时间，我无疑会想出一种更好的算法，但是其他人必须在我之前完成此操作，因此似乎值得一问：什么是最知名的算法？