2026-07-26T00:57:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8408 2024-03-06T10:41:56Z ddc:004 open_access

Modulo Counting on Words and Trees Bednarczyk, Bartosz Charatonik, Witold satisfiability trees words two-variable logic modulo quantifiers We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bartosz Bednarczyk and Witold Charatonik 2018 Is Part Of LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2017.12 urn:nbn:de:0030-drops-84083 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.12 eng https://creativecommons.org/licenses/by/3.0/legalcode