Reducing CMSO model checking to highly connected graphs

DOI10.4230/LIPICS.ICALP.2018.135MaRDI QIDQ5002822zbMATH OpenOpenAlexFDO

Authors Daniel Lokshtanov, M. S. Ramanujan, Saket Saurabh, Meirav Zehavi

Publication date 28 July 2021

Full work available at URL https://arxiv.org/abs/1802.01453

zbMATH Keywords

model checkingfixed-parameter tractabilityrecursive understanding

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Parameterized complexity, tractability and kernelization (68Q27)

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 $Gmodelspsi$. 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.

Recommendations

• On supergraphs satisfying CMSO properties
• Large induced subgraphs via triangulations and CMSO
• The parameterised complexity of counting connected subgraphs and graph motifs
• Large Induced Subgraphs via Triangulations and CMSO
• On the parameterized intractability of monadic second-order logic

Cites work

• scientific article; zbMATH DE number 475614 (Why is no real title available?)
• scientific article; zbMATH DE number 1161563 (Why is no real title available?)
• scientific article; zbMATH DE number 969067 (Why is no real title available?)
• (Meta) kernelization
• A parameterized algorithm for mixed-cut
• Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families
• Deciding first-order properties of locally tree-decomposable structures
• Designing FPT algorithms for cut problems using randomized contractions
• Easy problems for tree-decomposable graphs
• FO model checking of interval graphs
• Faster existential FO model checking on posets
• Finding topological subgraphs is fixed-parameter tractable
• Fixed-parameter tractability, definability, and model-checking
• Fundamentals of parameterized complexity
• Graph structure and monadic second-order logic. A language-theoretic approach
• Parameterized algorithms
• Parameterized algorithms for min-max multiway cut and list digraph homomorphism
• Strong parameterized deletion: bipartite graphs
• Subexponential parameterized algorithms on bounded-genus graphs and H-minor-free graphs
• Testing first-order properties for subclasses of sparse graphs
• The minimum k-way cut of bounded size is fixed-parameter tractable
• The monadic second-order logic of graphs III : tree-decompositions, minors and complexity issues
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs

Cited in

(19)

• Model checking disjoint-paths logic on topological-minor-free graph classes
• Roman cycle hitting set
• On supergraphs satisfying CMSO properties
• Parameterized complexity of multi-node hubs
• An FPT algorithm for elimination distance to bounded degree graphs
• Breaking a graph into connected components with small dominating sets
• FPT algorithms to compute the elimination distance to bipartite graphs and more
• A fixed-parameter tractable algorithm for elimination distance to bounded degree graphs
• Distance from triviality 2.0: hybrid parameterizations
• Parameterized analysis and crossing minimization problems
• Lossy planarization: a constant-factor approximate kernelization for planar vertex deletion
• Deletion to scattered graph classes. I: Case of finite number of graph classes
• Single-exponential FPT algorithms for enumerating secluded \(\mathcal{F}\)-free subgraphs and deleting to scattered graph classes
• Finding connected secluded subgraphs
• Advances in algorithmic meta theorems (invited paper)
• Single-exponential FPT algorithms for enumerating secluded \(\mathcal{F}\)-free subgraphs and deleting to scattered graph classes
• On the parameterized complexity of multiway near-separator
• Parameterized complexity of multi-node hubs
• Path-contractions, edge deletions and connectivity preservation

This page was built for publication: Reducing CMSO model checking to highly connected graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5002822)