Deriving Efficient Graph Algorithms

Abstract

Two case studies are presented that demonstrate the systematic derivation of efficient algorithms from simple combinatorial definitions. These case studies contribute to an exploration of evolutionary approaches to the explanation, proof, adaptation, and possibly the design of complex algorithms.

The algorithms derived are the linear-time depth-first-search algorithms developed by Tarjan and Hopcroft for strong connectivity and biconnectivity. These algorithms are generally considered by students to be complex and difficult to understand. The problems they solve, however, have simple combinatorial definitions that can themselves be considered inefficient algorithms.

The derivations employ systematic program manipulation techniques combined with appropriate domain-specific knowledge. The derivation approach offers evolutionary explanations of the algorithms that make explicit the respective roles of programming knowledge (embodied as program manipulation techniques) and domain-specific knowledge (embodied as graph-theoretic lemmas). Because the steps are rigorous and can potentially be formalized, the explanations are also proofs of correctness. We consider the merits of this approach to proof as compared with the usual a posteriori proofs. These case studies also illustrate how significant algorithmic derivations can be accomplished with a relatively small set of core program manipulation techniques.

A summary version of the biconnectivity derivation appeared in the first LICS conference, 1983 (Springer LNCS 164).

This research was supported in part by National Science Foundation Grant NSF-MCS79-21024, ONR N00014-80-C-0647, and DARPA/AFSOR F30602-01-2-0561, NSF ITR EIA-0086015, NSF EIA-0218376, and NSF EIA-0218359.

Author for correspondence. This research was supported in part by the Defense Advanced Research Projects Agency, ARPA Order No. 3597, monitored by the Air Force Avionics Laboratory under Contract F33615-81-K-1539, and U.S. Army Communications R&D Command under Contract DAAK80-81-K-0074, and the High Dependability Computing Program from NASA Ames cooperative agreement NCC-2-1298. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of NASA, DARPA, or the U.S. Government.