Perfect Hashing for State Spaces in BDD Representation

摘要

In this paper we design minimum perfect hash functions on the basis of BDDs that represent all reachable states S {is contained in} {0, l}~n. These functions are one-to-one on S and can be evaluated quite efficiently. Such hash functions are useful to perform search in a bitvector representation of the state space. The time to compute the hash value with standard operations on the BDD G is (n|G|), the time to compute the inverse is 0(n~2|G|). When investing O(n) bits per node, we arrive at O(|G|) preprocessing time and optimal time O(n) for ranking and unranking.