Title: Symbolic OBDD-Based Reachability Analysis Needs Exponential Space
Abstract: 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. Despite the hardness results there are not many concrete nontrivial lower bounds known for the complexity of problems on OBDD-represented graph instances. Computing the set of vertices that are reachable from some predefined vertex s ∈ V in a directed graph 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 on the space complexity of an arbitrary OBDD-based algorithm for the reachability problem. As a by-product a general exponential lower bound is obtained for the computation of OBDDs representing all connected node pairs in a graph, the transitive closure.
Publication Year: 2010
Publication Date: 2010-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 3
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot