There are two problems involved in simplifying formulas containing negations. Converting such formulas to disjunctive normal form can lead to an explosive growth in the size of the formula. This leads previous algorithms for computing value-based data dependences to have poor performance on many real-world FORTRAN codes [MAL93][Fea91]. Secondly, previous techniques for negating non-convex constraints, based on quasilinear constraints [AI91], were discovered to be incomplete in certain pathological cases [PW93b]. We [PW93b] provide methods for dealing with both of these problems.