An Optimal Construction for the Barthelmann-Schwentick Normal Form on Classes of Structures of Bounded Degree

TL;DR

This paper investigates the complexity of converting first-order logic formulas into Barthelmann-Schwentick normal form (BSNF), showing that while the general case has non-elementary blow-up, restricted classes of structures allow more efficient algorithms.

Contribution

The paper proves that non-elementary blow-up in BSNF conversion is unavoidable in general, but provides optimal algorithms for structures of degree ≤ 2 and ≤ d, with matching lower bounds.

Findings

BSNF conversion has non-elementary blow-up in general.

Efficient algorithms exist for structures of degree ≤ 2 and ≤ d.

Matching lower bounds confirm the optimality of these algorithms.

Abstract

Building on the locality conditions for first-order logic by Hanf and Gaifman, Barthelmann and Schwentick showed in 1999 that every first-order formula is equivalent to a formula of the shape $\exists x_1 \dotsc \exists x_k \forall y\,\phi$ where quantification in $\phi$ is relativised to elements of distance $\leq r$ from $y$. Such a formula will be called Barthelmann-Schwentick normal form (BSNF) in the following. However, although the proof is effective, it leads to a non-elementary blow-up of the BSNF in terms of the size of the original formula. We show that, if equivalence on the class of all structures, or even only finite forests, is required, this non-elementary blow-up is indeed unavoidable. We then examine restricted classes of structures where more efficient algorithms are possible. In this direction, we show that on any class of structures of degree $\leq 2$, BSNF can be computed in 2-fold exponential time with respect to the size of the input formula. And for any class of structures of degree $\leq d$ for some $d\geq 3$, this is possible in 3-fold exponential time. For both cases, we provide matching lower bounds.