The main challenge in BDD-based verification is dealing with the memory explosion problem during reachability analysis. In this paper we advocate a methodology to handle this problem based on state space partitioning of functions as well as relations. We investigate the key questions of how to perform partitioning in reachability based verification and provide suitable algorithms. We also address the problem of instability of BDD-based verification by automatically picking the best configuration from different short traces of the reachability computation. Our approach drastically decreases verification time, often by orders of magnitude.