LIPIcs.SWAT.2024.35.pdf
- Filesize: 0.85 MB
- 18 pages
For some time, it has been known that the model checking problem for first-order formulas is fixed-parameter tractable on nowhere dense graph classes, so we shall ask in which direction there is space for improvements. One of the possible directions is to go beyond first-order formulas: Augmenting first-order logic with general counting quantifiers increases the expressiveness by far, but makes the model checking problem hard even on graphs of bounded tree-depth. The picture is different if we allow only "simple" - but arbitrarily nested - counting terms of the form #y φ(x^- ,y) > N. Even then, only approximate model checking is possible on graph classes of bounded expansion. Here, the largest known logic fragment, on which exact model checking is still fpt, consists of formulas of the form ∃x_1 … ∃x_k #y φ(x^- ,y) > N, where φ(x^- ,y) is a first-order formula without counting terms. An example of a problem that can be expressed in this way is partial dominating set: Are there k vertices that dominate at least a given number of vertices in the graph? The complexity of the same problem is open if you replace at least with exactly. Likewise, the complexity of "are there k vertices that dominate at least half of the blue and half of the red vertices?" is also open. We answer both questions by providing an fpt algorithm that solves the model checking problem for formulas of the more general form ψ ≡ ∃x_1 … ∃x_k P(#y φ_1(x^- ,y), …, #y φ_ℓ(x^- ,y)), where P is an arbitrary polynomially computable predicate on numbers. The running time is f(|ψ|)n^{𝓁+1} polylog(n) on graph classes of bounded expansion. Under SETH, this running time is tight up to almost linear factor.
Feedback for Dagstuhl Publishing