Containment for Guarded Monotone Strict NP

Guarded Monotone Strict NP ($\mathrm{GMSNP}$) is a syntactic fragment of existential second-order logic describing problems of the form

Is there a colouring of the relational tuples in a given finite relational structure avoiding a fixed set of finitely many forbidden colour-patterns?

The logic GMSNP was introduced in [6] as a generalisation of the logic Monotone Monadic Strict NP without inequality ($\mathrm{MMSNP}$) of Feder and Vardi [19], which captures similar problems concerning colourings of vertices instead of relational tuples. However, its true origins actually go back to an earlier work of Madelaine [28], who was studying GMSNP under the names MMSNP₂ and FPP (standing for Forbidden Pattern Problems).

Formally, a GMSNP sentence $\mathrm{\Phi }$ is of the form $\exists X_1,\mathrm{\dots },X_n\forall \overline{x}.\varphi (\overline{x})$, for a CNF-formula $\varphi$ over a finite relational signature $\tau \cup \{X_1,\mathrm{\dots },X_n\}$, satisfying the following two conditions:

• $\mathrm{■}$

  $\tau$-atoms and equalities may only appear negatively in clauses of $\varphi$, i.e., the only positive atoms in clauses of $\varphi$ are of the form $X_i(\overline{x})$ for some $i\in [n]$; (Monotonicity)

• $\mathrm{■}$

  for every clause $\psi$ of $\varphi$ and every positive atom $X_i(\overline{x})$ in $\psi$ there exists a negative atom $\neg R(\overline{y})$ in $\psi$ with $R\in \tau \cup \{X_1,\mathrm{\dots },X_n\}$ such that $\overline{x}\subseteq \overline{y}$. (Guarding)

Unless stated otherwise, we will denote the set $\{X_1,\mathrm{\dots },X_n\}$ of the second-order variables in $\mathrm{\Phi }$ by $\sigma$; we refer to $\sigma$ as the existential symbols and $\tau$ as the input symbols in $\mathrm{\Phi }$. We also refer to the first-order $(\tau \cup \sigma )$-sentence $\forall \overline{x}.\varphi (\overline{x})$ as the first-order part of $\mathrm{\Phi }$. By a simple application of De Morgan’s laws, we can rewrite $\varphi$ as a formula of the form ${\bigwedge }_i\neg {\varphi }_i$, where each ${\varphi }_i$ is a conjunction of $\tau$-atoms and possibly negated $\sigma$-atoms. We refer to the conjuncts ${\varphi }_i$ as the forbidden patterns of $\mathrm{\Phi }$.

A typical example of a problem that can be defined in $\mathrm{GMSNP}$ is whether a given undirected simple graph, say with edge relation denoted by $E$, can be edge-2-coloured while avoiding monochromatic triangles [21]:

See Figure 1 for illustration.

The forbidden patterns of this problem are the two monochromatic triangles, overlapping colours, and uncoloured edges. In MMSNP, we can formulate a similar problem where the task is to find a vertex-2-colouring instead of an edge-2-colouring:

Strictly speaking, $\mathrm{GMSNP}$ does not fully contain $\mathrm{MMSNP}$ because the latter does not require the guarding axiom (it instead requires the monadicity axiom). However, the containment does hold up to a small syntactic transformation, modulo which GMSNP is in fact strictly more expressive than MMSNP [6]. Namely, every MMSNP sentence $\mathrm{\Phi }$ can be converted into a GMSNP sentence $\mathrm{\Gamma }(\mathrm{\Phi })$ by expanding the base signature $\tau$ by a fresh unary “domain” symbol $D$ and adding negative atoms $\neg D(v)$ to each clause, for every universally quantified first-order variable $v$ appearing in that clause. Given a $\tau$-structure $𝔄$, we have that $\mathrm{\Phi }$ holds in $𝔄$ if and only if $\mathrm{\Gamma }(\mathrm{\Phi })$ holds in ${𝔄}^{+}$, where ${𝔄}^{+}$ is the $(\tau \cup \{D\})$-structure obtained from $𝔄$ by including every domain element in the relation interpreting $D$. On the other hand, given a $(\tau \cup \{D\})$-structure $𝔄$, we have that $\mathrm{\Gamma }(\mathrm{\Phi })$ holds in $𝔄$ if and only if $\mathrm{\Phi }$ holds in ${𝔄}^{-}$, where ${𝔄}^{-}$ is the $\tau$-structure obtained from $𝔄$ by forgetting $D$ and removing all domain elements which were not contained in the relation interpreting $D$. For example, the last two clauses in (1.1) do not satisfy the guarding axiom, but we can obtain a polynomial-time equivalent GMSNP sentence by padding (1.1) with the predicate $D\in \tau$:

