Reducing CMSO Model Checking to Highly Connected Graphs

TL;DR

This paper establishes a reduction from CMSO model checking on general graphs to highly connected graphs, enabling new fixed-parameter algorithms and simplifying existing methods for graph problems.

Contribution

It proves that polynomial-time solvability on highly connected graphs implies polynomial-time solvability on all graphs for CMSO problems, and applies this to parameterized algorithm design.

Findings

Reduces CMSO model checking to highly connected graphs

Enables fixed-parameter tractability for a broad class of problems

Simplifies the design of parameterized algorithms using a black-box approach

Abstract

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 $G\models \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.