Elementary first-order model checking for sparse graphs
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913860146954240 |
|---|---|
| author | Gajarský, Jakub Pilipczuk, Michał Sokołowski, Marek Stamoulis, Giannos Toruńczyk, Szymon |
| author_facet | Gajarský, Jakub Pilipczuk, Michał Sokołowski, Marek Stamoulis, Giannos Toruńczyk, Szymon |
| contents | It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula size is non-elementary, and in fact, this is unavoidable even for the class of all trees [Frick and Grohe, LICS 2002]. On the other hand, it is known that the dependency is elementary for classes of bounded degree [Frick and Grohe, LICS 2002] as well as for classes of bounded pathwidth [Lampis, ICALP 2023]. In this paper we generalise these results and almost completely characterise subgraph-closed graph classes for which the model checking problem is fixed-parameter tractable with an elementary dependency on the formula size. Those are the graph classes for which there exists a number $d$ such that for every $r$, some tree of depth $d$ and size bounded by an elementary function of $r$ is avoided as an $({\leq} r)$-subdivision in all graphs in the class. In particular, this implies that if the class in question excludes a fixed tree as a topological minor, then first-order model checking for graphs in the class is fixed-parameter tractable with an elementary dependency on the formula size. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_16230 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Elementary first-order model checking for sparse graphs Gajarský, Jakub Pilipczuk, Michał Sokołowski, Marek Stamoulis, Giannos Toruńczyk, Szymon Logic in Computer Science Discrete Mathematics Data Structures and Algorithms Combinatorics Logic It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula size is non-elementary, and in fact, this is unavoidable even for the class of all trees [Frick and Grohe, LICS 2002]. On the other hand, it is known that the dependency is elementary for classes of bounded degree [Frick and Grohe, LICS 2002] as well as for classes of bounded pathwidth [Lampis, ICALP 2023]. In this paper we generalise these results and almost completely characterise subgraph-closed graph classes for which the model checking problem is fixed-parameter tractable with an elementary dependency on the formula size. Those are the graph classes for which there exists a number $d$ such that for every $r$, some tree of depth $d$ and size bounded by an elementary function of $r$ is avoided as an $({\leq} r)$-subdivision in all graphs in the class. In particular, this implies that if the class in question excludes a fixed tree as a topological minor, then first-order model checking for graphs in the class is fixed-parameter tractable with an elementary dependency on the formula size. |
| title | Elementary first-order model checking for sparse graphs |
| topic | Logic in Computer Science Discrete Mathematics Data Structures and Algorithms Combinatorics Logic |
| url | https://arxiv.org/abs/2401.16230 |