[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Klaus Schulz
Date: September 1998
Summary: What is the exact complexity of word unification?
Satisfiability of word equations, that is unifiability in the algebra of ground terms built on a set of constants and a binary, associative concatenation operator, has been shown decidable by [Mak77], see [Die02] for a recent presentation of Makanin’s algorithm. The best known upper bounds for its complexity are exponential space and doubly exponential time ([Gut98]), leaving a wide gap to the best known lower bound of its complexity which is just NP (see [Die02]). There is an strange discrepancy between this weak lower bound and the enormous difficulty in designing word unification algorithms. So, what is the exact complexity of word unification?
Satisfiability of word equations is in PSPACE [Pla99].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |