On reordering conjunctions of literals; a simple, fast algorithm

Abstract

In most formulations, finding the optimal order of evaluation of subgoals in the body of a clause is known to be inherently exponential in lime. On the other hand, we have found it useful to apply a quick reordering algorithm, based only on individual rules, which, though not guaranteed always to generate an optimal order, often does yield large specdups in the executions of programs to which it is applied. The time complexity of the algorithm is - in the absence of nonlogical (builtin) predicates and in the presence of only safe negative literals - at most O(n2 log n) steps, where n is the length, in symbols, of the input conjunction.