Symbolic state space exploration techniques for Finite State Machines (FSMs) are a major recent result in CAD for VLSI. Most of them are exact and based on forward traversal, but limited to medium-size circuits. Approximate forward traversal deals with bigger circuits at the expense of exactness. Backward traversal takes into account many irrelevant, unreachable states. This paper combines the advantages of approximate forward traversal and of exact backward traversal. Cofactoring plays a key role in ecient function simplication. For the rst time, we are able to symbolically manipulate some of the larger ISCAS'89 and MCNC circuits in an exact way and to generate test patterns for them. 1 2