Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes

Petr A. Golovach, Giannos Stamoulis, Dimitrios M. Thilikos

TL;DR

The paper extends the frontier of algorithmic meta-theorems by proving that model-checking for $\mathrm{FOL+DP}$ on proper minor-closed graph classes and for $\mathrm{FOL+SDP}$ on graphs of bounded Euler genus can be done in quadratic time in the input size. It introduces the logical extensions $\mathrm{FOL+DP}$ and $\mathrm{FOL+SDP}$, with $\mathrm{dp}_k$ and $s\text{-}dp_k$ predicates, and develops a comprehensive framework combining the irrelevant-vertex technique, flat walls/annuli, pattern-encoding, and folio-containment to reduce general instances to bounded-treewidth cores where Courcelle-type results apply. The main technical thrust is to encode FO+DP queries into recursive folios and partial-signature structures that can be manipulated via representatives and exchangeability lemmas, enabling quadratic-time model-checking via a sequence of reductions that preserve satisfiability. The paper further extends these ideas to $s$-scattered paths, achieving tractability for $\mathrm{FOL+s\text{-}sdp}$ on graphs embeddable on fixed surfaces. Overall, the results unify and extend tractable model-checking for logics between $\mathrm{FO}$ and MSOL under natural graph-structural constraints, with broad implications for problems expressible in these logics (e.g., various minor- and genus-related containment/reconfiguration questions).

Abstract

The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate $\mathsf{dp}_k(x_1,y_1,\ldots,x_k,y_k),$ expressing the existence of internally vertex-disjoint paths between $x_i$ and $y_i,$ for $i\in\{1,\ldots, k\}$. This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every proper minor-closed graph class, model-checking for FOL+DP can be done in quadratic time. We also introduce an extension of FOL+DP, namely the scattered disjoint paths logic, FOL+SDP, where we further consider the atomic predicate $s{\sf -sdp}_k(x_1,y_1,\ldots,x_k,y_k),$ demanding that the disjoint paths are within distance bigger than some fixed value $s$. Using the same technique we prove that model-checking for FOL+SDP can be done in quadratic time on classes of graphs with bounded Euler genus.

Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes

TL;DR

The paper extends the frontier of algorithmic meta-theorems by proving that model-checking for on proper minor-closed graph classes and for on graphs of bounded Euler genus can be done in quadratic time in the input size. It introduces the logical extensions and , with and predicates, and develops a comprehensive framework combining the irrelevant-vertex technique, flat walls/annuli, pattern-encoding, and folio-containment to reduce general instances to bounded-treewidth cores where Courcelle-type results apply. The main technical thrust is to encode FO+DP queries into recursive folios and partial-signature structures that can be manipulated via representatives and exchangeability lemmas, enabling quadratic-time model-checking via a sequence of reductions that preserve satisfiability. The paper further extends these ideas to -scattered paths, achieving tractability for on graphs embeddable on fixed surfaces. Overall, the results unify and extend tractable model-checking for logics between and MSOL under natural graph-structural constraints, with broad implications for problems expressible in these logics (e.g., various minor- and genus-related containment/reconfiguration questions).

Abstract

The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate expressing the existence of internally vertex-disjoint paths between and for . This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every proper minor-closed graph class, model-checking for FOL+DP can be done in quadratic time. We also introduce an extension of FOL+DP, namely the scattered disjoint paths logic, FOL+SDP, where we further consider the atomic predicate demanding that the disjoint paths are within distance bigger than some fixed value . Using the same technique we prove that model-checking for FOL+SDP can be done in quadratic time on classes of graphs with bounded Euler genus.
Paper Structure (156 sections, 28 theorems, 86 equations, 13 figures)

This paper contains 156 sections, 28 theorems, 86 equations, 13 figures.

Table of Contents

  1. Introduction
  2. AMTs for MSOL and FOL
  3. Meta-algorithmics of FOL.
  4. AMTs between FOL and MSOL.
  5. AMTs for FOL + DP and extensions
  6. Our results.
  7. The irrelevant vertex technique
  8. The potential of irrelevant vertex technique.
  9. What to do with a clique.
  10. Organization of the paper.
  11. Overview of the proof
  12. General scheme of the algorithm
  13. Irrelevant vertices for model-checking.
  14. Translating model-checking to (recursive) folio containment
  15. Assigning annotated graphs to rooted trees.
  16. ...and 141 more sections

Key Result

Theorem 1

Every problem on graphs that is expressible by some formula $\varphi$ in FOL + DP can be solved by an algorithm running in time $\mathcal{O}_{|\varphi|,r}(n^2)$, where $r$ is the Hadwiger number of $G$.

Figures (13)

  • Figure 1: An example of an assignment of an annotated graph $(G,R,R,R)$ (depicted on the upper left part of the figure) to a rooted tree $(T,t_0)$ (in the center of the figure). We use colors for each vertex of $G$ in order to distinguish them, without using indices and we use colors in the nodes of $T$ to show where each vertex of $G$ is mapped to. The small graphs below each leaf of $T$ encode the pattern-coloring, i.e., are the (boundaried) graphs induced by the vertices collected in each root-to-leaf path of $T$ and the linear orderings of their vertex sets (from left to right) follow the ordering of the corresponding path. Vertices that are picked twice in the same path are drawn inside a same-colored bag (respecting the ordering). The subtree $T'$ is a $\varphi$-spanning subtree of $(T,t_0)$ for the FOL-sentence $\varphi = \exists {\sf x}_1\in {\sf R}_1\ \forall {\sf x}_2\in{\sf R}_2\ \exists {\sf x}_3\in{\sf R}_3\ ({\sf x}_1 = {\sf x}_2 \vee {\sf E}({\sf x}_2,{\sf x}_3))$, that certifies that $(G,R,R,R)\models \varphi$.
  • Figure 2: An illustration of a (flat) railed annulus and a linkage (depicted in red) that is combed through some prescribed vertices of the railed annulus (depicted in orange).
  • Figure 3: A rooted tree $(T,t_0)$ and a $\varphi$-spanning subtree $T'$ of $T$ (depicted in red), for a sentence $\varphi=\forall{\sf x}_1 \exists {\sf x}_2 \forall {\sf x}_3 \psi({\sf x}_1,{\sf x}_2, {\sf x}_3)$.
  • Figure 4: An example of a $5$-boundaried $(3,3)$-colored graph $(G,X_1,X_2,X_3, a_1,\mathvisiblespace, a_3, v_1,v_2,\mathvisiblespace, v_4,v_5)$, where $X_1$ is the set of vertices depicted in red, $X_2$ is the set of vertices depicted in blue, and $X_3$ is the set of vertices depicted in green.
  • Figure 5: An illustration of a partially annulus-embedded graph.
  • ...and 8 more figures

Theorems & Definitions (44)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Claim 1
  • Claim 2
  • Proposition 1
  • ...and 34 more