2026-08-14T17:29:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6553 2024-03-06T10:38:42Z ddc:004 open_access

Monadic Second Order Finite Satisfiability and Unbounded Tree-Width Kotek, Tomer Veith, Helmut Zuleger, Florian Monadic Second Order Logic MSO Two variable Fragment with Counting C2 Finite decidability Unbounded Tree-width WS1S with Cardinality Constraints The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese. We prove that the following problem is decidable: Input: (i) A monadic second order logic sentence alpha, and (ii) a sentence beta in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of alpha and beta may intersect. Output: Is there a finite structure which satisfies alpha and beta such that the restriction of the structure to the vocabulary of alpha has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic MS^{exists card} extending monadic second order logic with linear cardinality constraints of the form |X_{1}|+...+|X_{r}| < |Y_{1}|+...+|Y_{s}| on the variables X_i, Y_j of the outer-most quantifier block. We prove the decidability of a similar extension of WS1S. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tomer Kotek and Helmut Veith and Florian Zuleger 2016 Is Part Of LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2016.13 urn:nbn:de:0030-drops-65537 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.13 eng https://creativecommons.org/licenses/by/3.0/legalcode