Abstract
We present a symbolic OBDD algorithm for topological sorting which requires O(log2 N) OBDD operations. Then we analyze its true runtime for the directed grid graph and show an upper bound of O(log4 N). This is the first true runtime analysis of a symbolic OBDD algorithm for a fundamental graph problem, and it demonstrates that one can hope that the algorithm behaves well for sufficiently structured inputs.
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
Breitbart, Y., Hunt III, H.B., Rosenkrantz, D.J.: On the size of binary decision diagrams representing boolean functions. Theor. Comp. Sci. 145, 45–69 (1995)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inform. and Comp. 98, 142–170 (1992)
Cho, H., Hachtel, G., Jeong, S.-W., Plessier, B., Schwarz, E., Somenzi, F.: ATPG aspects of FSM verification. In: IEEE Int. Conf. on CAD, pp. 134–137 (1990)
Cho, H., Jeong, S.-W., Somenzi, F., Pixley, C.: Synchronizing sequences and symbolic traversal techniques in test generation. Journal of Electronic Testing: Theory and Applications 4, 19–31 (1993)
Hachtel, G.D., Somenzi, F.: A symbolic algorithm for maximum flow in 0-1 networks. Formal Methods in System Design, 207–219 (1997)
Jukna, S.: The graph of integer multiplication is hard for read-k-times networks. Technical Report 95–10, Universität Trier (1995)
Keim, M., Drechsler, R., Becker, B., Martin, M., Molitor, P.: Polynomial formal verification of multipliers. Formal Methods in System Design 22, 39–58 (2003)
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: IEEE Int. Conf. on CAD, pp. 42–47 (1993)
Sawitzki, D.: Implicit flow maximization by iterative squaring (manuscript), http://ls2-www.cs.uni-dortmund.de/~sawitzki
Sawitzki, D.: Implicit flow maximization on grid networks (manuscript), http://ls2-www.cs.uni-dortmund.de/~sawitzki
Sawitzki, D.: Implizite Algorithmen für Graphprobleme. Diploma thesis, Univ. Dortmund (2002)
Wegener, I.: Branching Programs and Binary Decision Diagrams - Theory and Applications. SIAM, Philadelphia (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woelfel, P. (2003). Symbolic Topological Sorting with OBDDs. In: Rovan, B., Vojtáš, P. (eds) Mathematical Foundations of Computer Science 2003. MFCS 2003. Lecture Notes in Computer Science, vol 2747. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45138-9_61
Download citation
DOI: https://doi.org/10.1007/978-3-540-45138-9_61
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40671-6
Online ISBN: 978-3-540-45138-9
eBook Packages: Springer Book Archive