In 2014, Bienvenu, ten Cate, Lutz, and Wolter [6] discovered an interesting correspondence that allows one to translate complexity classification results for certain well-behaved fragments of the logic SNP [26, 34] to analogous statements about the complexity of ontology-mediated queries. In the special case of MMSNP, the above-mentioned result from [6] implies that there is a dichotomy between P and NP-completeness if and only if there is a dichotomy between P and coNP-completeness for the evaluation of unions of conjunctive queries mediated by ontologies specified in the description logic $𝒜ℒ𝒞$ [1]. The significance of this equivalence lies in the fact that the computational complexity of MMSNP had already been intensively investigated within the programme initiated by Feder and Vardi in 1998 [19].

Feder and Vardi proved that every problem described by an MMSNP sentence is equivalent under polynomial-time randomised reductions to the Constraint Satisfaction Problem (CSP) of a structure with a finite domain, i.e., the problem of testing whether a given conjunctive query is satisfiable in that structure. They moreover conjectured that every finite-domain CSP is in P or NP-complete, which was eventually confirmed twenty years later by Bulatov and Zhuk [17, 39] in what can be viewed as the culmination of decades of work on connections between algorithms for CSPs and universal algebra. This implied dichotomies for MMSNP and, in turn, for the above-mentioned queries up to randomised reductions. Although the originally randomised reduction of MMSNP to CSPs by Feder and Vardi was derandomised by Kun in 2013 [27], it still relied on a probabilistic proof of the existence of expanders of large girth. The first truly constructive proof of the dichotomy was obtained in 2018 by Bodirsky, Madelaine, and Mottet [12] using methods from infinite-domain constraint satisfaction, i.e., CSPs of infinite structures. Roughly speaking, they start with the observation from [9] that every MMSNP sentence defines a finite union of CSPs of (infinite) $\omega$-categorical structures. They then gradually upgrade these structures until a state is reached where they can show that their CSPs admit a polynomial-time many-one reduction to a finite-domain CSP which is polynomial-time tractable unless one of the $\omega$-categorical structures can simulate the 3-colouring problem via a pp-construction [4] (in which case the sentence defines a NP-complete problem).

The question whether GMSNP also exhibits a P/NP-dichotomy was left open in [6]; a positive answer would yield a P/coNP-dichotomy for the evaluation of unions of conjunctive queries mediated by ontologies specified in guarded first-order logic. It was observed by Bodirsky, Knäuer, and Starke [11] that similarly to MMSNP, the logic GMSNP can be studied using methods from infinite-domain constraint satisfaction. Using this approach, the existence of a dichotomy has already been confirmed in some specific cases, e.g., for graph orientations with forbidden tournaments [10, 7, 20]. However, at the moment there is no clear road map for how exactly the question of the existence of a P/NP-dichotomy for GMSNP should be approached: it is apparent that the increase in the arity of the existentially quantified predicates introduces new obstacles which were not present with MMSNP. Hope is sparked by a recently announced result of Guzmán-Pro [22] who used the sparse-incomparability lemma [27] to show that the homomorphism-sandwiching method [16] for obtaining hardness reductions from finite-domain promise CSPs fails for CSPs definable in GMSNP. This is in fact a good plausibility argument for the applicability of methods from infinite-domain constraint satisfaction to GMSNP, because several NP-hardness results for finite-domain promise CSPs (Proposition 10.1 in [3] and Theorem 2.2 in [38]) are inconsistent with the algebraic dichotomy conjecture for infinite-domain CSPs [5].

