Parameterized circuit complexity of model-checking on sparse structures

DOI10.1145/3209108.3209136zbMATH Open1497.68319arXiv1805.03488OpenAlexW2799268901MaRDI QIDQ5145356FDOQ5145356

Authors: Michał Pilipczuk, Sebastian Siebertz, Szymon Toruńczyk 

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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 $mathbbA$ whose Gaifman graph belongs to $C$, the question whether $varphi$ holds in $mathbbA$ can be decided by a family of AC-circuits of size $f(varphi)cdot{n}^c$ and depth $f(varphi)+clogn$, 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-A{C}^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-A{C}^1$.

Full work available at URL: https://arxiv.org/abs/1805.03488

Recommendations

• Current trends and new perspectives for first-order model checking (invited talk)
• First-Order Model Checking Problems Parameterized by the Model
• The parameterized space complexity of model-checking bounded variable first-order logic
• First-order interpretations of bounded expansion classes
• First-order interpretations of bounded expansion classes

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Model theory of finite structures (03C13) Specification and verification (program logics, model checking, etc.) (68Q60) Networks and circuits as models of computation; circuit complexity (68Q06) Parameterized complexity, tractability and kernelization (68Q27)

Cited In (6)

• Polynomial bounds for centered colorings on proper minor-closed graph classes
• On the Descriptive Complexity of Color Coding
• On the parallel parameterized complexity of MaxSAT variants
• Sparse Boolean equations and circuit lattices
• Bounding generalized coloring numbers of planar graphs using coin models
• Computing hitting set kernels by \(\mathrm{AC}^0\)-circuits

This page was built for publication: Parameterized circuit complexity of model-checking on sparse structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145356)