Source-linked AI summary
Deciding first-order properties of nowhere dense graphs
Martin Grohe, Stephan Kreutzer, Sebastian Siebertz
TL;DR
The paper asks whether first-order properties can be decided efficiently on the broad sparse class of nowhere dense graphs. It develops recursive locality algorithms supported by sparse neighbourhood covers, a Splitter Game characterisation, and rank-preserving locality, proving fixed-parameter tractability and an O(n1+ε) bound. The result is optimal for subgraph-closed classes, while uniformity requires an effectively nowhere dense class.
Problem
Deciding first-order properties on arbitrary graphs is unlikely to be fixed-parameter tractable, motivating a tractability meta theorem for broad sparse graph classes.
Method
The paper combines recursive locality-based model checking with sparse neighbourhood covers, a Splitter Game characterisation, and a rank-preserving version of Gaifman’s theorem.
Results
For every nowhere dense class C and ε > 0, first-order properties are decidable in time O(n1+ε), yielding fixed-parameter tractability.
Takeaways & Limitations
The theorem generalises earlier first-order meta theorems and is optimal for graph classes closed under taking subgraphs.
Takeaways & Limitations
The introduction’s theorem statement gives non-uniform fixed-parameter tractability; uniform fixed-parameter tractability is obtained for effectively nowhere dense classes.
Abstract
from arXiv · showhide
Nowhere dense graph classes, introduced by Nesetril and Ossona de Mendez, form a large variety of classes of "sparse graphs" including the class of planar graphs, actually all classes with excluded minors, and also bounded degree graphs and graph classes of bounded expansion. We show that deciding properties of graphs definable in first-order logic is fixed-parameter tractable on nowhere dense graph classes. At least for graph classes closed under taking subgraphs, this result is optimal: it was known before that for all classes C of graphs closed under taking subgraphs, if deciding first-order properties of graphs in C is fixed-parameter tractable, then C must be nowhere dense (under a reasonable complexity theoretic assumption). As a by-product, we give an algorithmic construction of sparse neighbourhood covers for nowhere dense graphs. This extends and improves previous constructions of neighbourhood covers for graph classes with excluded minors. At the same time, our construction is considerably simpler than those. Our proofs are based on a new game-theoretic characterisation of nowhere dense graphs that allows for a recursive version of locality-based algorithms on these classes. On the logical side, we prove a "rank-preserving" version of Gaifman's locality theorem.
1 Introduction
The paper establishes a first-order model-checking meta theorem for nowhere dense graph classes, a broad family of sparse graphs, using recursive locality-based algorithms. It also introduces sparse neighbourhood covers, a game characterisation of nowhere density, and a rank-preserving locality theorem.
- Scope: Nowhere dense classes include planar graphs, bounded tree-width and bounded degree classes, bounded-expansion classes, and classes with excluded topological subgraphs.The paper presents nowhere density as a formalisation of broad classes of sparse graphs, while bounded average degree or bounded degeneracy alone do not guarantee nowhere density.
- Main result: For every nowhere dense class C and every ε > 0, first-order properties can be decided in time O(n1+ε).This yields fixed-parameter tractability for first-order model checking on nowhere dense classes.
- Algorithmic approach: The algorithm iterates locality reductions, evaluating formulas in r-neighbourhoods and solving an independent-set variant until the process terminates after a constant number of steps.This iterative approach addresses the fact that neighbourhoods in nowhere dense graphs need not have a simple directly exploitable structure.
- Sparse neighbourhood covers: The paper gives an algorithmic construction of sparse neighbourhood covers with clusters of radius 2r, where each vertex belongs to no(1) clusters.For bounded-expansion classes, each vertex belongs to only a constant number of clusters; the construction improves the radius of prior covers for planar and excluded-minor classes.
- Structural characterisation: The Splitter Game characterises nowhere dense classes by formalising the localisation-and-splitting process and its termination.Termination occurs exactly on nowhere dense graphs, providing a necessary and sufficient condition for nowhere density.
- Logical machinery: A Rank-Preserving Locality Theorem translates first-order formulas into local formulas of the same rank, using a discounted rank measure.This quantifier-rank control is needed because the locality transformation is applied repeatedly.
2 Preliminaries
The preliminaries fix graph, representation, distance, neighborhood, orientation, and parameterized model-checking terminology used throughout the paper.
- Graphs are finite, simple, and undirected unless directed graphs are explicitly mentioned.
- The paper uses adjacency-list representations, optionally storing separate in-neighbor and out-neighbor lists for an orientation.This supports adjacency checks in time O(∆−(⃗G)).
- A graph is k-degenerate when every induced subgraph has a vertex of degree at most k.Such graphs have at most k·n edges and admit orientations with maximum indegree at most k.
- Distances, radii, centers, r-neighborhoods, r-independent sets, and r-scattered sets provide the locality notions used later.The supplied preliminaries define these notions through shortest-path distances and neighborhood separation.
- The model-checking problem asks whether an input graph G in a class C satisfies a supplied first-order sentence ϕ.The framework treats the formula or sentence as part of a parameterized decision problem.
3 Nowhere Dense Classes of Graphs
Nowhere dense classes formalize sparse graph families through excluded shallow minors and equivalent sparsity, quasi-wideness, and algorithmic characterizations.
- A class C is nowhere dense if, for every radius r, some graph H_r is excluded as a depth-r minor from every graph in C.Excluding a depth-r minor is a local condition and is weaker than excluding a graph as an unrestricted minor.
- For effectively nowhere dense classes, the result is uniform: one computable algorithm runs in time f(|ϕ|, ε)·n1+ε.The introduction’s theorem statement itself provides only non-uniform fixed-parameter tractability.
- Nowhere dense classes have n^{1+o(1)} edges in all r-shallow minors of sufficiently large n-vertex graphs.This expresses uniform sparsity under local contractions, not merely sparsity of the original graphs and their subgraphs.
- Equivalent characterizations include depth-minor sparsity and uniform quasi-wideness, with effective versions when the associated bounds are computable.Lemma 3.4 gives a function f controlling shallow-minor edge counts, while Lemma 3.6 identifies nowhere density with uniform quasi-wideness.
4 Game theoretic characterisation of nowhere dense classes
The Splitter Game characterizes nowhere density and formalizes the recursive local splitting used by the paper’s algorithms.
- Splitter Game: In the (ℓ,m,r)-Splitter Game, Connector chooses a vertex and Splitter deletes at most m vertices from its r-neighborhood each round.The remaining induced neighborhood becomes the next game graph, and Splitter wins when it is empty within ℓ rounds.
- Splitter Game: Every nowhere dense class admits ℓ and m for each r such that Splitter wins the game on every graph in the class.For effectively nowhere dense classes, these parameters can be computed from r.
- Splitter strategy: The strategy deletes vertices lying on short paths connecting the current move to earlier moves, with at most i·(r+1) deletions after i rounds.The construction uses breadth-first search trees and can compute Splitter’s response efficiently.
- Characterization: If Splitter wins with suitable parameters for every radius, the class is nowhere dense, making the game characterization necessary and sufficient.Conversely, if a class is somewhere dense, complete shallow minors let Connector defeat Splitter for suitable game parameters.
5 Independent Sets in Nowhere Dense Classes of Graphs
The paper uses the Splitter Game to obtain fixed-parameter algorithms for distance independent sets on nowhere dense classes, via a rainbow reduction and recursive neighborhood decomposition.
- Problem and result: DISTANCE INDEPENDENT SET asks whether a graph contains an r-independent set of size k, and is NP-complete in general.The paper proves this problem fixed-parameter tractable on nowhere dense classes.
- Rainbow reduction: The algorithm reduces the ordinary problem to RAINBOW DISTANCE INDEPENDENT SET using the colored product G•K_k.A graph has an r-independent set of size k exactly when its product with K_k has a rainbow r-independent set of size k.
- Rainbow reduction: The product construction preserves nowhere density for every fixed k.This supports the non-uniform reduction; the uniform version translates a Splitter strategy with parameter m to one with parameter km.
- Recursive decomposition: The recursive procedure builds maximal rainbow independent sets, removes surrounding neighborhoods, and continues on smaller graphs for at most k stages.It then handles connected components, color assignments, and Splitter moves to decide the remaining instance.
6 Sparse Neighbourhood Covers
This section develops efficiently computable sparse neighbourhood covers for nowhere dense graphs through transitive fraternal augmentations and weak colouring numbers. The resulting covers have radius at most 2r, maximum degree at most n^ε, and can be computed in f(r,ε)·n^(1+ε) time.
- Motivation: Neighbourhood covers support the paper’s first-order model-checking data structure and are also useful in distributed-systems data structures.The section targets covers with small radius and small size.
- Definitions: An r-neighbourhood cover consists of connected clusters containing the r-neighbourhood of every vertex.Its radius is the maximum cluster radius, while its degree counts how many clusters contain a vertex.
- Main result: The main theorem constructs an r-neighbourhood cover with radius at most 2r, maximum degree at most n^ε, and running time f(r,ε)·n^(1+ε).The function f is computable when the class is effectively nowhere dense.
- Construction: Transitive fraternal augmentations provide sparse directed representations that can be computed efficiently on nowhere dense classes.For suitable parameters, the augmentation has maximum indegree at most n^ε and is computable in f(r,ε)·n^(1+ε) time.
- Weak colouring numbers: An augmentation with maximum indegree d yields the bound wcol_r(G) ≤ 2(d + 1)^2 through a degeneracy-based vertex ordering.The ordering bounds the number of weakly reachable vertices by counting path endpoints that are smallest on their paths.
- Weak colouring numbers: For every r and ε, vertices of sufficiently large nowhere dense graphs can be ordered so that every weak r-reachability set has size at most n^ε.The ordering is computable in f(r,ε)·n^(1+ε) time, with computable f for effectively nowhere dense classes.
7 Locality of First-Order Logic
This section refines Gaifman locality for first-order logic by controlling quantifier rank during translation. The rank-preserving theorem expresses formulas using local independence sentences and atomic formulas over neighbourhood-cover expansions.
- Locality foundations: The Gaifman graph of a structure records co-occurrence in relation tuples, providing the distance and neighbourhood notions used for locality.A formula is r-local when its truth depends only on the r-neighbourhood of its free variables.
- Locality foundations: Gaifman’s theorem represents every first-order sentence as a Boolean combination of basic local sentences.The paper needs stronger rank control because its locality-based algorithm applies the theorem repeatedly.
- Rank control: The discounted rank measure treats distance atoms as syntactic primitives and assigns their permitted radii according to quantifier scope.For q-rank at most ℓ, a distance atom under i quantifiers must satisfy d ≤ (4q)^(q+ℓ−i).
- Proof structure: The proof establishes equivalences between bounded-rank types and neighbourhood-cover expansions to support the locality translation.The argument includes a contradiction showing that more than k mutually separated representatives cannot be required in the relevant configuration.
- Rank-Preserving Locality Theorem: The Rank-Preserving Locality Theorem translates every FO formula of quantifier rank q into an FO+ formula of the same rank.The translation is a Boolean combination of (q+1,r)-independence sentences and atomic formulas, where r=f_q(q), and is computable from the input formula.
- Rank-Preserving Locality Theorem: For sentences, the theorem yields an FO+ sentence that is a Boolean combination of (q+1,r)-independence sentences and preserves the original truth value.This is the cover-independent corollary used for sentence-level reasoning.
8 The Main Algorithm
The main algorithm establishes near-linear-time first-order model checking on nowhere dense classes, including coloured graphs and formulas with one free variable. It combines rank-preserving locality, sparse neighbourhood covers, recursive decomposition, and game-theoretic reductions.
- Theorem: Every first-order formula with one free variable can be evaluated on coloured graphs whose underlying graph lies in a nowhere dense class in time O(n1+ε).The result also applies to effectively nowhere dense classes with running time f(|ϕ|, ε) · n1+ε.
- Recursive reduction: A game-theoretic splitting strategy recursively decomposes neighbourhoods after deleting only a few vertices.The construction uses Splitter’s response in the splitter game and recursively evaluates the resulting formulas on smaller graphs.
- Recursive reduction: Recursive calls remove a bounded set of vertices and encode their distances using fresh unary predicates.The transformed structure preserves formula evaluation through an atomic q-type and a rank-preserving formula translation.
- Locality reduction: The algorithm reduces first-order model checking to evaluating formulas in neighbourhoods and solving independence problems.Rank-preserving locality transforms the formula into a Boolean combination of independence sentences and atomic formulas.
- Neighbourhood covers: Sparse neighbourhood covers provide bounded-radius sets that support the locality-based evaluation.For sufficiently large inputs, the cover has radius at most 2r and maximum degree nδ.
- Running time: The running-time recurrence closes because the recursive depth and constants depend on the formula and class parameters, not on the input size.The proof bounds the recurrence by cℓn1+ε, with c and ℓ bounded in terms of ϕ, ε, and C.
9 Conclusion
The paper proves fixed-parameter tractability for first-order properties on nowhere dense graph classes and presents this as optimal for classes closed under subgraphs. It also identifies sparse neighbourhood covers as a further structural consequence, while leaving broader closure conditions and cover-degree optimization open.
- Main conclusion: Fixed-parameter tractability for first-order properties on nowhere dense classes generalizes earlier algorithmic meta theorems and is optimal for classes closed under taking subgraphs.The optimality statement leaves open the corresponding characterization for classes closed only under induced subgraphs or weaker conditions.
- Algorithmic significance: The algorithms avoid the enormous hidden constants associated with the graph-minor structure theory used for many excluded-minor algorithms.The conclusion contrasts the paper’s comparatively simple graph-theoretic basis with Robertson and Seymour’s structure theory.
- Further consequence: Nowhere dense and bounded-expansion classes have simple sparse neighbourhood covers with very good parameters.The paper optimizes cover radius rather than the number of covering sets containing a vertex; improved degree bounds remain future work.