A set of interacting finite state machines is often used as a model for formal verification. Most formal verification algorithms, based on Binary Decision Diagrams (BDD's), build the transition relation of the product machine, and then existentially quantify out the non-state variables. The early quantification problem is to compute a schedule for multiplying and existentially quantifying variables, such that the maximum size BDD encountered at any point is minimized. We give two algorithms for the early quantification problem, one which is rather fast (running in linear time on sparse structures), and produces excellent results and another which produces an optimal schedule for a given linear ordering of the terms. Even with early quantification partial products can become very large. In this paper, we present techniques to find don't cares, with respect to which the partial products are minimized. Some of our techniques involve state minimization and can result in smaller BDD's for the reachable states set. Two notions for state minimization are new, and involve approximations to trace equivalence. All the algorithms have been implemented and integrated in our formal verification software for design verification. We present our experimental results.