Optimization in Cnf solves the problem of huge redundancy

[Javantea]

Writeup When working with very simple equations like the below, satispy will use excessive memory holding unnecessary statements. For example:

    import satispy
    a = satispy.Variable('a')
    b = satispy.Variable('b')
    c = satispy.Variable('c')
    e = satispy.Variable('e')
    d = -((((a ^ b) & c) ^ a) ^ e)

This patch fixes that problem. The function reduceCnf describes what it does, removing any clause with (a | -a).

The class NaiveCnf preserves the previous functionality for testing and uses that require optimization be turned off.

[netom]

Somathing like the Tseitin transformation (https://en.wikipedia.org/wiki/Tseitin_transformation) would be even better for transforming arbitrary expressions to CNF.

If you'll ever had the time & patience... ;)