paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Going deep and going wide: Counting logic and homomorphism indistinguishability over graphs of bounded treedepth and treewidth

深入与拓宽:有界树深与树宽图上的计数逻辑与同态不可区分性
LMCS vol.Volume 22, Issue 22026匹配度 2/10 · 该论文属于有限模型论与图逻辑,研究计数逻辑、同态不可区分性及有界树宽/树深图类,与用户关注的程序静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关联。虽然树宽等概念偶尔用于程序分析,但本文未涉及程序、LLM 或相关交叉方向。引用 17 inbox
Isolde Adler, Eva Fluck, Tim Seppelt, Gian Luca Spitzer
crossref: 2026-09-10

AI 速览

一句话:重新证明并拓展计数逻辑与同态不可区分性关系,分离有界树宽/树深类,并证明相关图类同态区分封闭。

本文研究带计数量词的一阶逻辑(尤其 k 变量、量词秩 q 片段)的表达能力,并用同态不可区分性刻画其语义。Dawar 等人曾证明:两图满足相同 k 变量量词秩 q 句子,当且仅当它们在具有深度 q 的 k-pebble 森林覆盖的图上同态不可区分。作者先初等重证,再分析该图类,证明当 q 充分大于 k 时,它可与树宽不超过 k−1 与树深不超过 q 的图类之交集分离,并提升为同态不可区分关系的语义分离。为证明 Roberson 猜想中该图类的同态区分封闭性,作者用单调 Cops-and-Robber 游戏刻画,关键是将 Cop 获胜策略转为 pre-tree-decomposition,并通过宽度优先清理与顶点交换在控制轮数时获得单调性。

问题
研究带计数量词的一阶逻辑片段的表达能力,以及同态不可区分性对相应图类的刻画与分离。
方法
初等重证 Dawar 等人的刻画,并对 k-pebble 森林覆盖图类做图论分析;用单调 Cops-and-Robber 游戏、pre-tree-decomposition 与顶点交换证明同态区分封闭性。
评估
通过理论证明与构造性分析:给出图类分离,证明其可提升为同态不可区分关系的语义分离,并验证 Roberson 猜想的相关情形。
原文摘要(Abstract)

We study the expressive power of first-order logic with counting quantifiers, especially the $k$-variable and quantifier-rank-$q$ fragment, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio~(2021) proved that two graphs satisfy the same $k$-variable and quantifier-rank-$q$ sentences if and only if they are homomorphism indistinguishable over the class of graphs admitting a $k$-pebble forest cover of depth $q$. After reproving this result using elementary means, we provide a graph-theoretic analysis of this graph class. This allows us to separate it from the intersection of the class of all graphs of treewidth at most $k-1$ and the class of all graphs of treedepth at most $q$, provided that $q$ is sufficiently larger than $k$. We are able to lift this separation to a (semantic) separation of the respective homomorphism indistinguishability relations. We do this by showing that the graph classes of all graphs of treedepth at most $q$ and of graphs admitting a $k$-pebble forest cover of depth $q$ are homomorphism distinguishing closed, as conjectured by Roberson~(2022). In order to prove Roberson's conjecture for the class of graphs admitting a $k$-pebble forest cover of depth $q$ we characterise the class in terms of a monotone Cops-and-Robber game.The crux is to prove that if Cop has a winning strategy then Cop also has a winning strategy that is monotone.To that end, we show how to transform Cop's winning strategy into a pre-tree-decomposition, which is inspired by decompositions of matroids, and then applying an intricate breadth-first `cleaning up' procedure along the pre-tree-decomposition (which may temporarily lose the property of representing a strategy), in order to achieve monotonicity while controlling the number of rounds simultaneously across all branches of the decomposition via a vertex exchange argument. arXiv admin note: text overlap with arXiv:2308.06044

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-2505-01193,
  title = {Going deep and going wide: Counting logic and homomorphism indistinguishability over graphs of bounded treedepth and treewidth},
  author = {Isolde Adler and Eva Fluck and Tim Seppelt and Gian Luca Spitzer},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 2},
  year = {2026},
  doi = {10.46298/lmcs-22(2:33)2026}
}