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

TL;DR

This paper demonstrates that model checking first-order logic on sparse graph classes with bounded expansion can be efficiently decided by parameterized AC-circuits, placing it in a low complexity class.

Contribution

It establishes that model checking on classes of bounded expansion is in para-AC^1 and shows that key decomposition tools can be computed within this class.

Findings

Model checking for bounded expansion classes is in para-AC^1.

Decomposition tools like orderings and treedepth decompositions are computable in para-AC^1.

The approach provides a circuit complexity perspective on sparse graph model checking.

Abstract

We prove that for every class $C$ of graphs with effectively bounded expansion, given a first-order sentence $\varphi$ and an $n$-element structure $\mathbb{A}$ whose Gaifman graph belongs to $C$, the question whether $\varphi$ holds in $\mathbb{A}$ can be decided by a family of AC-circuits of size $f(\varphi)\cdot n^c$ and depth $f(\varphi)+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-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 $para-AC^1$.