Transformations for backtracking SETL programs

Candidate: Nathan,Albert


We study program transformations for a class of combinatorial search problems whose solutions are usually found by backtrack searching. High-level algorithms for such problems can be elegantly specified using SETL's backtracking primitives ok and fail, for which we give a more formal and precise semantic definition than the one which currently exists. Then we explore two types of transformations applicable to such specifications. First, we derive Finite Differencing transformations which reduce the amount of computation performed at each node of the search tree. Though the formal derivation of these transformations is somewhat lengthy, the net results are simple and easily understood. In the process of deriving the transformations, we also expose some difficulties encountered when applying Finite Differencing methods to programs which use ok/fail. Second, we propose two general transformations which reduce the size of the search tree generated by pruning subtrees which are guaranteed to fail. The first one is based on the idea of using knowledge accumulated during the search to guide the search, while the second one prunes subtrees which contain no paths of sufficient length needed to extend the current partial solution to a complete solution. For each filter, we describe its enabling conditions, give a high-level specification, and then formally derive an efficient implementation using Finite Differencing. Finally, we suggest suitable representations, based on SETL's Data Representation Sublanguage, for implementing the data structures used in our transformations. We demonstrate the effectiveness of all these transformations by programming some familiar backtrack-search problems and comparing the running times and number of nodes generated in the transformed versions against those of the original specification. We also show some papers from the literature in which some suggestion of these transformations does appear, but in which (in contrast to this work) no formal demonstration of their correctness or applicability to other problem domains is given.