Reducing CMSO Model Checking to Highly Connected Graphs
share
Given a Counting Monadic Second Order (CMSO) sentence ψ, the CMSO[ψ] problem is defined as follows. The input to CMSO[ψ] is a graph G, and the objective is to determine whether Gψ. Our main theorem states that for every CMSO sentence ψ, if CMSO[ψ] is solvable in polynomial time on "globally highly connected graphs", then CMSO[ψ] is solvable in polynomial time (on general graphs). We demonstrate the utility of our theorem in the design of parameterized algorithms. Specifically we show that technical problem-specific ingredients of a powerful method for designing parameterized algorithms, recursive understanding, can be replaced by a black-box invocation of our main theorem. We also show that our theorem can be easily deployed to show fixed parameterized tractability of a wide range of problems, where the input is a graph G and the task is to find a connected induced subgraph of G such that "few" vertices in this subgraph have neighbors outside the subgraph, and additionally the subgraph has a CMSO-definable property.
READ FULL TEXT