发表机构
University of Warsaw; CAMS, EHESS/CNRS UMR 8557; University of Bremen; Université Paris Cité, CNRS, IRIF; LIRMM, Univ Montpellier, CNRS; LIMOS, Univ Clermont Auvergne, Clermont Auvergne INP（华沙大学; EHESS/CNRS联合研究单位8557; 不来梅大学; 巴黎西岱大学，法国国家科学研究中心，信息学研究所; 蒙彼利埃大学，法国国家科学研究中心，计算机科学与微电子研究所; 克勒蒙奥弗涅大学，克勒蒙奥弗涅理工学院，计算与信息系统实验室）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出子连通逻辑FOscon，证明其模型检验与幺半依赖性可由排除固定小图刻画，并给出高效算法及组合重构应用。
AI 中文摘要
我们引入子连通逻辑，记为FOscon，它是对具有指定可容许边集Z的图的一阶逻辑的扩展。其附加原子scon(x,y;z̄)断言x和y之间存在一条仅使用Z中的边并避开z̄中顶点的路径。我们的主要结构结果表明，对于每个弱稀疏图类C，C中所有图通过根生成森林序的扩张类具有有界孪生宽度，当且仅当C排除一个固定小图。当C排除一个固定小图时，我们还可以在多项式时间内计算一个额外的线性序，该线性序保持有界孪生宽度。我们将FOscon翻译为在可容许边图的深度优先生成森林序扩张上的一阶逻辑。将此翻译与我们的结构结果相结合，我们获得了一个FOscon的模型检验算法，其运行时间为f(|φ|,h(G))·|G|^c，其中f是可计算的，c是绝对常数，h(G)是G的Hadwiger数。该翻译和模型检验算法扩展到二元关系结构，Hadwiger数在Gaifman图上度量。对于图类C，令C_Z:={(G,Z):G∈C, Z⊆E(G)}。我们证明，对于每个弱稀疏图类C，类C_Z对于FOscon是幺半依赖的，当且仅当C排除一个固定小图。对于允许高效小图编码的单调类，相应的困难结果使这一边界在计算上紧密。我们将此应用于组合重构和解发现问题，并研究了受数据库查询启发的FOscon的受保护扩展。
英文摘要
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.
