Approximate Evaluation of First-Order Counting Queries

TL;DR

This paper develops an efficient approximation scheme for model-checking a fragment of first-order counting logic on structures with bounded expansion, balancing correctness and computational feasibility.

Contribution

It introduces a linear fixed-parameter tractable approximation algorithm for FO({>0}) model-checking on bounded expansion structures, with a novel 'I do not know' response option.

Findings

Approximation scheme runs in linear fpt time.

Exact model-checking is hard on trees of bounded depth.

Slightly more expressive logic makes approximation hard on trees.

Abstract

Kuske and Schweikardt introduced the very expressive first-order counting logic FOC(P) to model database queries with counting operations. They showed that there is an efficient model-checking algorithm on graphs with bounded degree, while Grohe and Schweikardt showed that probably no such algorithm exists for trees of bounded depth. We analyze the fragment FO({>0}) of this logic. While we remove for example subtraction and comparison between two non-atomic counting terms, this logic remains quite expressive: We allow nested counting and comparison between counting terms and arbitrarily large numbers. Our main result is an approximation scheme of the model-checking problem for FO({>0}) that runs in linear fpt time on structures with bounded expansion. This scheme either gives the correct answer or says "I do not know." The latter answer may only be given if small perturbations in the number-symbols of the formula could make it both satisfied and unsatisfied. This is complemented by showing that exactly solving the model-checking problem for FO({>0}) is already hard on trees of bounded depth and just slightly increasing the expressiveness of FO({>0}) makes even approximation hard on trees.