Containment for Guarded Monotone Strict NP

TL;DR

This work resolves the open question of whether containment is decidable for Guarded Monotone Strict NP (GMSNP) and establishes a $2NEXPTIME$-complete upper bound, matching the known lower bound for MMSNP containment. The authors develop a multi-layered approach that first reduces containment to SNP via a recolouring framework, then leverages a refined model-theoretic construction to obtain SNP sentences with the amalgamation and Ramsey properties. A key contribution is the notion of recolouring-readiness, which allows one to transform connected GMSNP sentences into a form suitable for edge-recolouring arguments, at the cost of a controlled, doubly-exponential blow-up. The methodology—rooted in structural Ramsey theory and infinite-domain CSP techniques—provides a pathway toward complexity classifications for query evaluation in infinite domains and suggests how to extend these ideas to broader logics with guarded or amalgamation-based properties.

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 problem for GMSNP is 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 problem, which matches the lower bound for containment of MMSNP due to Bourhis and Lutz. In order to obtain these results, we significantly improve the state of knowledge of the model-theoretic properties of GMSNP. Bodirsky, Knäuer, and Starke previously showed that every GMSNP sentence defines a finite union of CSPs of $ω$-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 certain map called recolouring, albeit in a more general setting than GMSNP; a careful analysis of this yields said upper bound. As a secondary contribution, we refine the construction of Bodirsky, Knä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.

Figures (3)

• Figure 1: An edge-2-colouring of the complete graph on $5$ vertices avoiding monochromatic triangles (outer edges red, inner blue). Note that there is no vertex-2-colouring with this property.
• Figure 2: A recolouring from $\Phi_1$ to $\Phi_2$ in Example \ref{['ex:recolouring']}.
• Figure 3: An illustration of some pieces of the canonical databases of the forbidden patterns of the SNP sentence $\Phi_1$ from Example \ref{['ex:recolouring']}; the roots of the pieces are marked by the dashed lines.

Theorems & Definitions (39)

• Theorem 1.1: Theorem 3 in bouhris_lutz2016
• Theorem 1.2
• Corollary 1.3
• Theorem 1.4
• Lemma 2.1: Lemma 4.1.7 in Bodirsky_book
• Theorem 2.2: Fraïssé, Theorem 6.1.2 in hodges_book
• Theorem 2.2: bodirsky_pinsker_tsankov, Theorem 5 in bodirsky_pinsker_ramsey_canonical
• Proposition 3.1: Proposition 1 in bodirsky_asnp
• Corollary 3.2
• Lemma 3.3