<p>Least general generalization is the problem of finding the most specific term that can generate all given terms via substitutions. It is also known as anti-unification and is considered a dual of the most general unification. It is known that both the least general generalization problem and the unification problem can be solved in polynomial time; however the latter becomes NP-hard when commutative function symbols are allowed. In this paper, we study the complexity of the least general generalization problem with commutative functions, formulated as a minimization problem. In particular, we show that this problem is NP-hard even if both input and output terms are restricted so that each variable occurs only once. We also show that this restricted variant can be solved in polynomial time if both the maximum arity and the number of input terms are bounded by constants. For the general terms, we present exponential-time algorithms for finding the most specific term in some restricted cases and in the general case.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On the complexity of least general generalization with commutative functions

  • Tatsuya Akutsu,
  • Atsuhiro Takasu

摘要

Least general generalization is the problem of finding the most specific term that can generate all given terms via substitutions. It is also known as anti-unification and is considered a dual of the most general unification. It is known that both the least general generalization problem and the unification problem can be solved in polynomial time; however the latter becomes NP-hard when commutative function symbols are allowed. In this paper, we study the complexity of the least general generalization problem with commutative functions, formulated as a minimization problem. In particular, we show that this problem is NP-hard even if both input and output terms are restricted so that each variable occurs only once. We also show that this restricted variant can be solved in polynomial time if both the maximum arity and the number of input terms are bounded by constants. For the general terms, we present exponential-time algorithms for finding the most specific term in some restricted cases and in the general case.