The satisfiability problem for a formula of monadic second-order logic is the problem of determining whether there exists at least one graph (possibly within a restricted family of graphs) for which the formula is true.
As a partial converse, proved that, whenever a family of graphs has a decidable MSO2 satisfiability problem, the family must have bounded treewidth.