Intelligent backtracking in logic programs analyses unification failure to avoid thrashing, which is an inefficient behaviour of ordinary backtracking. We show that the computation of all maximal unifiable subsets of constraints, as a means to avoid thrashing, is intractable in the sense that the solution length can be non-polynomially related to the input length. We also give a corresponding result for minimal nonunifiability. Restrictions of the problem of finding all maximal unifiable (minimal nonunifiable) subsets to those of certain sizes, for use with heuristics, are shown to be NP-hard. The results apply not only to standard unification but for unification without the occur-check as in many versions of Prolog. This now justifies the necessity for approximate or heuristic approaches in general.
CITATION STYLE
Wolfram, D. A. (1986). Intractable unifiability problems and backtracking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 225 LNCS, pp. 107–121). Springer Verlag. https://doi.org/10.1007/3-540-16492-8_68
Mendeley helps you to discover research relevant for your work.