← All problems
Unverified

What is the exact complexity of word unification?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

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 [Schulz, 1998], see [Schulz, 1998] for a recent presentation of Makanin's algorithm. The best known upper bounds for its complexity are \textit{exponential space} and \textit{doubly exponential time} ([Schulz, 1998]), leaving a wide gap to the best known lower bound of its complexity which is just NP (see [Schulz, 1998]). 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?

Recorded progress.

Satisfiability of word equations is in PSPACE [Schulz, 1998].

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu