Preservation and decomposition theorems for bounded degree structures

TL;DR

This paper develops algorithms for transforming first-order logic sentences into equivalent forms on finite structures with bounded degree, providing complexity bounds and lower bounds for these transformations.

Contribution

It introduces elementary algorithms for preservation theorems on finite structures with bounded degree, including complexity bounds and extensions to FO+MODm and decomposition methods.

Findings

Existential and existential-positive sentences can be constructed with 4- or 5-fold exponential time.

Lower bounds show a 3-fold exponential blow-up is unavoidable.

Feferman-Vaught decompositions can be computed in 3-fold exponential time.

Abstract

We provide elementary algorithms for two preservation theorems for first-order sentences (FO) on the class \^ad of all finite structures of degree at most d: For each FO-sentence that is preserved under extensions (homomorphisms) on \^ad, a \^ad-equivalent existential (existential-positive) FO-sentence can be constructed in 5-fold (4-fold) exponential time. This is complemented by lower bounds showing that a 3-fold exponential blow-up of the computed existential (existential-positive) sentence is unavoidable. Both algorithms can be extended (while maintaining the upper and lower bounds on their time complexity) to input first-order sentences with modulo m counting quantifiers (FO+MODm). Furthermore, we show that for an input FO-formula, a \^ad-equivalent Feferman-Vaught decomposition can be computed in 3-fold exponential time. We also provide a matching lower bound.