Prevent blow-up with or operator

[yberman]

The library does distribution directly when ORing two CNFs together. This results in exponential blowup in certain cases

from satispy import Variable as v
reduce(lambda x, y: x|y, [v("x" + str(i)) & v("y" + str(i)) for i in range(100)])

Would it be within the scope of this libraries purpose to not do any algebraic simplifications until a solution is requested at which point it does https://en.wikipedia.org/wiki/Tseytin_transformation to produce a CNF?

[netom]

That's a good idea, and already did some research on the topic, but haven't implemented anything yet. I hope I can invest some time soon.