我在哪里可以找到将任意布尔表达式转换为连接或析取范式的方法？

Question

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

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

现在,转换为CNF或DNF是我一直手工完成的,以简化复杂的表达式.(好吧,也许不是所有的时间,但我确实知道如何使用例如demorgan的定律,分配定律等).但是,我不知道如何开始将其转换为可作为算法实现的方法.我看过有关查询优化的论文,有几篇以"首先我们把东西放入CNF"或"首先我们把东西放入DNF"开头,他们似乎从未解释过他们实现这一目标的方法.

我应该从哪里开始？

Answer 1

看看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)

Answer 2

对于无量词公式,天真的香草算法是:

• 对于CNF,使用De Morgan法则转换为否定正常形式,然后在AND上分配OR
• 对于DNF,使用De Morgan法则转换为否定正常形式,然后在OR上分配AND

如果你的公式是量化的,我不清楚.但即使它们不是,它似乎是维基百科关于联合正规形式的文章的结尾,它 - 在自动化的规范证明世界中大致相当 - clausal正规形式改变自我概述了一个可用的算法(并指出如果你想要的参考使这种转变更加聪明一点.如果您需要更多,请告诉我们您遇到困难的地方.

Answer 3

我遇到过这个页面：How to Convert a Formula to CNF。它以伪代码形式展示了将布尔表达式转换为 CNF 的算法。帮助我开始了解这个主题。