Besides query evaluation, two other computational decision problems for ontology-mediated queries were studied in [6]: first-order/datalog rewritability and containment. As with their counterparts in automata theory, the complexity of such problems tends to be significantly higher. This raises the question of whether, in studying the complexity of these problems, one can perhaps avoid the fine-grained analysis that makes the proof of complexity dichotomies so intricate. In the case of MMSNP, the precise complexity of first-order/datalog rewritability and containment is known: both are 2NEXPTIME-complete [31, 32, 15]. While rewritability seems to be intimately linked to the reduction from MMSNP to finite-domain CSPs [31, 32], for the containment problem, the link seems to be much weaker [15, 12]. This makes the study of the containment problem for GMSNP a perfect starting point for the development of tools that will later be useful for approaching the topics of rewritability and query evaluation.

In the proof of our main result, it will be important that we formulate the containment problem in the more general setting of SNP sentences, which are obtained by leaving out the monotonicity and the guarding axioms. For an SNP sentence $\mathrm{\Phi }$, we denote the class of all finite models of $\mathrm{\Phi }$ by $\mathrm{𝑓𝑚}(\mathrm{\Phi })$. Formally, the containment problem can be stated as follows:
Containment for SNP
INSTANCE: A pair $({\mathrm{\Phi }}_1,{\mathrm{\Phi }}_2)$ of SNP sentences in a common signature $\tau$.
QUESTION: Is it true that $\mathrm{𝑓𝑚}({\mathrm{\Phi }}_1)\subseteq \mathrm{𝑓𝑚}({\mathrm{\Phi }}_2)$?

The containment problem for SNP is undecidable in general; in fact, it is already undecidable for the Datalog fragment [37]. The question whether it is decidable for GMSNP was left open in [6, 15]; the only known result regarding the complexity of this problem is the lower bound of Bourhis and Lutz for the containment within MMSNP. To see that this lower bound also applies for GMSNP, note that the map $\mathrm{\Gamma }$ introduced in Section 1.1 is not only a polynomial-time reduction from MMSNP to GMSNP, but it also acts as a fully faithful covariant functor with respect to containment. More specifically, for a pair $({\mathrm{\Phi }}_1,{\mathrm{\Phi }}_2)$ of MMSNP $\tau$-sentences, we have $\mathrm{𝑓𝑚}({\mathrm{\Phi }}_1)\subseteq \mathrm{𝑓𝑚}({\mathrm{\Phi }}_2)$ if and only if $\mathrm{𝑓𝑚}(\mathrm{\Gamma }({\mathrm{\Phi }}_1))\subseteq \mathrm{𝑓𝑚}(\mathrm{\Gamma }({\mathrm{\Phi }}_2))$.

The contributions of the present article are twofold. On the one hand, we confirm that the containment problem for GMSNP is indeed decidable. Our proof of decidability also comes with an upper bound on the complexity matching the lower bound in Theorem 1.

The proof of Theorem 2 is based on the recolouring method, first used implicitly by Feder and Vardi [19, Theorem 7] in their proof of decidability of containment for MMSNP.¹¹1Recolourings were first explicitly mentioned in the work of Madelaine and Stewart [30] (see also [29]). Roughly said, the strategy is to modify the input sentences by adding new clauses and existentially quantified symbols until a state is reached where the containment problem becomes equivalent to the much simpler problem of testing the existence of a mapping between the existential symbols of the two sentences satisfying a certain condition (a recolouring). In contrast to MMSNP, in order to achieve the promised 2NEXPTIME upper bound on the complexity of containment for GMSNP using the recolouring method, we have to deviate from the GMSNP framework (to SNP) and significantly generalise the notion of a recolouring.

