Minor-free graph classes have efficient logic model checking and combinatorial properties
A Logic for Minor-Free Graph Classes: Model Checking, Dependence, and Combinatorial Reconfiguration
Logic in Computer ScienceDiscrete Mathematics
Summary
The paper introduces a new logical language called sub-connectivity logic that allows expressing connectivity constraints in graphs with certain edge restrictions. The authors prove that for certain graph classes that exclude specific complex subgraphs (known as minors), this logic can be efficiently checked and analyzed. They show that this property characterizes graph classes with bounded twin-width, connecting logical expressiveness to structural graph theory. Their results also have implications for solving problems where graph connectivity changes over time and for database query systems.
What this means in practice
- •For software verification teams: Enable efficient model checking for graph properties in systems modeled by minor-free graphs using advanced logic.
- •For database developers: Improve database query optimization by applying guarded extensions of sub-connectivity logic for complex relational data.
A theory result. No direct application yet.
Authors
Nikolas Mählmann, Patrice {Ossona de Mendez}, Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, {Dimitrios M. } Thilikos, Alexandre Vigny
Abstract
We introduce \emph{sub-connectivity logic}, denoted by $\textsf{FOscon}$, an extension of first-order logic for graphs with a specified set $Z$ of admissible edges. Its additional atom $\textsf{scon}(x,y;\bar z)$ asserts that $x$ and $y$ are connected by a path using only edges of $Z$ and avoiding the vertices in $\bar z$. Our main structural result states that, for every weakly sparse graph class $\mathscr C$, the class of all expansions of graphs in $\mathscr C$ by rooted spanning forest orders has bounded twin-width if and only if $\mathscr C$ excludes a fixed minor. When $\mathscr C$ excludes a fixed minor, we can also compute an additional linear order that preserves bounded twin-width in polynomial time. We translate $\textsf{FOscon}$ into first-order logic over an expansion by a depth-first spanning forest order of the admissible-edge graph. Combining this translation with our structural result, we obtain a model checking algorithm for $\textsf{FOscon}$ with running time $f(|φ|,h(G))\cdot |G|^c$, where $f$ is computable, $c$ is an absolute constant, and $h(G)$ is the Hadwiger number of $G$. The translation and model-checking algorithm extend to binary relational structures, with the Hadwiger number measured on the Gaifman graph. For a graph class $\mathscr C$ let $\mathscr C_Z:=\{(G,Z):G\in\mathscr C,\ Z\subseteq E(G)\}$. We show that for every weakly sparse graph class $\mathscr C$, the class $\mathscr C_Z$ is monadically dependent for $\textsf{FOscon}$ if and only if $\mathscr C$ excludes a fixed minor. For monotone classes that admit efficient minor encodings, a corresponding hardness result makes this frontier computationally tight. We give applications to combinatorial reconfiguration and solution discovery problems, and study a guarded extension of $\textsf{FOscon}$ motivated by database queries.