Symbolic Topological Sorting with OBDDs

Symbolic Topological Sorting with OBDDs (Extended Abstract) Philipp Woelfelstar FB Informatik, LS2, Univ. Dortmund, 44221 Dortmund, Germany philipp.woelfel@cs.uni-dortmund.de Abstract. We present a symbolic OBDD algorithm for topological sort- ing which requires O(log2N) OBDD operations. Then we analyze its true runtime for the directed grid graph and show an upper bound of O(log4N). 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. 1 Introduction Algorithms on graphs is one of the best studied areas in computer science. Usu- ally, a graph G = (V,E) is given by an adjacency list or by an adjacency matrix. Such an explicit representation of a graph requires space Θ(|V|+|E|) or Θ(|V|2), and for many graph problems efficient algorithms are known. However, there are several application areas where typical problem instances have such a large size that a linear or even polynomial runtime is not feasible, or where even the explicit representation of the problem instance itself may not fit into memory anymore. In order to deal with very large graphs, symbolic (or implicit) graph al- gorithms have been devised, where the vertex and edge sets representing the involved graphs are stored symbolically, i.e., in terms of their characteristic func- tions. The characteristic functions are usually represented by so-called Binary Decision Diagrams (BDDs) or more specifically by Ordered Binary Decision Di- agrams (OBDDs) — see Section 2 for definitions. Such approaches have been successfully applied in the areas of model checking, circuit verification and finite state machine verification (see e.g. [2–4]). These applications can be viewed as particular cases of symbolic graph problems, which raises the question whether it is also possible to devise symbolic graph algorithms with a good behavior for fun- damental graph theoretical problems. One approach in this direction was under- taken by Hachtel and Somenzi [5] who introduced a symbolic OBDD algorithm for the maximum flow problem in 0-1 networks. The promising experimental studies demonstrated that the algorithm is able to handle graphs with over 1036 edges and that it is competitive with traditional algorithms on dense random graphs. The paper lacks however, a theoretical analysis of its performance with star Supported in part by DFG grant We 1066/10-1 respect to runtime. Recently, Sawitzki [9,11] has analyzed the number of OBDD operations (i.e., the number of required synthesis operations of characteristic functions) required by the flow algorithm of Hachtel and Somenzi and has pro- posed an improved algorithm. But note that there is only a very weak relation between the number of OBDD operations and the true runtime of a symbolic OBDD algorithm. The time required for one synthesis step is mainly influenced by the sizes of the involved OBDDs which may range from linear to exponential (in the number of variables of the represented characteristic functions). In...

Website: pages.cpsc.ucalgary.ca | Filesize: -
No of Page(s): 10
Download Symbolic Topological Sorting with OBDDs.pdf