Abstract: In BDD-based model checking, it is a critical step to build a small and efficient transition relationship. An effective method is to partition it according to the bit of future state. The author proposed a strategy to group the partitioned transition relationship. The experiment conducted on the benchmark of ISCAS89 exhibits that our method is more effective under certain conditions.