BDD-based symbolic techniques of approximate reachability analysis
based on decomposing the circuit into a collection of overlapping
sub-machines (also referred to as {\em overlapping projections}) have
been recently proposed. Computing a superset of the reachable states
in this fashion is susceptible to false negatives. Searching for real
counterexamples in such an approximate space is liable to
failure. In this paper, the ``hybridization effect'' induced by the
choice of projections is identified as the cause for the failure. A
heuristic based on Hamming Distance is proposed to improve the choice
of projections, that reduces the hybridization effect and facilitates
either a genuine counterexample or proof of the property. The ideas
are evaluated on a real large design example from the PCI Interface
unit in the MAGIC chip of the Stanford FLASH
Multiprocessor.