First-order query evaluation on structures of bounded degree

TL;DR

This paper provides a new proof that first-order query evaluation on structures of bounded degree can be performed with constant delay after linear preprocessing, using Gaifman's locality theorem, matching existing complexity bounds.

Contribution

It offers a different proof of constant-delay enumeration for first-order queries on bounded degree structures, leveraging Gaifman's locality theorem.

Findings

Enumeration problem is in Constant-Delaylin class

Total evaluation time is triply exponential in formula size

New proof matches the complexity of existing algorithms

Abstract

We consider the enumeration problem of first-order queries over structures of bounded degree. It was shown that this problem is in the Constant-Delaylin class. An enumeration problem belongs to Constant-Delaylin if for an input of size n it can be solved by: - an O(n) precomputation phase building an index structure, - followed by a phase enumerating the answers with no repetition and a constant delay between two consecutive outputs. In this article we give a different proof of this result based on Gaifman's locality theorem for first-order logic. Moreover, the constants we obtain yield a total evaluation time that is triply exponential in the size of the input formula, matching the complexity of the best known evaluation algorithms.