An Analysis of Consecutively Bounded Depth-First Search with Applications in Automated Deduction

Abstract

Consecutively bounded depth-first search involves repeatedly performing exhaustive depth-first search with increasing depth bounds of 1, 2, 3, and so on. The effect is similar to that of breadth-first search, but, instead of retaining the results at Ievel n - 1 for use in computing Ievel n, earlier results are recomputed . Consecutively bounded depth-first search is useful whenever a complete search strategy is needed and either it is desirable to minimize memory requirements or depth-first search can be implemented particularly efficiently. It is notably applicable to automated deduction, especially in logic-programming systems, such as PROLOG and EQLOG, and their extensions. Consecutively bounded depth-first search, unlike unbounded breadthfirst search, can perform cutoffs by using heuristic estimates of the minimum number of steps remaining on a solution path. Even if the possibility of such cutoffs is disregarded, an analysis shows that, in general, consecutively bounded depth-first search requires only ~ times as many operations as breadthfirst search, where bis the brauehing factor.