Exponential space complexity for OBDD-based reachability analysis

摘要

Ordered binary decision diagrams (OBDDs) are one of the most common dynamic data structures for Boolean functions. Nevertheless, many basic graph problems are known to be PSPACE-hard if their input graphs are represented by OBDDs. Computing the set of nodes that are reachable from some source s ∈ V in a digraph G = (V, E) is an important problem in computer-aided design, hardware verification, and model checking. Until now only exponential lower bounds on the space complexity of a restricted class of OBDD-based algorithms for the reachability problem have been known. Here, the result is extended by presenting an exponential lower bound for the general reachability problem. As a byproduct a general exponential lower bound is obtained for the computation of OBDDs representing all connected node pairs in a graph, the transitive closure.