paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Parameterized circuit complexity of model-checking on sparse structures

稀疏结构上模型检测的参数化电路复杂度
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 论文研究有界扩张稀疏结构上一阶模型检测的参数化电路复杂度,属于逻辑/描述复杂度理论,与用户核心关注的LLM/Agent与静态分析、浮点程序分析、贝叶斯程序分析等没有直接交叉;仅与形式化验证中的模型检测理论有很弱关联。引用 12 inbox
Michał Pilipczuk, Sebastian Siebertz, Szymon Toruńczyk
crossref: 2026-09-12

AI 速览

一句话:证明有界扩张图类上的一阶模型检测可由参数化 AC 电路判定,属于 para-AC^1。

论文研究稀疏结构上一阶逻辑模型检测的参数化电路复杂度。作者针对 Gaifman 图属于有效有界扩张图类的 n 元素结构 A 与一阶句子 φ,构造判定 φ 是否在 A 中成立的 AC 电路族,其大小为 f(φ)·n^c,深度为 f(φ)+c log n,其中 f 为可计算函数,c 为通用常数。由此将此类模型检测问题定位在参数化电路复杂度类 para-AC^1 中。作为证明路线的一部分,论文还表明有界扩张图类的基本分解工具箱,包括具有有界弱着色数的排序和低树深分解,均可在 para-AC^1 中计算。

问题
研究 Gaifman 图属于有效有界扩张图类的稀疏结构上一阶逻辑模型检测问题的参数化电路复杂度,即能否在 para-AC^1 中判定。
方法
构造判定一阶句子的 AC 电路族,并证明有界扩张图类的基本分解工具(有界弱着色数排序、低树深分解)可在 para-AC^1 中计算。
评估
通过电路大小与深度的渐近上界进行理论证明,将模型检测问题归入 para-AC^1。
原文摘要(Abstract)

We prove that for every class ℒ of graphs with effectively bounded expansion, given a first-order sentence φ and an n-element structure A whose Gaifman graph belongs to ℒ, the question whether φ holds in A can be decided by a family of AC-circuits of size f(φ) · nc and depth f(φ) + c log n, where f is a computable function and c is a universal constant. This places the model-checking problem for classes of bounded expansion in the parameterized circuit complexity class para-AC1. On the route to our result we prove that the basic decomposition toolbox for classes of bounded expansion, including orderings with bounded weak coloring numbers and low treedepth decompositions, can be computed in para-AC1.

链接与引用

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

BibTeX
@inproceedings{paperbot4340,
  title = {Parameterized circuit complexity of model-checking on sparse structures},
  author = {Michał Pilipczuk and Sebastian Siebertz and Szymon Toruńczyk},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209136}
}