Is deciding the satisfiability of word equations in NP? This question is equivalent to asking whether one can check the correctness of a proposed solution of a word equation within a time bound that is polynomial in the size (length) of the equation. It is known that solving word equations is NP-hard, and it is known that it is in PSPACE, that is, one can decide the question using polynomial space (and exponential time). It is also known that, if the size of the shortest solution (if it exists) is exponentially bounded by the size of the equation, then solving equations is in NP. So far, only a double exponential bound has been shown.

-- JeffreyShallit - 13 Jul 2011