Where might I find a method to convert an arbitrary boolean expression into conjunctive or disjunctive normal form?

Question

I've written a little app that parses expressions into abstract syntax trees. Right now, I use a bunch of heuristics against the expression in order to decide how to best evaluate the query. Unfortunately, there are examples which make the query plan extremely bad.

I've found a way to provably make better guesses as to how queries should be evaluated, but I need to put my expression into CNF or DNF first in order to get provably correct answers. I know this could result in potentially exponential time and space, but for typical queries my users run this is not a problem.

Now, converting to CNF or DNF is something I do by hand all the time in order to simplify complicated expressions. (Well, maybe not all the time, but I do know how that's done using e.g. demorgan's laws, distributive laws, etc.) However, I'm not sure how to begin translating that into a method that is implementable as an algorithm. I've looked at papers on query optimization, and several start with "well first we put things into CNF" or "first we put things into DNF", and they never seem to explain their method for accomplishing that.

Where should I start?

Answer 1

Look at https://github.com/bastikr/boolean.py Example:

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

Output is:

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

UPDATE: Now I prefer this sympy logic package:

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