Compact Labelings For Efficient First-Order Model-Checking

TL;DR

This paper introduces compact labelings enabling efficient first-order model-checking on certain graph classes, generalizing previous decomposability notions and extending to counting queries.

Contribution

It proves the existence of logarithmic-length labelings for first-order model-checking on nicely locally cwd-decomposable and bounded expansion graph classes.

Findings

Labelings of logarithmic length enable efficient model-checking.

Generalization from tree-decomposable to cwd-decomposable classes.

Extension of results to counting queries.

Abstract

We consider graph properties that can be checked from labels, i.e., bit sequences, of logarithmic length attached to vertices. We prove that there exists such a labeling for checking a first-order formula with free set variables in the graphs of every class that is \emph{nicely locally cwd-decomposable}. This notion generalizes that of a \emph{nicely locally tree-decomposable} class. The graphs of such classes can be covered by graphs of bounded \emph{clique-width} with limited overlaps. We also consider such labelings for \emph{bounded} first-order formulas on graph classes of \emph{bounded expansion}. Some of these results are extended to counting queries.