The first preprocessing step, common across most approaches to the containment problem for MMSNP, is a reduction to the connected case [12, 15, 19, 29]. Intuitively, an MMSNP sentence is connected if its forbidden colour-patterns are connected in the graph-theoretic sense. This reduction can be generalised to GMSNP, as shown in [11]. Bodirsky, Knäuer, and Starke [11, Proposition 1] showed that every GMSNP sentence is logically equivalent to a finite disjunction of connected GMSNP sentences. An inspection of their proof reveals that if the complexity of checking containment is in 2NEXPTIME for connected GMSNP sentences, then so it is for the entire class GMSNP.

The second preprocessing step (in the approaches to the containment for MMSNP) is typically a reduction to the biconnected case [15, 12]. Intuitively, an MMSNP sentence is biconnected if no forbidden colour-pattern can be disconnected by deleting a single vertex. The reduction to biconnected MMSNP is the point where a significant amount of work can be outsourced to a general combinatorial result, e.g., a lemma of Erdős in the case of [15] or a theorem of Hubička and Nešetřil in the case of [12]. The procedure for attaining biconnectedness from [12, Lemma 4.4] transforms a given connected MMSNP sentence to a logically equivalent biconnected MMSNP sentence by iteratively selecting a forbidden colour-pattern which can be disconnected by deleting a single vertex and splitting it into two forbidden colour-patterns (corresponding to the two parts); the split is then marked using a fresh unary existential predicate. The GMSNP-analogue of this procedure does not terminate if the arities of the existentially quantified predicates are greater than $2$, and we do not see any way how this issue could be fixed. Therefore, to progress further, we must understand how exactly the said general combinatorial results are used in the complexity analysis of the containment problem; in the present paper, we focus specifically on the approach from [12] using the mentioned theorem of Hubička and Nešetřil.

Roughly said, the theorem implies that every connected MMSNP $\tau$-sentence $\mathrm{\Phi }$ can be assigned a highly symmetric infinite structure ${ℭ}_{\mathrm{\Phi }}$ in a signature extending $\tau \cup \sigma$ such that the $(\tau \cup \sigma )$-reducts of the finite substructures of ${ℭ}_{\mathrm{\Phi }}$ are up to isomorphism precisely the finite models of the first-order part of $\mathrm{\Phi }$; this was first observed by Bodirsky and Dalmau [9]. Bodirsky, Madelaine, and Mottet [12] proved that if $\mathrm{\Phi }$ is biconnected, then the $(\tau \cup \sigma )$-reduct of ${ℭ}_{\mathrm{\Phi }}$ retains a certain amount of the original symmetry, and this fact is crucial in their take on the recolouring method. Later on, Bodirsky, Knäuer, and Starke [11] showed that also connected GMSNP sentences can be assigned said highly symmetric infinite structures; they did not comment on whether this fact is helpful in analysing the complexity of the containment problem for GMSNP. We show that the highly symmetric infinite structures ${ℭ}_{\mathrm{\Phi }}$ associated with GMSNP sentences $\mathrm{\Phi }$ can be described by SNP sentences $\mathrm{\Delta }(\mathrm{\Phi })$ of size doubly exponential in the size of $\mathrm{\Phi }$. Subsequently, we show that the containment $\mathrm{𝑓𝑚}({\mathrm{\Phi }}_1)\subseteq \mathrm{𝑓𝑚}({\mathrm{\Phi }}_2)$ is equivalent to the existence of a particular mapping from ${ℭ}_{{\mathrm{\Phi }}_1}$ to ${ℭ}_{{\mathrm{\Phi }}_2}$ which is uniquely determined by the images of substructures whose size is bounded by the maximal arity of a symbol in ${\mathrm{\Phi }}_1$ or ${\mathrm{\Phi }}_2$. From this fact, we extract our more general version of recolourings for SNP. By carefully analysing the total complexity of computing the SNP sentences $\mathrm{\Delta }({\mathrm{\Phi }}_1)$ and $\mathrm{\Delta }({\mathrm{\Phi }}_2)$ stemming from the theorem of Hubička and Nešetřil and of the subsequent check for the existence of a recolouring between such sentences, we conclude that the containment problem for GMSNP is in 2NEXPTIME. We remark that our methods are, in theory, applicable in a more general setting than GMSNP; a fragment of SNP which is closely related to such applicability is Amalgamation SNP introduced in [11]. We also remark that the SNP sentences $\mathrm{\Delta }({\mathrm{\Phi }}_1)$ and $\mathrm{\Delta }({\mathrm{\Phi }}_2)$ define a linear order over the domain of a given structure, which is at the core of our argument why the recolouring method works in our case. It is provably not possible to define a linear order in GMSNP [11, Example 6], which indicates that this method requires us to leave the GMSNP framework.

