Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity

Fuente: arXiv
Guardado en:
Detalles Bibliográficos
Autores principales: Knop, Dušan, Koutecký, Martin, Masařík, Tomáš, Toufar, Tomáš
Formato: Preprint
Publicado: 2017
Materias:
Acceso en línea:
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
_version_ 1866915708139470848
author Knop, Dušan
Koutecký, Martin
Masařík, Tomáš
Toufar, Tomáš
author_facet Knop, Dušan
Koutecký, Martin
Masařík, Tomáš
Toufar, Tomáš
contents This paper settles the computational complexity of model checking of several extensions of the monadic second order (MSO) logic on two classes of graphs: graphs of bounded treewidth and graphs of bounded neighborhood diversity. A classical theorem of Courcelle states that any graph property definable in MSO is decidable in linear time on graphs of bounded treewidth. Algorithmic metatheorems like Courcelle's serve to generalize known positive results on various graph classes. We explore and extend three previously studied MSO extensions: global and local cardinality constraints (CardMSO and MSO-LCC) and optimizing the fair objective function (fairMSO). First, we show how these extensions of MSO relate to each other in their expressive power. Furthermore, we highlight a certain "linearity" of some of the newly introduced extensions which turns out to play an important role. Second, we provide parameterized algorithm for the aforementioned structural parameters. On the side of neighborhood diversity, we show that combining the linear variants of local and global cardinality constraints is possible while keeping the linear (FPT) runtime but removing linearity of either makes this impossible. Moreover, we provide a polynomial time (XP) algorithm for the most powerful of studied extensions, i.e. the combination of global and local constraints. Furthermore, we show a polynomial time (XP) algorithm on graphs of bounded treewidth for the same extension. In addition, we propose a general procedure of deriving XP algorithms on graphs on bounded treewidth via formulation as Constraint Satisfaction Problems (CSP). This shows an alternate approach as compared to standard dynamic programming formulations.
format Preprint
id arxiv_https___arxiv_org_abs_1703_00544
institution arXiv
publishDate 2017
record_format arxiv
spellingShingle Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
Knop, Dušan
Koutecký, Martin
Masařík, Tomáš
Toufar, Tomáš
Computational Complexity
Logic in Computer Science
F.2.2, G.2.2
F.2.2; G.2.2
This paper settles the computational complexity of model checking of several extensions of the monadic second order (MSO) logic on two classes of graphs: graphs of bounded treewidth and graphs of bounded neighborhood diversity. A classical theorem of Courcelle states that any graph property definable in MSO is decidable in linear time on graphs of bounded treewidth. Algorithmic metatheorems like Courcelle's serve to generalize known positive results on various graph classes. We explore and extend three previously studied MSO extensions: global and local cardinality constraints (CardMSO and MSO-LCC) and optimizing the fair objective function (fairMSO). First, we show how these extensions of MSO relate to each other in their expressive power. Furthermore, we highlight a certain "linearity" of some of the newly introduced extensions which turns out to play an important role. Second, we provide parameterized algorithm for the aforementioned structural parameters. On the side of neighborhood diversity, we show that combining the linear variants of local and global cardinality constraints is possible while keeping the linear (FPT) runtime but removing linearity of either makes this impossible. Moreover, we provide a polynomial time (XP) algorithm for the most powerful of studied extensions, i.e. the combination of global and local constraints. Furthermore, we show a polynomial time (XP) algorithm on graphs of bounded treewidth for the same extension. In addition, we propose a general procedure of deriving XP algorithms on graphs on bounded treewidth via formulation as Constraint Satisfaction Problems (CSP). This shows an alternate approach as compared to standard dynamic programming formulations.
title Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
topic Computational Complexity
Logic in Computer Science
F.2.2, G.2.2
F.2.2; G.2.2
url https://arxiv.org/abs/1703.00544