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.
@InProceedings{lokshtanov_et_al:LIPIcs.ICALP.2018.135, author = {Lokshtanov, Daniel and Ramanujan, M. S. and Saurabh, Saket and Zehavi, Meirav}, title = {{Reducing CMSO Model Checking to Highly Connected Graphs}}, booktitle = {45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)}, pages = {135:1--135:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-076-7}, ISSN = {1868-8969}, year = {2018}, volume = {107}, editor = {Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.135}, URN = {urn:nbn:de:0030-drops-91391}, doi = {10.4230/LIPIcs.ICALP.2018.135}, annote = {Keywords: Fixed Parameter Tractability Model Checking Recursive Understanding} }
Feedback for Dagstuhl Publishing