As our secondary contribution, we analyse to what extent it is possible to prove the decidability of the containment problem for GMSNP while staying as close as possible to the original recolouring method for MMSNP. A (vertex)-recolouring $\xi$ between two MMSNP sentences ${\mathrm{\Phi }}_1$ and ${\mathrm{\Phi }}_2$ is simply a mapping from the (unary) existential symbols of ${\mathrm{\Phi }}_1$ to those of ${\mathrm{\Phi }}_2$ whose application to the relations denoted by these symbols of any model of the first-order part of ${\mathrm{\Phi }}_1$ yields a model of the first-order part of ${\mathrm{\Phi }}_2$. That is, the mapping $\xi$ does not introduce any vertex-colour patterns forbidden by ${\mathrm{\Phi }}_2$ into structures which originally did not contain any patterns forbidden by ${\mathrm{\Phi }}_1$ (see [12, Definition 4.25]). If ${\mathrm{\Phi }}_1$ and ${\mathrm{\Phi }}_2$ assert that the existential relations form a partition of all vertices (cf. the notion of normal form in [12]), then this is what one would intuitively understand under a recolouring of vertices – hence the name. But the true intention of this concept, which does not require any additional assumptions on ${\mathrm{\Phi }}_1$ and ${\mathrm{\Phi }}_2$ (such as the vertices being partitioned by the existential predicates) is to capture a very specific case of the containment $\mathrm{𝑓𝑚}({\mathrm{\Phi }}_1)\subseteq \mathrm{𝑓𝑚}({\mathrm{\Phi }}_2)$, which is witnessed uniformly across all structures in $\mathrm{𝑓𝑚}({\mathrm{\Phi }}_1)$. The natural extension of vertex-recolourings to GMSNP would be edge-recolourings, i.e., mappings

where $R\in \tau$ and ${\alpha }_i$ is an atomic ${\sigma }_i$-formula ($i\in [2]$), such that $\xi$ induces a mapping between models of the first-order parts of the two sentences. The notion of a recolouring for SNP we use in the proof of Theorem 2 is considerably more general and abstract. Hence, it makes sense to ask whether one can also prove decidability of containment for GMSNP by simply refining the input sentences ${\mathrm{\Phi }}_1$ and ${\mathrm{\Phi }}_2$ long enough, while staying in GMSNP, until the containment $\mathrm{𝑓𝑚}({\mathrm{\Phi }}_1)\subseteq \mathrm{𝑓𝑚}({\mathrm{\Phi }}_2)$ becomes equivalent to the existence of an edge-recolouring from ${\mathrm{\Phi }}_1$ to ${\mathrm{\Phi }}_2$.

