DocumentCode
3450618
Title
Satisfiability of word equations with constants is in PSPACE
Author
Plandowski, Wojciech
Author_Institution
Inst. of Inf., Warsaw Univ., Poland
fYear
1999
fDate
1999
Firstpage
495
Lastpage
500
Abstract
We prove that the satisfiability problem for word equations is in PSPACE. The satisfiability problem for word equations has a simple formulation: find out whether or not an input word equation has a solution. The decidability of the problem was proved by G.S. Makanin (1977). His decision procedure is one of the most complicated algorithms existing in the literature. We propose an alternative algorithm. The full version of the algorithm requires only a proof of the upper bound for index of periodicity of a minimal solution (A. Koscielski and L. Pacholski, see Journal of ACM, vol.43, no.4. p.670-84). Our algorithm is the first one which is proved to work in polynomial space
Keywords
computability; computational complexity; decidability; theorem proving; PSPACE; decidability; decision procedure; index of periodicity; input word equation; minimal solution; satisfiability problem; upper bound; word equation satisfiability; Equations; Informatics; NP-hard problem; Polynomials; Upper bound;
fLanguage
English
Publisher
ieee
Conference_Titel
Foundations of Computer Science, 1999. 40th Annual Symposium on
Conference_Location
New York City, NY
ISSN
0272-5428
Print_ISBN
0-7695-0409-4
Type
conf
DOI
10.1109/SFFCS.1999.814622
Filename
814622
Link To Document