On solving quadratic word equations

Word equations are natural constraints in an automatic analysis of string manipulating programs. In particular, equations with at most two occurrences of each variable (quadratic word equations) are of interest of the analysis. The algorithm solving such equations with the exponential complexity is given by Yu. Hmelevskij in 1971. V. Diekert in 1999 proved that the satisfiability problem for the quadratic word equations is NP-hard. In this paper we suggest some refinements of Hmelevskij's algorithm to make it more applicable in the automatic analysis of programs. We consider the length analysis and splitting procedures and show when these refinements can be used to extract explicit solutions of the equations and when they can be used only for deciding satisfiability. (In Russian). (in Russian).