\documentclass{rtaloop}
\rtalabel{stringunif-complexity}


\begin{document}
\begin{problem}{Klaus Schulz}{}{September 1998}

\begin{abstract}
What is the exact complexity of word unification?
\end{abstract}

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 \cite{Makanin:77}, see
\cite{Dieckert:Makanin01} for a recent presentation of Makanin's algorithm.
The best known upper bounds for its complexity are {\it exponential space\/}
and {\it doubly exponential time\/} (\cite{Gutierrez:focs98}), leaving a wide
gap to the best known lower bound of its complexity which is just NP (see
\cite{Dieckert:Makanin01}). 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?

\begin{remark}
Satisfiability of word equations is in PSPACE \cite{plandowski99focs}.
\end{remark}
\end{problem}
\end{document}