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

我写过一个小应用程序 https://bitbucket.org/BillyONeal/pevfind/overview将表达式解析为抽象语法树。现在，我对表达式使用一系列启发式方法来决定如何最好地评估查询。不幸的是，有些例子使查询计划变得非常糟糕。

我找到了一种方法，可以证明对如何评估查询做出更好的猜测，但我需要首先将我的表达式放入 CNF 或 DNF 中，以获得可证明正确的答案。我知道这可能会导致时间和空间呈指数级增长，但对于我的用户运行的典型查询来说，这不是问题。

现在，为了简化复杂的表达式，我一直手动转换为 CNF 或 DNF。 （嗯，也许不是每时每刻，但我确实知道如何使用例如德摩根定律、分配律等）但是，我不确定如何开始将其转化为可作为算法实现的方法。我看过有关查询优化的论文，其中有几篇以“首先我们将内容放入 CNF”或“首先我们将内容放入 DNF”开头，但他们似乎从未解释过实现这一目标的方法。

我应该从哪里开始？

Look at https://github.com/bastikr/boolean.py 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']

UPDATE: 现在我更喜欢这个sympy 逻辑包 http://docs.sympy.org/latest/modules/logic.html:

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