On symbolic OBDD-based algorithms for the minimum spanning tree problem

The minimum spanning tree problem is one of the most fundamental algorithmic graph problems and OBDDs are a very common dynamic data structure for Boolean functions. Since in some applications graphs become larger and larger, a research branch has emerged which is concerned with the design and analysis of so-called symbolic algorithms for classical graph problems on OBDD-represented graph instances. Here, a symbolic minimum spanning tree algorithm using O(log3|V|) functional operations is presented, where V is the set of vertices of the input graph. Moreover, the computation of the transitive closure is investigated and it is proved that there can be an exponential blow-up from input to output size. Furthermore, answering an open problem posed by Sawitzki [37] it is shown that every symbolic OBDD-based algorithm for the minimum spanning tree problem needs exponential space (with respect to the OBDD size of the input graph). This result even holds for planar input graphs.