A Logic for Minor-Free Graph Classes: Model Checking, Dependence, and Combinatorial Reconfiguration

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(|\phi|,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.