2026-07-24T05:17:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9139 2024-03-06T10:43:27Z ddc:004 open_access

Reducing CMSO Model Checking to Highly Connected Graphs Lokshtanov, Daniel Ramanujan, M. S. Saurabh, Saket Zehavi, Meirav Fixed Parameter Tractability Model Checking Recursive Understanding 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 |= 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Daniel Lokshtanov and M. S. Ramanujan and Saket Saurabh and Meirav Zehavi 2018 Is Part Of LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2018.135 urn:nbn:de:0030-drops-91391 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.135 eng https://creativecommons.org/licenses/by/3.0/legalcode