Prevent blow-up with or operator

netom / satispy

An interface to SAT solver tools (like minisat)

Other

58 stars 17 forks source link

Prevent blow-up with or operator #12

Open yberman opened 6 years ago

yberman commented 6 years ago

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 commented 6 years ago

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.