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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Balcázar, J.L., Lozano, A.: The Complexity of Graph Problems for Succinctly Represented Graphs. In: Nagl, M. (ed.) WG 1989. LNCS, vol. 411, pp. 277–285. Springer, Heidelberg (1990)
Bollig, B.: On the OBDD Complexity of the Most Significant Bit of Integer Multiplication. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol. 4978, pp. 306–317. Springer, Heidelberg (2008)
Bollig, B.: Larger Lower Bounds on the OBDD Complexity of Integer Multiplication. In: Dediu, A.H., Ionescu, A.M., Martín-Vide, C. (eds.) LATA 2009. LNCS, vol. 5457, pp. 212–223. Springer, Heidelberg (2009)
Bollig, B., Klump, J.: New Results on the Most Significant Bit of Integer Multiplication. In: Hong, S.-H., Nagamochi, H., Fukunaga, T. (eds.) ISAAC 2008. LNCS, vol. 5369, pp. 883–894. Springer, Heidelberg (2008)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers 35, 677–691 (1986)
Bryant, R.E.: On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. IEEE Trans. on Computers 40, 205–213 (1991)
Burch, J.R., Clarke, E.M., Long, D.E., Mc Millan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: Proc. of Symposium on Logic in Computer Science, pp. 428–439 (1990)
Coudert, O., Berthet, C., Madre, J.C.: Verification of Synchronous Sequential Machines Based on Symbolic Execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 365–373. Springer, Heidelberg (1990)
Feigenbaum, J., Kannan, S., Vardi, M.V., Viswanathan, M.: Complexity of Problems on Graphs Represented as OBDDs. In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol. 1373, pp. 216–226. Springer, Heidelberg (1998)
Galperin, H., Wigderson, A.: Succinct Representations of Graphs. Information and Control 56, 183–198 (1983)
Gentilini, R., Piazza, C., Policriti, A.: Computing Strongly Connected Components in a Linear Number of Symbolic Steps. In: Proc. of SODA, pp. 573–582. ACM Press, New York (2003)
Gentilini, R., Piazza, C., Policriti, A.: Symbolic Graphs: Linear Solutions to Connectivity Related Problems. Algorithmica 50, 120–158 (2008)
Hachtel, G.D., Somenzi, F.: A Symbolic Algorithm for Maximum Flow in 0 − 1 Networks. Formal Methods in System Design 10, 207–219 (1997)
Jukna, S.: The Effect of Null-Chains on the Complexity of Contact Schemes. In: Csirik, J.A., Demetrovics, J., Gecseg, F. (eds.) FCT 1989. LNCS, vol. 380, pp. 246–256. Springer, Heidelberg (1989)
Krause, M., Meinel, C., Waack, S.: Separating the Eraser Turing Machine Classes L e , NL e , co-NL e and P e . Theoretical Computer Science 86, 267–275 (1991)
Papadimitriou, C.H., Yannakakis, M.: A Note on Succinct Representations of Graphs. Information and Control 71, 181–185 (1986)
Sawitzki, D.: Implicit Flow Maximization by Iterative Squaring. In: Van Emde Boas, P., Pokorný, J., Bieliková, M., Štuller, J. (eds.) SOFSEM 2004. LNCS, vol. 2932, pp. 301–313. Springer, Heidelberg (2004)
Sawitzki, D.: Lower Bounds on the OBDD Size of Graphs of Some Popular Functions. In: Vojtáš, P., Bieliková, M., Charron-Bost, B., Sýkora, O. (eds.) SOFSEM 2005. LNCS, vol. 3381, pp. 298–309. Springer, Heidelberg (2005)
Sawitzki, D.: Algorithmik und Komplexität OBDD-repräsentierter Graphen. PhD Thesis, University of Dortmund, in German (2006)
Sawitzki, D.: Exponential Lower Bounds on the Space Complexity of OBDD-Based Graph Algorithms. In: Correa, J.R., Hevia, A., Kiwi, M. (eds.) LATIN 2006. LNCS, vol. 3887, pp. 781–792. Springer, Heidelberg (2006)
Sieling, D., Wegener, I.: NC-Algorithms for Operations on Binary Decision Diagrams. Parallel Processing Letters 48, 139–144 (1993)
Wegener, I.: Branching Programs and Binary Decision Diagrams – Theory and Applications. SIAM Monographs on Discrete Mathematics and Applications (2000)
Woelfel, P.: Symbolic Topological Sorting with OBDDs. Journal of Discrete Algorithms 4(1), 51–71 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bollig, B. (2010). Symbolic OBDD-Based Reachability Analysis Needs Exponential Space. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds) SOFSEM 2010: Theory and Practice of Computer Science. SOFSEM 2010. Lecture Notes in Computer Science, vol 5901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11266-9_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-11266-9_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11265-2
Online ISBN: 978-3-642-11266-9
eBook Packages: Computer ScienceComputer Science (R0)