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