Reducing CMSO Model Checking to Highly Connected Graphs


Abstract in English

Given a Counting Monadic Second Order (CMSO) sentence $psi$, the CMSO$[psi]$ problem is defined as follows. The input to CMSO$[psi]$ is a graph $G$, and the objective is to determine whether $Gmodels psi$. Our main theorem states that for every CMSO sentence $psi$, if CMSO$[psi]$ is solvable in polynomial time on globally highly connected graphs, then CMSO$[psi]$ 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.

Download