Monadic second order finite satisfiability and unbounded tree-width

TL;DR

This paper proves the decidability of certain finite satisfiability problems involving monadic second order logic and bounded tree-width structures, extending known results to more complex logical frameworks.

Contribution

It establishes the decidability of a new class of finite satisfiability problems involving MSO logic combined with counting and linear cardinality constraints, even with unbounded tree-width.

Findings

Decidability of MSO satisfiability with bounded tree-width structures.

Decidability of MSO extended with linear cardinality constraints.

Decidability of similar extensions of WS1S.

Abstract

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 (1991). We prove 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\land\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 extending monadic second order logic with linear cardinality constraints of the form $|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$, where the $X_{i}$ and $Y_{j}$ are monadic second order variables. We prove the decidability of a similar extension of WS1S.