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

Abstract

We introduce \emph{sub-connectivity logic}, denoted by $\text{FOscon}$, an extension of first-order logic for graphs with a specified set $Z$ of admissible edges. Its additional atom $\text{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 $\mathcal{C}$, the class of all expansions of graphs in $\mathcal{C}$ by rooted spanning forest orders has bounded twin-width if and only if $\mathcal{C}$ excludes a fixed minor. When $\mathcal{C}$ excludes a fixed minor, we can also compute an additional linear order that preserves bounded twin-width in polynomial time. We translate $\text{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 $\text{FOscon}$ with running time $f(|\varphi |,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 $\mathcal{C}$ let ${\mathcal{C}}_Z:=\{(G,Z):G\in \mathcal{C},Z\subseteq E(G)\}$. We show that for every weakly sparse graph class $\mathcal{C}$, the class ${\mathcal{C}}_Z$ is monadically dependent for $\text{FOscon}$ if and only if $\mathcal{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 $\text{FOscon}$ motivated by database queries.