The central notion in analysing this possibility is recolouring-readiness, which is comparable to the notion of a simple program of Bourhis and Lutz [15] or the normal form of Bodirsky, Madelaine, and Mottet [12]. Instead of relying purely on syntactic preprocessing, in the definition of recolouring-readiness, we draw our inspiration from the proof of Theorem 2. Intuitively, a GMSNP $\tau$-sentence $\mathrm{\Phi }$ is recolouring-ready if it can be assigned a highly symmetric infinite structure ${ℭ}_{\mathrm{\Phi }}$ as in our proof of Theorem 2 such that the $(\tau \cup \sigma )$-reduct of ${ℭ}_{\mathrm{\Phi }}$ retains a sufficient amount of the original symmetry for a reduction from containment to edge-recolouring to work. We show that every connected GMSNP sentence $\mathrm{\Phi }$ is logically equivalent to a connected recolouring-ready GMSNP sentence $\mathrm{\Omega }(\mathrm{\Phi })$. However, the size of the smallest such $\mathrm{\Omega }(\mathrm{\Phi })$ that we are able to obtain surpasses the upper bound provided in Theorem 2. We leave it as an open question whether the precise complexity of containment for GMSNP can be determined purely from within the GMSNP framework.

In Section 2, we provide some background knowledge necessary for the presentation of our results. Section 3 contains the proof of Theorem 2, where the individual steps are presented in the order given in the introduction. Section 4 contains a proof sketch for Theorem 4.

An SNP $\tau$-sentence $\exists X_1,\mathrm{\dots },X_n\forall \overline{x}.\varphi (\overline{x})$ is connected in the sense of [11, 8] if, for each clause $\psi$ in $\varphi$, the following $(\tau \cup \sigma )$-structure ${ℭ}_{\psi }$ is connected: the domain consists of all variables in $\psi$, and $\overline{t}\in R^{{ℭ}_{\psi }}$ if and only if $\neg R(\overline{t})$ is a disjunct in $\psi$ ($R\in \tau \cup \sigma$). For example, the sentences in equations (1.1) and (1.1) from the introduction are connected, while the sentence

is not because the variable sets $\{x,y\}$ and $\{u,v\}$ partition the structure ${ℭ}_{\psi }$ associated to the clause $\psi =\left(\neg E(x,y)\vee \neg E(u,v)\vee \neg R(x,y)\vee B(u,v)\right)$ into two disjoint substructures.

The next proposition was essentially proved in [11] (Proposition 1), except that the authors did not comment on the complexity of the procedure arising from their proof.

Proposition 8 shows that when studying the complexity of the the containment problem for GMSNP, we may without loss of generality restrict ourselves to connected GMSNP.

