Paliath Narendran and D A Wolfram
December 1992, 6pp.
We show that the problems of nilpotent unifiability and that of finding, given a set of pairs of terms, whether there is a minimal non-unifiable subset whose size exceeds a given bound are both NP-complete problems. The reductions used are from the NP-complete problems of THREE SATISFIABILITY, and EXACT COVER respectively. The solution to the second problem answers a question by Wolfram (Intractable unifiability problems and backtracking, Journal of Automated Reasoning 5, 1989).
It has been superseded by "Unification and matching modulo nilpotence" by Paliath Narendran, Qing Guo, and D A Wolfram, to appear in Proceedings of the Thirteenth International Conference on Automated Deduction (CADE-13), (Michael McRobbie and John Slaney, Eds.), Lecture Notes in Computer Science (Springer, Berlin, 1996).