Unifications,deunifications, and their complexity

The execution of a Prolog program can be viewed as a sequence of unifications and backtracks over unifications. We study the time requirement of executing a sequence of such operations (the unify-deunify problem). It is shown that the well-known set union problem is reducible to this problem, even in the case when no function symbols are allowed (the Datalog unify-deunify problem). As the set union problem requires nonlinear time on a large class of algorithms, the same holds for the unify-deunify problem. Thus the linearity of single unifications does not give a complete picture of the time complexity of Prolog primitives. We discuss the methods for executing sequences of Datalog unifications used in Prolog interpreters and show that some of them require even quadratic time in the worst case. Complementing these results, we show that if the number of variables occurring in one clause is bounded by a constant, then the Datalog unify-deunify problem can be solved in linear time.A preliminary version of this paper appeared in the Third International Conference on Logic Programming, London, July 1986. This work was supported by the Academy of Finland and by TEKES.