Intractable unifiability problems and backtracking

Abstract

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 reults 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.

© 1986 by Springer-Verlag

BiBTeX Entry

@inproceedings{ICLP86,
               AUTHOR = "D.A.\ Wolfram",
               TITLE = "Intractable unifiability problems and backtracking",
               BOOKTITLE = "Third International Conference on Logic Programming,
                            Lecture Notes in Computer Science {\bf 225}",
               YEAR = "1986",
               EDITOR = "Ehud Shapiro",
               PAGES = "107--121",
               PUBLISHER = "Springer",
               ADDRESS = "Berlin"}

Some Citations

1. Maria Alpuente, Moreno Falaschi, and Giorgio Levi.
   Incremental constraint satisfaction for constraint logic programming, Theoretical Computer Science 142 (1995) 27-57.

2. Christian Cordognet and Philippe Cordognet.
   Non-deterministic stream AND-parallelism based on intelligent backtracking, Logic Programming: Proceedings of the Sixth International Conference, Giorgio Levi and Maurizio Martelli (Editors), (MIT, Cambridge, Mass., 1989) 63-79.

3. Christian Cordognet, Philippe Cordognet, and Gilberto Filè.
   Yet another intelligent backtrack method, Logic Programming: Proceedings of the Fifth Conference and Symposium, R.A. Kowalski and K.A. Bowen (Editors), Volume One, (MIT, Cambridge, Mass., 1988) 447-465.

4. Christian Haack and J. B. Wells.
   Type error slicing in implicitly typed, higher-order languages. Sci. Comput. Programming, 50:189-224, 2004.

5. Antonis Kotzamanidis.
   Intelligent Backtracking in Logic Programming with Constraints over the Real Numbers, PhD dissertation, Imperial College, London, October 1995, 195pp.

6. Graham S. Port.
   A simple approach to finding the cause of non-unifiability, Logic Programming: Proceedings of the Fifth Conference and Symposium, R.A. Kowalski and K.A. Bowen (Editors), Volume One, (MIT, Cambridge, Mass., 1988) 651-665.

7. Murray P Shanahan, Exploiting Dependencies in Search and Inference Mechanisms, PhD Dissertation, University of Cambridge, 1987.

8. Jeffrey Mark Siskind.
   The Culprit Pointer Method for Selective Backtracking, M.S. Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, January, 1989.

9. Bradley S. Stewart, Ching-Fang Liaw, and Chelsea C. White III.
   A bibliograph of heuristic search research through 1992, IEEE Transactions on Systems, Man, and Cybernetics 24, 2 (February, 1994) 268-293.

10. Jiwei Wang and Simon Lavington.
    The Wivenhoe computational model: in search of more parallelisms, in Derek R. Brough, Ed., Logic Programming: New Frontiers, (Intellect Books, 1992) pp. 282-310.