{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T19:22:56Z","timestamp":1787340176506,"version":"build-2736575974"},"reference-count":24,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[2008,1]]},"abstract":"<jats:p>Monadic second-order unification is second-order unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete, where we use the technique of compressing solutions using singleton context-free grammars. We prove that monadic second-order matching is also NP-complete.<\/jats:p>","DOI":"10.1137\/050645403","type":"journal-article","created":{"date-parts":[[2008,7,16]],"date-time":"2008-07-16T18:09:41Z","timestamp":1216231781000},"page":"1113-1140","source":"Crossref","is-referenced-by-count":10,"title":["The Complexity of Monadic Second-Order Unification"],"prefix":"10.1137","volume":"38","author":[{"given":"Jordi","family":"Levy","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mateu","family":"Villaret","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2008,7,2]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","unstructured":"G. Dowek,\n                      Higher-order unification and matching\n                      , in Handbook of Automated Reasoning, Vol. II, A. Robinson and A. Voronkov, eds., Elsevier Science, Amsterdam, 2001, pp. 1009\u20131062.","DOI":"10.1016\/B978-044450813-3\/50018-7"},{"key":"R2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90015-2"},{"key":"R3","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(06)80003-4"},{"key":"R4","unstructured":"M. R. Garey and D. S. Johnson,\n                      \u201cComputers and Intractability\": A Guide to the Theory of NP-Completeness\n                      , W. H. Freeman, San Francisco, 1979."},{"key":"R5","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"R6","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"R7","first-page":"172","volume":"4","author":"Karpinski M.","year":"1997","journal-title":"Nordic J. Comput.","ISSN":"https:\/\/id.crossref.org\/issn\/1236-6064","issn-type":"print"},{"key":"R8","doi-asserted-by":"publisher","DOI":"10.1145\/234533.234543"},{"key":"R9","doi-asserted-by":"crossref","unstructured":"J. Levy,\n                      Decidable and undecidable second-order unification problems\n                      , in Proceedings of the 9th Annual International Conference on Rewriting Techniques and Applications (RTA'98), Lecture Notes in Comput. Sci. 1379, Springer-Verlag, Berlin, 1998, pp. 47\u201360.","DOI":"10.1007\/BFb0052360"},{"key":"R10","doi-asserted-by":"crossref","unstructured":"J. Levy, M. Schmidt-Schau\u00df, and M. Villaret,\n                      Monadic second-order unification is NP-complete\n                      , in Proceedings of the 15th Annual International Conference on Rewriting Techniques and Applications (RTA'04), Lecture Notes in Comput. Sci. 3091, Springer-Verlag, Berlin, 2004, pp. 55\u201369.","DOI":"10.1007\/978-3-540-25979-4_4"},{"key":"R11","doi-asserted-by":"crossref","unstructured":"J. Levy, M. Schmidt-Schau\u00df, and M. Villaret,\n                      Bounded second-order unification is NP-complete\n                      , in Proceedings of the 17th Annual International Conference on Rewriting Techniques and Applications (RTA'06), Lecture Notes in Comput. Sci. 4098, Springer-Verlag, Berlin, 2006, pp. 400\u2013414.","DOI":"10.1007\/11805618_30"},{"key":"R12","doi-asserted-by":"crossref","unstructured":"J. Levy, M. Schmidt-Schau\u00df, and M. Villaret,\n                      Stratified context unification is NP-complete\n                      , in Proceedings of the 3rd Annual International Joint Conference on Automated Reasoning (IJCAR'06), Lecture Notes in Comput. Sci. 4130, Springer-Verlag, Berlin, 2006, pp. 82\u201396.","DOI":"10.1007\/11814771_8"},{"key":"R13","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2877"},{"key":"R14","doi-asserted-by":"crossref","unstructured":"J. Levy and M. Villaret,\n                      Currying second-order unification problems\n                      , in Proceedings of the 13th Annual International Conference on Rewriting Techniques and Applications (RTA'02), Lecture Notes in Comput. Sci. 2378, Springer-Verlag, Berlin, 2002, pp. 326\u2013339.","DOI":"10.1007\/3-540-45610-4_23"},{"key":"R15","unstructured":"Y. Lifshits,\n                      Solving Classical String Problems on Compressed Texts\n                      , The Computing Research Repository (CoRR); available online from http:\/\/www.avxiv.orgabs\/cs\/0604058 (2006)."},{"key":"R16","doi-asserted-by":"publisher","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"R17","doi-asserted-by":"crossref","unstructured":"W. Plandowski,\n                      Testing equivalence of morphisms on context-free languages\n                      , in Proceedings of the Second Annual European Symposium on Algorithms (ESA'94), Lecture Notes in Comput. Sci. 855, Springer-Verlag, London, 1994, pp. 460\u2013470.","DOI":"10.1007\/BFb0049431"},{"key":"R18","unstructured":"W. Plandowski,\n                      The Complexity of the Morphism Equivalence Problem for Context-Free Languages\n                      , Ph.D. thesis, Department of Mathematics, Informatics and Mechanics, Warsaw University, Warsaw, Poland, 1995."},{"key":"R19","doi-asserted-by":"crossref","unstructured":"W. Plandowski,\n                      Satisfiability of word equations with constants is in PSPACE\n                      , in Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science (FOCS'99), pp. 495\u2013500.","DOI":"10.1109\/SFFCS.1999.814622"},{"key":"R20","doi-asserted-by":"publisher","DOI":"10.1145\/990308.990312"},{"key":"R21","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df,\n                      Stratified context unification is in PSPACE\n                      , in Proceedings of the 15th International Workshop in Computer Science Logic (CSL'01), Lecture Notes in Comput. Sci. 2142, Springer-Verlag, Berlin, 2001, pp. 498\u2013512.","DOI":"10.1007\/3-540-44802-0_35"},{"key":"R22","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.002"},{"key":"R23","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df and K. U. Schulz,\n                      On the exponent of periodicity of minimal solutions of context equations\n                      , in Proceedings of the 9th Annual International Conference on Rewriting Techniques and Applications (RTA'98), Lecture Notes in Comput. Sci. 1379, Springer-Verlag, Berlin, 1998, pp. 61\u201375.","DOI":"10.1007\/BFb0052361"},{"key":"R24","first-page":"735","volume":"15","author":"Zhezherun A. P.","year":"1980","journal-title":"Kibernetika (Kiev), 5 (1979), pp. 120\u2013125 (in Russian); Cybernetics"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/050645403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T18:22:57Z","timestamp":1787336577000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/050645403"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["10.1137\/050645403"],"URL":"https:\/\/doi.org\/10.1137\/050645403","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1]]}}}