Intractable unifiability problems and backtracking (Q1262770)

In an input theorem prover, backtracking can be reduced by pruning whole subtrees of a search tree, which do not yield compatible unifiers. The corresponding computational problem consists in the computation of maximal unifiable assignment sets [\textit{T. Y. Chen}, \textit{J. L. Lassez}, \textit{G. S. Port}, New Generation Comput. 4, 133-152 (1986; Zbl 0591.68083)]. The author shows the intractability of the problem to find maximal unifiable subsets, as well as the NP-hardness of some subproblems. Formally, the problem is the following: Given a set of pairs of atoms C, find a maximal subset \(C'\) of C s.t. \(C'\) is unifiable (that means, there is a \(\vartheta\) s.t. for all \((p,q)\in C'\), \(p\vartheta =q\vartheta)\). An assignment s is a non-unifiable set of assignments, C is called a failure assignment if \(C=\{s\}\) is unifiable. It is shown that the number of maximal unifiable subsets of an assignment set may be exponential; thus the problem of constructing all these subsets is intractable. The following problems are shown to be NP-complete: (Let C be an assignment set, \(s\in C\) be a failure assignment and \(k\leq | C|.)\) a) There exists a set \(C'\) s.t. \(s\in C'\), \(C'\subseteq C\), \(| C'| \geq k\) and \(C'\) is unifiable. b) There exists a minimal non-unifiable subset \(C'\) of C s.t. \(s\in C'\) and \(| C'| \geq k.\) As a consequence, some NP-hardness results follow, as finding a largest maximal unifiable subset, or finding a largest minimal non-unifiable subset. The complexity results illustrate that the computation of maximal assignment sets in order to reduce backtracking, is very problematic, because the costs may be as high as those payed for the search itself.