More efficient to_cnf

to_cnf needs to be more efficient. For some expressions, it takes forever and produces huge expressions, which tend to have tons of unnecessary clauses (lots of x | ~x).

I googled, and http://gauss.ececs.uc.edu/Courses/c626/lectures/BDD/st.pdf looks like it might be an algorithm. Any kind of optimization would probably help. Right now, it just does the naive distribution.