Exponential improvement of exhaustive backtracking: data structure and implementation

Abstract

The paper presents the data structure enabling an implementation of an efficient backtracking method for plan-based deduction. The structure consists of two parts. Static structure combines information about the initial set of clauses and unifiers. Dynamic structure records information about the history of the deduction process (plan graph), about the unifications built in this process (graph of constraints), and about the conflicts encountered. Dynamic structure consists purely of pointers and integers and is extremely economical. The system operates on units. The units describe attempts to find the solution and reside on disk. A procedure controlling traffic of units between disk and memory and guaranteeing completeness of the search is presented. Some other procedures (development and pruning of plans, development of constraints graph and conflict detection) are also discussed. The last section presents an example of a problem and follows its solution by a conventional PROLOG interpreter and by our system.