13

我编写了一个将表达式解析为抽象语法树的小应用程序。现在,我对表达式使用了一堆启发式方法来决定如何最好地评估查询。不幸的是,有些例子使查询计划非常糟糕。

我已经找到了一种可以证明更好地猜测应该如何评估查询的方法,但是我需要首先将我的表达式放入 CNF 或 DNF 中,以便获得可证明的正确答案。我知道这可能会导致潜在的指数时间和空间,但对于我的用户运行的典型查询,这不是问题。

现在,为了简化复杂的表达式,我一直手动转换为 CNF 或 DNF。(好吧,也许不是一直,但我确实知道这是如何使用例如德摩根定律、分配定律等来完成的。)但是,我不确定如何开始将其转换为可作为算法实现的方法。我看过关于查询优化的论文,有几篇以“首先我们将事物放入 CNF”或“首先我们将事物放入 DNF”开始,但他们似乎从未解释过他们实现这一目标的方法。

我应该从哪里开始?

4

3 回答 3

10

查看https://github.com/bastikr/boolean.py 示例:

def test(self):
    expr = parse("a*(b+~c*d)")
    print(expr)

    dnf_expr = normalize(boolean.OR, expr)
    print(list(map(str, dnf_expr)))

    cnf_expr = normalize(boolean.AND, expr)
    print(list(map(str, cnf_expr)))

输出是:

a*(b+(~c*d))
['a*b', 'a*~c*d']
['a', 'b+~c', 'b+d']

更新:现在我更喜欢这个sympy 逻辑包

>>> from sympy.logic.boolalg import to_dnf
>>> from sympy.abc import A, B, C
>>> to_dnf(B & (A | C))
Or(And(A, B), And(B, C))
>>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True)
Or(A, C)
于 2013-10-24T09:22:14.897 回答
9

对于无量词公式,朴素的香草算法是:

我不清楚你的公式是否被量化。但即使不是这样,维基百科关于合取范式的文章似乎也结束了,它——在自动定理证明器世界中大致等价——从句范式改变自我概述了一个可用的算法(如果你愿意,请指向参考资料使这种转换更加聪明)。如果您需要更多,请告诉我们更多关于您遇到困难的地方。

于 2011-11-03T11:41:37.857 回答
4

我遇到了这个页面:如何将公式转换为 CNF。它显示了在伪代码中将布尔表达式转换为 CNF 的算法。帮助我开始研究这个话题。

于 2016-10-18T09:41:40.847 回答