We study the satisfiability of string constraints where context-free membership constraints may be imposed on variables. Additionally a variable may be constrained to be a subword of a word obtained by shuffling variables and their transductions. The satisfiability problem is known to be undecidable even without rational transductions. It is known to be NExptime-complete without transductions, if the subword relations between variables do not have a cyclic dependency between them. We show that the satisfiability problem stays decidable in this fragment even when rational transductions are added. It is 2NExptime-complete with context-free membership, and NExptime-complete with only regular membership. For the lower bound we prove a technical lemma that is of independent interest: The length of the shortest word in the intersection of a pushdown automaton (of size 𝒪(n)) and n finite-state automata (each of size 𝒪(n)) can be double exponential in n.
@InProceedings{aiswarya_et_al:LIPIcs.STACS.2024.5, author = {Aiswarya, C. and Mal, Soumodev and Saivasan, Prakash}, title = {{Satisfiability of Context-Free String Constraints with Subword-Ordering and Transducers}}, booktitle = {41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)}, pages = {5:1--5:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-311-9}, ISSN = {1868-8969}, year = {2024}, volume = {289}, editor = {Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.5}, URN = {urn:nbn:de:0030-drops-197154}, doi = {10.4230/LIPIcs.STACS.2024.5}, annote = {Keywords: satisfiability, subword, string constraints, context-free, transducers} }
Feedback for Dagstuhl Publishing