English

Parameterized circuit complexity of model checking first-order logic on sparse structures

Discrete Mathematics 2018-05-10 v1 Computational Complexity

Abstract

We prove that for every class CC of graphs with effectively bounded expansion, given a first-order sentence φ\varphi and an nn-element structure A\mathbb{A} whose Gaifman graph belongs to CC, the question whether φ\varphi holds in A\mathbb{A} can be decided by a family of AC-circuits of size f(φ)ncf(\varphi)\cdot n^c and depth f(φ)+clognf(\varphi)+c\log n, where ff is a computable function and cc is a universal constant. This places the model-checking problem for classes of bounded expansion in the parameterized circuit complexity class paraAC1para-AC^1. 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 paraAC1para-AC^1.

Keywords

Cite

@article{arxiv.1805.03488,
  title  = {Parameterized circuit complexity of model checking first-order logic on sparse structures},
  author = {Michał Pilipczuk and Sebastian Siebertz and Szymon Toruńczyk},
  journal= {arXiv preprint arXiv:1805.03488},
  year   = {2018}
}
R2 v1 2026-06-23T01:49:34.262Z