We call a relational structure standard if its domain is $[n]$ for some $n\in \mathbb{N}$. For an SNP $\tau$-sentence $\mathrm{\Phi }$, we denote the class of all finite models of the first-order part of $\mathrm{\Phi }$ (over the signature $\tau \cup \sigma$) by $\mathrm{𝑒𝑥𝑝𝑓𝑚}(\mathrm{\Phi })$. We define the $n$-colours of $\mathrm{\Phi }$, denoted $n\text{-}\mathrm{𝑐𝑜𝑙𝑜𝑢𝑟𝑠}(\mathrm{\Phi })$, as the set of all standard structures from $\mathrm{𝑒𝑥𝑝𝑓𝑚}(\mathrm{\Phi })$ of size $\le n$. A recolouring between two SNP $\tau$-sentences ${\mathrm{\Phi }}_1$ and ${\mathrm{\Phi }}_2$ is a mapping $\xi$ from $n\text{-}\mathrm{𝑐𝑜𝑙𝑜𝑢𝑟𝑠}({\mathrm{\Phi }}_1)$ to $n\text{-}\mathrm{𝑐𝑜𝑙𝑜𝑢𝑟𝑠}({\mathrm{\Phi }}_2)$, where $n≔\max (\mathrm{ar}({\mathrm{\Phi }}_1),\mathrm{ar}({\mathrm{\Phi }}_2))$, with the two following properties. First, the $\tau$-reducts of every $n$-colour of ${\mathrm{\Phi }}_1$ and of its $\xi$-image are identical. Secondly, for every $𝔄\in \mathrm{𝑒𝑥𝑝𝑓𝑚}({\mathrm{\Phi }}_1)$, there is a structure ${\xi }^{\prime }(𝔄)\in \mathrm{𝑒𝑥𝑝𝑓𝑚}({\mathrm{\Phi }}_2)$ on the same domain such that for all $𝔑\in n\text{-}\mathrm{𝑐𝑜𝑙𝑜𝑢𝑟𝑠}({\mathrm{\Phi }}_1)$ and every embedding $e\in \left(\genfrac{}{}{0pt}{}{𝔄}{𝔑}\right)$ we have $e\in \left(\genfrac{}{}{0pt}{}{{\xi }^{\prime }(𝔄)}{\xi (𝔑)}\right)$. In other words, the following extension ${\xi }^{\prime }$ of $\xi$ is a well-defined mapping from $\mathrm{𝑒𝑥𝑝𝑓𝑚}({\mathrm{\Phi }}_1)$ to $\mathrm{𝑒𝑥𝑝𝑓𝑚}({\mathrm{\Phi }}_2)$:

For every $𝔄\in \mathrm{𝑒𝑥𝑝𝑓𝑚}({\mathrm{\Phi }}_1)$, the structure ${\xi }^{\prime }(𝔄)$ on the same domain as $𝔄$ is obtained by replacing for every $𝔑\in n\text{-}\mathrm{𝑐𝑜𝑙𝑜𝑢𝑟𝑠}({\mathrm{\Phi }}_1)$ and every embedding $e\in \left(\genfrac{}{}{0pt}{}{𝔄}{𝔑}\right)$ the substructure $e(𝔑)$ of $𝔄$ by $e(\xi (𝔑))$.

Note that the second formulation makes it clear that ${\xi }^{\prime }(𝔄)$ is unique, because $n=\max (\mathrm{ar}({\mathrm{\Phi }}_1),\mathrm{ar}({\mathrm{\Phi }}_2))$. For the same reason, we have that ${𝔄}^{\tau }={\xi }^{\prime }{(𝔄)}^{\tau }$. Also observe that in the second formulation the well-definedness of ${\xi }^{\prime }$ is a non-trivial property since the required replacements might be on overlapping substructures.

We remark that this definition of a recolouring is compatible with the definition of a recolouring for the logic MMSNP given in [29, 12]. There, the unary existential symbols were interpreted as colours, and a recolouring was simply a mapping between the existential symbols which does not introduce any forbidden patterns. It is noteworthy, however, that in that case the compatibility on overlapping structures is trivially satisfied.

A general construction method of $\omega$-categorical homogeneous Ramsey structures was provided by Hubička and Nešetřil [25]. We use a variant of their result, which can be found in the appendix of [12] (Theorem A.4 in the print version, or Theorem A.3 in the arXiv version).

Besides the reduction to the connected case, the proof of Theorem 2 is a straightforward consequence of the combination of the following three intermediate results. First, Lemma 11 from Section 3.2 gives a (non-deterministic) double-exponential upper bound on the time complexity of finding a recolouring between two SNP sentences. Second, Proposition 14 below states that every connected GMSNP sentence is equivalent to an at most double-exponentially larger SNP sentence whose class of expanded finite models enjoys the AP and the RP. Third, Proposition 15 states that, for SNP sentences with the latter property, containment is equivalent to the existence of a recolouring. Here we are in fact very lucky that the parameters on which Lemma 11 and Proposition 14 depend doubly-exponentially are different – this will become clear in the proof of Theorem 2.

The proof of Proposition 14 below builds on on the proof of [11, Theorem 5], so we omit some details that can be found in [11].