The Golden Path to Guarded Monotone Strict NP

TL;DR

This paper proves the decidability and complexity bounds for containment and FO-rewritability problems in Guarded Monotone Strict NP, advancing understanding of its model-theoretic properties and connections to CSPs.

Contribution

It establishes decidability and complexity bounds for GMSNP problems and refines the associated model-theoretic structures for future research.

Findings

Containment and FO-rewritability are decidable for GMSNP.

Complexity of these problems is 2NEXPTIME.

Structures related to GMSNP can be used to reduce problems to recoloring tests.

Abstract

Guarded Monotone Strict NP (GMSNP) extends Monotone Monadic Strict NP (MMSNP) by guarded existentially quantified predicates of arbitrary arities. We prove that the containment and the FO-rewritability problems for GMSNP are decidable, thereby settling an open question of Bienvenu, ten Cate, Lutz, and Wolter, later restated by Bourhis and Lutz. Our proof also comes with a 2NEXPTIME upper bound on the complexity of the two problems, which matches the lower bounds for MMSNP due to Bourhis and Lutz. To obtain these results, we significantly improve the state of knowledge of the model-theoretic properties of GMSNP. Bodirsky, Kn\"{a}uer, and Starke previously showed that every GMSNP sentence defines a finite union of CSPs of $\omega$-categorical structures. We show that these structures can be used to obtain a reduction from the containment problem for GMSNP to the much simpler problem of testing the existence of a recolouring; a careful analysis of this yields said upper bound for containment. The upper bound for FO-rewritability is subsequently obtained by an application of several standard techniques from the theory of infinite-domain CSPs. As our secondary contribution, we refine the construction of Bodirsky, Kn\"{a}uer, and Starke by adding a restricted form of homogeneity to the properties of these structures, making the logic amenable to future complexity classifications for query evaluation using techniques developed for infinite-domain CSPs.