Petr A Golovach
email: petr.golovach@uib.no.

Giannos Stamoulis
email: giannos.stamoulis@lirmm.fr

Dimitrios M Thilikos

Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes 1

Keywords: Algorithmic meta-theorems, Model-checking, First-order logic, Disjoint paths, Hadwiger number, Graph minors, Irrelevant vertex technique

The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate dp k (x 1 , y 1 , . . . , x k , y k ), expressing the existence of internally vertex-disjoint paths between x i and y i , for i ∈ {1, . . . , k}. This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every proper minor-closed graph class, model-checking for FOL+DP can be done in quadratic time. We also introduce an extension of FOL+DP, namely the scattered disjoint paths logic, FOL+SDP, where we further consider the atomic predicate s-sdp k (x 1 , y 1 , . . . , x k , y k ), demanding that the disjoint paths are within distance bigger than some fixed value s. Using the same technique we prove that modelchecking for FOL+SDP can be done in quadratic time on classes of graphs with bounded Euler genus.

Introduction

Logic plays a fundamental role in algorithmic research. It provides a universal language for formally describing computational problems and is important for the investigation of their computational complexity. In many cases, the accumulation of knowledge on algorithm design revealed that several algorithmic techniques have conceptual similarities that result from some common logical description of the problems where they apply. These similarities become effective when the inputs of the corresponding problems have certain structural characteristics. In some cases, this empirical evidence has been materialized in the so called Algorithmic Meta-Theorems (AMTs), a term introduced by Martin Grohe in [START_REF] Grohe | Logic and Automata: History and Perspectives[END_REF]. Such theorems typically provide two types of conditions, a logical one and a combinatorial one, such that every problem that is expressible by the logical condition can be solved efficiently when its inputs are restricted by the combinatorial condition. The importance of AMTs resides to the fact that they are able to unify wide families of computational problems (and also the algorithmic solutions for them) under a single model-theoretic/combinatorial framework (see [START_REF] Grohe | Logic and Automata: History and Perspectives[END_REF][START_REF] Grohe | Methods for algorithmic meta theorems[END_REF][START_REF] Kreutzer | Algorithmic meta-theorems[END_REF]).

AMTs for MSOL and FOL

Probably, the most prototypical AMT is known as Courcelle's Theorem proved in [START_REF] Courcelle | The monadic second-order logic of graphs. I. recognizable sets of finite graphs[END_REF] (see also [START_REF] Arnborg | Easy problems for tree-decomposable graphs[END_REF][START_REF] Borie | Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families[END_REF] and [START_REF] Dreier | Approximate evaluation of first-order counting queries[END_REF]), asserting that every problem on graphs that is expressible by a sentence ϕ in Monadic Second Order Logic (MSOL) can be solved in time 1 O |ϕ|,k (n), when restricted to graphs of treewith at most k. Clearly, when ϕ and k are fixed, this readily implies a linear-time algorithm. However, we prefer to display the dependencies on ϕ and k, under the O |ϕ|,k notation, so as to make clear that this theorem provides a linear-time parameterized2 algorithm, for every problem expressible in MSOL, when it is parameterized by treewidth.

Clearly, the logical/combinatorial compromise of Courcelle's theorem is not the only possible one. In fact, each AMT constitutes a different compromise between the logical and the combinatorial condition and a considerable amount of research in the theory of algorithms has been dedicated to the conception of alternative such compromises. Also, for particular logics, research has been dedicated to the identification of their combinatorial horizon, i.e., the most general combinatorial conditions that can accompany them in an AMT. For instance, for MSOL, the meta-algorithmic horizon is, under certain assumptions, delimited by the graph classes of bounded treewidth (see [START_REF] Bojanczyk | Definability equals recognizability for graphs of bounded treewidth[END_REF][START_REF] Ganian | Lower bounds on the complexity of mso 1 model-checking[END_REF][START_REF] Kreutzer | Lower bounds for the complexity of monadic secondorder logic[END_REF]).

Meta-algorithmics of FOL. Given that the meta-algorithmic limits of MSOL are fairly well understood, research on AMTs has been largely oriented to the meta-algorithmics of First-Order Logic (FOL). The two most powerful results in this direction concern two different types of combinatorial conditions. The first was given by Grohe, Kreutzer, and Siebertz in [START_REF] Grohe | Deciding first-order properties of nowhere dense graphs[END_REF] and is the graph class property of being nowhere dense. The second was given by Bonnet, Kim, Thomassé, and Watrigant in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] and is the graph class property of having bounded twin-width. We should stress here that the notion of being nowhere dense originates from a long line of research on graph sparsity, initiated by Nešetřil and Ossona de Mendez in [START_REF] Nesetril | The grad of a graph and classes with bounded expansion[END_REF] (see also [START_REF] Dvorák | Testing first-order properties for subclasses of sparse graphs[END_REF][START_REF] Kreutzer | Parameterized complexity of first-order logic[END_REF][START_REF] Kreutzer | Polynomial kernels and wideness properties of nowhere dense graph classes[END_REF][START_REF] Nesetril | On nowhere dense graphs[END_REF][START_REF] Nesetril | Sparsity -Graphs, Structures, and Algorithms[END_REF][START_REF] Pilipczuk | On the number of types in sparse graphs[END_REF]). On the other side, twin-width is a recently introduced graph parameter, defined in terms of sequences of vertex identifications (see [10, 17, 26, 28-36, 67, 93, 95, 122, 128, 153, 187, 191, 192, 201] for a sample of the vibrant current research on the algorithmic and combinatorial properties of twin-width). Seminal results on the above two combinatorial conditions indicate that, under certain assumptions, they approach the combinatorial horizon of FOL (see [START_REF] Dvorák | Testing first-order properties for subclasses of sparse graphs[END_REF] for nowhere density and [START_REF] Bonnet | Twin-width IV: ordered graphs and matrices[END_REF] for bounded twin-width). Research on the meta-algorithmics of FOL is nowadays quite active and has moved to several directions such as the study of FOL-interpretability [START_REF] Bonnet | Model checking on interpretations of classes of bounded local cliquewidth[END_REF][START_REF] Gajarský | First-order interpretations of bounded expansion classes[END_REF][START_REF] Nesetril | Rankwidth meets stability[END_REF][START_REF] Nesetril | Structural properties of the first-order transduction quasiorder[END_REF][START_REF] Nesetril | Linear rankwidth meets stability[END_REF][START_REF] Pilipczuk | Transducing paths in graph classes with unbounded shrubdepth[END_REF] or the enhancement of FOL with counting/numerical predicates [START_REF] Dreier | Approximate evaluation of first-order counting queries[END_REF][START_REF] Grohe | First-order query evaluation with cardinality conditions[END_REF][START_REF] Kuske | First-order logic with counting[END_REF][START_REF] Kuske | Gaifman normal forms for counting extensions of first-order logic[END_REF] (see also [START_REF] Eickmeyer | Succinctness of order-invariant logics on depth-bounded structures[END_REF][START_REF] Grange | Successor-invariant first-order logic on classes of bounded degree[END_REF][START_REF] Grohe | Locality of order-invariant first-order formulas[END_REF][START_REF] Van Den | Model-checking for successor-invariant first-order formulas on graph classes of bounded expansion[END_REF] for other extensions).

AMTs between FOL and MSOL. A challenging direction is the introduction of new logics whose expressive power is between FOL and MSOL that can lead to AMTs under combinatorial conditions that are less general than those applicable for FOL and more general than those applicable for MSOL. Two approaches that have been initiated in this direction are the following. The first direction is the introduction of compound logics that can express problems whose description combines both FOL and MSOL queries. Such a compound logic has been recently introduced in [START_REF] Fedor | A compound logic for modification problems: Big kingdoms fall from within[END_REF] and yielded AMTs that are applicable on a wide family of graph modification problems. The second direction is the extension of FOL with additional predicates that are not expressible in FOL. An important step in this direction was the introduction of the separator logic FOL+conn. This extension of FOL was introduced independently by Schirrmacher, Siebertz, and Vigny in [START_REF] Schirrmacher | First-Order Logic with Connectivity Operators[END_REF] and by Bojańczyk in [START_REF] Bojańczyk | Separator logic and star-free expressions for graphs[END_REF] (under the name separator logic), who considered, for every k ≥ 1, the general predicate conn k (x, y, z 1 , ..., z k ), that evaluates to true on a graph G if (the valuations of) x and y are joined in G by a path that avoids (the valuations) of the variables {z 1 , ..., z k }. According to the recent meta-algorithmic results of Pilipczuk, Schirrmacher, Siebertz, Toruńczyk, and Vigny in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF], every problem on graphs that is expressible by some formula ϕ ∈ FOL+conn can be solved in time O |ϕ|,r (n3 ), where r = hj(G) is the Hajós number 3 of G. Notice that this AMT implies the existence of parameterized algorithms on graph classes with bounded Hajós number for problems whose definition uses connectivity queries and therefore are not expressible in FOL. The most indicative example of a (meta-) problem displaying the expressibility power of FOL+conn is Elimination Distance to ϕ, asking whether the elimination distance of a graph G from some model of ϕ ∈ FOL is at most k. This problem is W[2]-hard (when parameterized by k) even for simple instantiations of ϕ [START_REF] Fedor | Parameterized complexity of elimination distance to first-order logic properties[END_REF], however, it admits a time O |ϕ|,k,r (n 3 ) algorithm when restricted to graph classes with Hajós number at most r, because of the results in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF]. For more examples of the expressibility power of FOL+conn, see [START_REF] Schirrmacher | First-Order Logic with Connectivity Operators[END_REF]. Also, in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF] it was proved that the tractability horizon of FOL+conn is, under certain assumptions, delimited by graph classes of bounded Hajós number.

AMTs for FOL+DP and extensions

As a next step towards a more expressive logic, Schirrmacher, Siebertz, and Vigny [START_REF] Schirrmacher | First-Order Logic with Connectivity Operators[END_REF] defined the, more expressive, disjoint-paths logic FOL+DP by adding, for every k, the atomic predicates dp k (x 1 , y 1 , . . . , x k , y k ) that evaluate to true if there are internally vertex-disjoint paths between (the valuations of) x i and y i , for all i ∈ {1, . . . , k}. In the same paper they defined 4 the logical hierarchy FOL+dp k that uses predicates for at most k disjoint paths and proved that these fragments of FOL+DP define a strict descriptive complexity hierarchy.

The challenging open question is whether an AMT exists for this logic, under some suitable combinatorial restriction that is more general than the one of having bounded treewidth (that is where Courcelle's theorem is applicable).

Our results. Given a graph G, we define the Hadwiger number of G, denoted by hw(G), as the maximum r for which G contains K r as a minor. 5 Our main result is the following AMT.

Theorem 1. Every problem on graphs that is expressible by some formula ϕ in FOL+DP can be solved by an algorithm running in time O |ϕ|,r (n 2 ), where r is the Hadwiger number of G. Some indicative (meta) problems whose standard parameterizations (i.e., those defined by the parameter k in their inputs) are automatically classified in FPT because of Theorem 1 are Minor Containment, Topological Minor Containment, Cyclability, Unordered Linkability, Ordered Linkability, F-Minor-Deletion, F-Topological Minor-Deletion, F-Contraction Deletion (for bounded genus graphs), Annotated F--Deletion, Subset F--Deletion, ϕ-Deletion, ϕ-Amalgamation, L-ϕ-Replacement, ϕ-Elimination distance, ϕ-Reconfiguration. For the definitions, the complexity, and the FOL+DP-expressibility of all these problems we refer the reader to Appendix A.

Our next step towards a more expressive logic, is to extend FOL+DP by considering, for every k ≥ 1, a more general form of predicate s-dp k (x 1 , y 1 , . . . , x k , y k ) where we now demand that the disjoint paths in question are pairwise s-scattered, i.e., there are no two vertices of two distinct paths that are within distance at most s. We call the new logic FOL+SDP. As 0-dp k (x 1 , y 1 , . . . , x k , y k ) = dp k (x 1 , y 1 , . . . , x k , y k ), we readily have that FOL+SDP is an extension of FOL+DP. Our second result is the following AMT.

Theorem 2. Every problem on graphs that is expressible by some formula ϕ in FOL+SDP can be solved by an algorithm running in time O |ϕ|,k (n 2 ), where k is the Euler genus of G. Some indicative problems whose standard parameterizations are automatically classified in FPT because of Theorem 2 are Induced Minor, Induced Topological Minor Containment, Contraction Containment, Induced Unordered Linkability, Induced Ordered Linkability, F-Induced Minor Deletion, F-Induced Topological Minor Deletion, ϕ-Deletion, ϕ-Amalgamation, L-ϕ-Replacement, ϕ-Elimination distance, ϕ-Reconfiguration. For the definitions, the complexity, and the FOL+SDP-expressibility of all these problems we refer the reader to Appendix A.

The irrelevant vertex technique

In Volume XIII of their Graphs Minors series, Robertson and Seymour introduced the celebrated irrelevant vertex technique in order design a time O k (n 3 ) algorithm for the following problem [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF].

Disjoint Paths

Input: a graph G and pairs (s 1 , t 1 ), . . . , (s k , t k ) of vertices of G. Question: Are there pairwise vertex-disjoint paths between s i and t i , for i ∈ {1, . . . , k}?

Notice that the description of the above problem does not fit in FOL. It demands the existence of k pairwise disjoint sets of vertices each inducing a connected graph containing the terminals s i and t i . While connectivity is expressible in MSOL it is known that it cannot be expressed in FOL (see e.g., [START_REF] Ebbinghaus | Finite model theory[END_REF][START_REF] Libkin | Elements of Finite Model Theory[END_REF]).

The general idea behind the irrelevant vertex technique is that if some part of the input graph is "sufficiently insulated" from the rest of the graph, then it may be irrelevant in the sense that the solution can be "reconfigured" away from it. When this idea applies, then this irrelevant part can be safely deleted and produce an equivalent, and simpler, instance of the problem.

The original application of the irrelevant vertex technique for the Disjoint Paths problem have had two phases:

• 1st phase: when the input graph G contains a big (as a function of k) clique minor • 2nd phase: when G minor-excludes a clique, that is G has small Hadwiger number.

Theorem 1 and Theorem 2 deal with the applicability of the 2nd phase. We next give a brief outline of how this phase was applied for the Disjoint Paths problem and, in particular, in the "non-trivial" situation where G has "big" treewidth. To deal with this situation, Robertson and Seymour proved in [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF] the so called Flat Wall Theorem, asserting that if a graph has small Hadwiger number and big treewidth, then after the removal from G of "few" vertices, called apex vertices, the resulting graph contains a big wall that is "flat". Intuitively, by the term "flat wall" we refer to a wall W whose perimeter P contains a separator S of G where the inner part of the wall is inside one of the connected components C of G \ V (S) and where no two disjoint (s i , t i )-paths, i ∈ {1, 2}, exist in the graph G[V (P ) ∪ V (C)], called the compass of W , where s 1 , s 2 , t 1 , and t 2 are vertices of S, appearing in this ordering in P . This flatness property implies that every set of homocentric cycles around the central part of the wall can act as a system of separators "insulating" the two central vertices of W from the part of the graph that lies outside the compass of the wall. With this structural result at hand, Robertson and Seymour proved that every set of k disjoint paths that may certify a yes-instance of the Disjoint Paths problem can be rerouted away from its central vertices, that is it they be declared irrelevant and be safely discarded from G. The proof of this rerouting argument is quite technical and was given in Volumes XXI and XXII of the Graph Minors series (this result is now known as the Unique Linkage Theorem -see [2, [START_REF] Golovach | Hitting topological minor models in planar graphs is fixed parameter tractable[END_REF][START_REF] Golovach | Combing a linkage in an annulus[END_REF]148,[START_REF] Mazoit | A single exponential bound for the redundant vertex theorem on surfaces[END_REF] for later proofs and improvements). Moreover, Kawarabayashi, Kobayashi, and Reed proved in [START_REF] Kawarabayashi | The disjoint paths problem in quadratic time[END_REF] that the flat wall W (and therefore its central vertices as well) can be found in linear time. Given now that a simpler equivalent instance of the Disjoint Paths problem is found, we may repeat the above procedure a linear number of times until the treewidth is "small" so that the problem can be solved by a dynamic programming algorithm (which exists because of Courcelle's theorem). This, taken into account the improvement of [START_REF] Kawarabayashi | The disjoint paths problem in quadratic time[END_REF], takes a total of O k (n 2 ) time.

The potential of irrelevant vertex technique. To adapt the above arguments for other problems has been a challenging enterprise for graph algorithm designers during the last 20 years. For a indicative (while not exhaustive) list of papers that made use of this technique, see [1, 14, 49, 81, 82, 84, 87, 89, 90, 100, 101, 111, 119, 127, 130, 133-136, 138, 142-146, 150, 167, 171, 197-200, 204]. Typically, for each problem, the challenge is to give an algorithm that is able to detect, in polynomial time, some vertex that can be declared irrelevant and then prove that this vertex is indeed irrelevant in the sense that discarding it from the input graph creates an equivalent instance. In some cases, apart from declaring a vertex irrelevant, "annotated versions" of problems have been considered and vertices may also be declared annotation-irrelevant in the sense that they can be safely excluded from the set of annotated vertices. This extended concept of irrelevancy was used in [START_REF] Golovach | The parameterized complexity of graph cyclability[END_REF] for the Cyclability problem and in [START_REF] Golovach | Hitting topological minor models in planar graphs is fixed parameter tractable[END_REF] for the F-Topological Minor-Deletion problem (see also the meta-algorithmic results in [START_REF] Fedor | A compound logic for modification problems: Big kingdoms fall from within[END_REF][START_REF] Fedor | An algorithmic meta-theorem for graph modification to planarity and FOL[END_REF][START_REF] Fedor | Modification to Planarity is Fixed Parameter Tractable[END_REF]). In our proof of Theorem 1 and Theorem 2 we largely make use of the annotation technology. In fact we consider an annotated set for the variables quantified in the FOL+DP formula.

Most of the problems that are amenable to the application of the irrelevant vertex technique have a common denominator: they are not FOL-expressible and they deal with graph classes with unbounded treewidth, that go beyond the combinatorial applicability of MSOL. Thus, they escape the logical/combinatorial conditions of the known meta-algorithmic technology of FOL and MSOL.

The proof of Theorem 1 and Theorem 2 is abstracting the irrelevant vertex technology of all the aforementioned problems into two AMTs. Theorem 1 (resp. Theorem 2) essentially indicates that, for graphs of bounded Hadwiger number (Euler genus), the descriptive potential of the Disjoint (Induced) Paths problem can be "embedded᾿᾿ inside FOL in the form of the predicates

dp k (x 1 , y 1 , . . . , x k , y k ) (s-dp k (x 1 , y 1 , . . . , x k , y k )).
What to do with a clique. Clearly Theorem 1 and Theorem 2 concern the 2nd phase of the irrelevant vertex technique where the Hadwiger number is bounded. At this point we wish to mention that the applicability of the 1st phase, concerning the question "what to do with a clique ", may vary depending on the problem in question. We distinguish three main categories of parameterized problems.

A. The first category contains standard parameterizations of problems, such as Minor Containment, F-Minor Amalgamation, F-Minor Deletion, or F-Minor Local Replacement, where Theorem 1 applies and, moreover, big enough Hadwiger number immediately certifies a yes-or a no-instance. Given that checking whether a clique K r is a minor of a graph can be done in time O r (n 2 ) [START_REF] Kawarabayashi | The disjoint paths problem in quadratic time[END_REF], for such problems, just FO+DP-expressibility is enough for implying that a problem is FPT, even in general graphs.

B. The second category of parameterized problems contains those where the 1st phase is nonapplicable in general, in the sense that they are already intractable. For instance, the standard parameterization of Cyclability or Subset Linkability, where Theorem 1 applies, is co-W[1]-hard and problems, where Theorem 2 applies, such as Induced Disjoint Paths, Contraction Containment, and Induced Minor Containment are NP-complete even for fixed values of the parameter (see [START_REF] Kawarabayashi | The induced disjoint paths problem[END_REF], [START_REF] Brouwer | Contractibility and NP-completeness[END_REF][START_REF] Levin | The computational complexity of graph contractions I: Polynomially solvable and NP-complete cases[END_REF][START_REF] Levin | The computational complexity of graph contractions II: Two tough polynomially solvable cases[END_REF], and [START_REF] Michael | The complexity of induced minors and related problems[END_REF][START_REF] Lévêque | Detecting induced subgraphs[END_REF] respectively).

C. The third category concerns standard parameterizations of problems, such as Disjoint Paths [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF], Topological Minor Containment [START_REF] Grohe | Finding topological subgraphs is fixed-parameter tractable[END_REF] , F-Topological Minor Deletion [START_REF] Fedor | Hitting topological minors is FPT[END_REF], F-TM Elimination Distance [START_REF] Agrawal | Deleting, eliminating and decomposing to hereditary classes are all fpt-equivalent[END_REF], and F-TM-Treewidth [START_REF] Agrawal | Deleting, eliminating and decomposing to hereditary classes are all fpt-equivalent[END_REF], where extra algorithmic machinery is employed for dealing with the 1st phase (typically related with the recursive understanding technique [START_REF] Cai | Random separation: A new method for solving fixed-cardinality optimization problems[END_REF]50,[START_REF] Grohe | Finding topological subgraphs is fixed-parameter tractable[END_REF][START_REF] Daniel Lokshtanov | Reducing CMSO Model Checking to Highly Connected Graphs[END_REF]). To our knowledge, there is no general treatment of the 1st phase, further than the results of [START_REF] Agrawal | Deleting, eliminating and decomposing to hereditary classes are all fpt-equivalent[END_REF][START_REF] Fedor | Hitting topological minors is FPT[END_REF][START_REF] Grohe | Finding topological subgraphs is fixed-parameter tractable[END_REF][START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF]. To investigate the meta-algorithmic conditions that may unify them, even for some combinatorial condition that is more general that having bounded Hadwiger number, is an interesting open challenge.

For more on the classification of the problems that are treated by Theorem 1 and Theorem 2 according to the above three categories, see Appendix A.

Organization of the paper. In Section 2, we provide an overview of our proof. In Section 3, we provide some basic definitions that will be used throughout the paper. In Section 4, we present a way to translate model-checking to (recursive) folio containment. Then, in Section 5, we give some additional definitions and results for dealing with collections of paths inside (partially planar) graphs. In Section 6, we present a trick to transform a disjoint paths query to one that can deal with the presence of some apex vertices that can "spoil" flatness and in Section 7 we present the combinatorial result that supports the correctness of the main subroutine of the algorithm of Theorem 1 and Theorem 2. Next, in Section 8, we present the proof of Theorem 1 and in Section 9 we present the proof of Theorem 2. We conclude the paper with Section 10. In Appendix A we present a list of problems expressible in FOL+DP and in FOL+SDP and in Appendix B we present the flat wall framework that we use in this paper, which was introduced in [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]. Appendix C contains missing complexity proofs of problems mentioned in Section 10 and Appendix A.

Overview of the proof

In this section we summarize the main ideas involved in the proof of Theorem 1 and Theorem 2. We describe our approach for graphs. However, our results are proven for colored graphs (i.e., graphs equipped with a sequence of subsets of their vertex set).

General scheme of the algorithm

For our algorithms we follow the typical motif of the irrelevant vertex technique: if the treewidth of the input graph G is upper-bounded by an appropriately chosen function, depending only on the sentence ϕ ∈ FOL+DP and hw(G), then because of Courcelle's Theorem [START_REF] Courcelle | The monadic second-order logic of graphs. I. recognizable sets of finite graphs[END_REF][START_REF] Courcelle | The monadic second-order logic of graphs III: tree-decompositions, minor and complexity issues[END_REF][54] we can check whether G satisfies ϕ in linear time, using the fact that FOL+DP is a fragment of MSOL (see Subsection 3.3). Otherwise, if the treewidth is "large enough", we identify an irrelevant vertex in linear time, that is a vertex whose removal does not affect satisfiability of ϕ. This highly non-trivial procedure of finding an irrelevant vertex is our main goal and, in what follows, we describe in an intuitive level the main ingredients of this approach.

Irrelevant vertices for model-checking. Applying the irrelevant vertex technique in a modelchecking setting demands the restriction of the part of the graph that is used to interpret variables and predicates of the sentence. To show that a vertex is irrelevant, one has to prove that whether the given sentence is satisfied or not does not depend on the presence of this vertex inside the graph. The "building blocks" of our sentences are either first-order variables (quantified by universal or existential quantifiers), or interpretations of relation symbols of the given vocabulary (in our case, these are edges and colors in the vertices), or disjoint-path predicates between some of the already quantified first-order variables. Towards building an irrelevant vertex argument, an essential step is to reduce the scope of the quantification of the variables, while preserving the satisfiability status of the sentence. The fact that a vertex can be discarded from the scope of a quantifier, permits to declare it annotation-irrelevant with respect to this quantifier. Moreover, even if some vertex is annotation-irrelevant with respect to all quantifiers, this vertex could still be important for the existence (or not) of disjoint paths between vertices (that are picked inside the annotation). Such a vertex can be removed from the graph, therefore be declared problem-irrelevant, only if we can guarantee that disjoint paths can be safely rerouted away from it. The pursue of such a problemirrelevant vertex is executed inside a "big enough" bidimensional area of vertices that are annotationirrelevant for all quantifiers. While this does not deviate from the "typical" rerouting arguments of the irrelevant vertex technique, dealing with the restriction of the annotation is the most demanding part. In the rest of this section, we aim to demonstrate a way to tackle this problem.

Translating model-checking to (recursive) folio containment

Our main tool in order to create equivalent (annotated) instances is to express model-checking in graph-theoretic terms. Throughout this section, we assume that all sentences are given in prenexnormal form, i.e., ϕ = Q 1 x 1 . . . Q r x r ψ(x 1 , . . . , x r ), where Q 1 , . . . , Q r ∈ {∀, ∃}, x 1 , . . . , x r are firstorder variables, and ψ(x 1 , . . . , x r ) is a quantifier-free formula with x 1 , . . . , x r as free variables.

Assigning annotated graphs to rooted trees. Our first step (Section 4) is to interpret the satisfaction of a sentence ϕ from a graph in terms of the existence of a subtree inside a tree where the graph is embedded, such that the bifurcations of this subtree correspond to the quantifiers of ϕ and the vertices collected in each root-to-leaf path evaluate to true the quantifer-free "tail" of ϕ. These trees, known as game trees, appear with different names in the literature, like evaluation trees [START_REF] Gajarský | Differential games, locality, and model checking for FO logic of graphs[END_REF] or morphism trees [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] (see also [START_REF] Grädel | Automata, logics, and infinite games: a guide to current research[END_REF]). These trees follow the recursive structure of a set sig r (G, R). This set, called signature of (G, R), is defined as the recursive collection of the different types of tuples v 1 , . . . , v i i ≤ r of vertices of R (see the definition in Subsection 4.1). We can construct a rooted tree (T, t 0 ) following the recursive structure (of depth r) of this set and this naturally gives a mapping of each node of the tree to the vertex of G of a particular type (when considering the tuple of all ancestors of it). We call this mapping an assignement of (G, R) to (T, t 0 ). Intuitively, every root-to-leaf path is mapped to a tuple of (possibly repeating) vertices v 1 , . . . , v r , where v i ∈ R, for every i ∈ {1, . . . , r} (see Figure 1). Also, we define a ϕ-spanning subtree of a rooted tree to be the (sub)tree T with the same root that is obtained following the quantifiers of ϕ, i.e., if Q i = ∃, then every node of T of depth i has only one child in T , while if Q i = ∀, every node of T of depth i bifurcates (in T ) to all its children in T (see Figure 1 for an example). In this setting, an (annotated

) formula ϕ = Q 1 x 1 ∈ R . . . Q r x r ∈ R ψ(x 1 , . . . , x r ) is satisfied from a tuple (G, R) iff
there is an assignment of (G, R) to a rooted tree and a ϕ-spanning subtree of this tree such that for every root-to-leaf path of the ϕ-spanning subtree, the formula ψ is satisfied when interpreting its free variables as the vertices collected in this path (Observation 2).

Patterns and pattern-coloring. A crucial observation that is central to our approach is the following: for every quantifier-free formula ψ(x 1 , . . . , x r ) ∈ FOL+DP, given a graph G and a tuple of vertices (v 1 , . . . , v r ) of G, the question whether ψ is satisfied when x 1 , . . . , x r are interpreted as v 1 , . . . , v r boils down to checking whether edges and/or disjoint paths between particular pairs from v 1 , . . . , v r (indicated by the atomic formulas of ψ) are present in G. For this reason, we define the pattern of a boundaried graph (G, v 1 , . . . , v r ) to be an encoding of the edges and the disjoint paths between all pairs in v 1 , . . . , v r in G. Note that, knowing the pattern of a boundaried graph, we can determine which quantifier-free formulas in FOL+DP are evaluated to true in this graph and which do not. Therefore, when considering a graph assigned in a rooted tree, we can "color" each leaf of the tree by the pattern of the corresponding boundaried graph (G, v 1 , . . . , v r ), where v 1 , . . . , v r are the vertices collected in the corresponding root-to-leaf path. This, we call the pattern-coloring of the leafs. Also, we introduce encoding in terms of patterns for formulas, i.e., we define the pattern of every clause of a quantifier-free formula, that encodes the presence (or not) of predicates or their nagation. This allows to restate Observation 2 and formulate model-chacking as the search of a ϕ-spanning tree with particular colors in its leafs, inside a leaf-colored tree (to which the annotated graph is assigned) where colors are given by the pattern-coloring (Observation 6). See Figure 1.

Same (recursive) patterns imply satisfaction of the same formulas. Our intuition is that for every graph G, the information encoded by the patterns, organised in a recursive tree structure as described above, is sufficient to evaluate every sentence in FOL+DP of a given number of quantifiers. In Subsection 4.4, we formalize this intuition by defining equivalence of leaf-colored trees and proving that two annotated graphs (G, R), (G , R ) that have the same recursive patterns for depth r (i.e., sig r (G, R) = sig r (G , R )) satisfy the same sentences in FOL+DP (Lemma 2). The proof of Lemma 2 is an induction on the numbers of quantifiers of a sentence.

We use Lemma 2 in the course of the proof of Theorem 3 in the following way: As long as we can find a set R ⊆ V (G) such that R ⊆ R and (G, R) and (G, R ) have the same signature, we can safely

R = { } G = (T, t 0 )
T Figure 1: An example of an assignment of an annotated graph (G, R) (depicted on the upper left part of the figure) to a rooted tree (T, t 0 ) (in the center of the figure). We use colors for each vertex of G in order to distinguish them, without using indices and we use colors in the nodes of T to show where each vertex of G is mapped to. The small graphs below each leaf of T encode the pattern-coloring, i.e., are the (boundaried) graphs induced by the vertices collected in each root-to-leaf path of T and the linear orderings of their vertex sets (from left to right) follow the ordering of the corresponding path. Vertices that are picked twice in the same path are drawn inside a same-colored bag (respecting the ordering). The subtree T is a ϕ-spanning subtree of (T, t 0 ) for the

FOL-sentence ϕ = ∃x 1 ∈ R ∀x 2 ∈ R ∃x 3 ∈ R (x 1 = x 2 ∨ E(x 2 , x 3 )), that certifies that (G, R) |= ϕ.
reduce the former instance to the latter and report progress. Finding the set R is not straightforward and in the next subsection we explain how to deal with this situation. Moreover, in our reduction, we will find a bidimensional annotation-irrelevant area and return a problem-irrelevant vertex v, i.e., a vertex v such that (G, R) and (G \ v, R ) are also equivalent. Finally, we reduce to an instance (G , R ) with the same r-signature as the input graph (i.e., sig r (G, V (G)) = sig r (G , R ), where the treewidth of G depends only on r and the minor we exclude. Then, following the tree-like assignment given by the signature, we can evaluate any FOL+DP sentence of quantifier rank at most r. This latter is done by applying Courcelle's theorem.

Combinatorial trick to compute folios

Our main difficulty is to compute recursive folios of the given annotated graph and obtain a different annotation that gives the same recursive patterns. To tackle this, we need some further tools to handle disjoint paths. From a high-level point of view, our approach considers expressing "partial" patterns inside a bounded treewidth part of the given graph. Using Courcelle's Theorem, we can compute partial patterns and the boundary (tuples of) vertices that give rise to these patterns.

Flat walls with bounded treewidth compasses. In the introduction, we already sketched a definition of flat walls, originating in the work of Robertson and Seymour [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF]. An alternative intuition for a flat wall is to see it as a structure made up of (not necessarily planar) pieces, called flaps, that are glued together with boundaries of size at most three, in a way that follows the bidimensional structure of a wall. In this article, we use the framework recently introduced in [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF] that provides a more accurate view on some previously defined notions on flat walls, particularly in [START_REF] Kawarabayashi | A new proof of the flat wall theorem[END_REF] (see Appendix B for formal definitions). In the course of our main algorithm, we use a variant of the Flat Wall Theorem proved in [START_REF] Kawarabayashi | A new proof of the flat wall theorem[END_REF][START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF] (see Proposition 9) that provides a guarantee that the compass of the flat wall has bounded treewidth. This permits us, because of Courcelle's Theorem, to answer in linear time MSOL-queries inside the compass.

In fact, for our arguments, instead of working with a flat wall, we work with a flat railed annulus (contained inside the flat wall). This is a structure similar to a flat wall, whose "underlying" structure is not a wall but a sequence of nested cycles transversed by some disjoint paths, called rails. See Figure 2.

A w0 A w1
Figure 2: An illustration of a (flat) railed annulus and a linkage (depicted in red) that is combed through some prescribed vertices of the railed annulus (depicted in orange).

Routing linkages through railed annuli. Recall that, the pattern of a boundaried graph (G, v 1 , . . . , v r ), apart from the edges between v 1 , . . . , v r , also encodes the existence or not of disjoint paths between pairs of the boundary vertices v 1 , . . . , v r . We are interested in the ways such a pattern may cross a cycle C of the railed annulus. To define a notion of "partial" pattern (i.e., the one "cropped" by a "central-enough" cycle C), we have to deal with the possibe ways that v 1 , . . . , v r can be connected through disjoint paths crossing C and this can be seen as a question about the variety of linkages, i.e., collections of disjoint paths, that can be routed between boundary vertices and the way they may cross C. Clearly, a linkage may transverse C in a quite entagled way, so that the partial pattern of (G, v 1 , . . . , v r ) cropped by C may have an unbounded number of additional boundary vertices on C. In order to deal with this situation, we make use of a special result for handling linkages, that is the Linkage Combing Lemma (Proposition 2) proved in [START_REF] Golovach | Combing a linkage in an annulus[END_REF] (which has appeared before in [START_REF] Golovach | Hitting topological minor models in planar graphs is fixed parameter tractable[END_REF]). This result is applied on partially annulus-embedded graphs, i.e., graphs that contain some subgraph K that is embedded in an annulus ∆ and ∆ separates the two other parts of the graph obtained after removing the vertices inside ∆. The Linkage Combing Lemma intuitively says that in the presence of an annulus-embedded railed annulus A inside a partially annulus-embedded graph G, every linkage L of G whose terminals are outside the annulus can be "combed", i.e., it can be routed throught the cycle C of A in a predefined number of vertices. This allows us to represent every linkage encoded in the partial pattern by a "combed" linkage with a few predefined additional terminals on C.

Applicability of the Linkage Combing Lemma. To encode the recursive patterns of a graph, we have to keep the pattern of the graph for every choice of the boundary tuple. Therefore, for each tuple of vertices, we have to encode all linkages between pairs of vertices in the tuple. The trace of each tuple indicates which (sub)annulus of the flat railed annulus remains "terminal-free" (see Figure 2). This railed annulus is flat but we can consider its leveling (see Subsection B.7), that is a planar representation of it, obtained by contracting the interior of the flaps to single vertices. We observe that for every linkage whose terminals are outside the compass of the flat railed annulus, there is an equivalent linkage in the graph obtained after replacing the flat railed annulus with its leveling (see Lemma 12). Therefore, the question for linkages between pairs of boundary vertices can be translated to an equivalent one in the partially annulus-embedded graph obtained after considering the leveling (this graph is different for every different trace). This allows for the application of the Linkage Combing Lemma.

Partial patterns. Using the Linkage Combing Lemma we can assume that, for each tuple of vertices, every linkage between these vertices has an appropriate part of the initial (flat) railed annulus where it is combed. This implies that the pattern of a boundaried graph can be "separated" to two parts, the one on the "inner" part and one on the "outer" part of the annulus corresponding to the trace of the boundary tuple. Therefore, we can encode partial patterns by considering boundaried graphs whose boundary vertices are the vertices of the rails where we comb the linkages and some vertices that are on the "inner side" of this annulus. Vertices can also be on the "outer side" of this annulus and thus we have to suitably encode their absence from the tuple (see Subsection 7.3).

Dealing with apices. Having sketched how to route linkages (that correspond to disjoint path queries of FOL+DP) in flat walls, it remains to discuss how the presence of apices, that are few vertices that can have neighbors inside the wall in a completely uncontrolled way. The high-level idea here is to define a way to syntactically interpret these (few) apices by adding some extra colors in the structure for the neighborood of each apex vertex, remove the edges between apices and the rest of the graph and translate a disjoint path query in the original graph to some disjoint path queries in the new colored graph, encoding possible ways that the original paths could enter/exit the apex set. This idea originates in [START_REF] Flum | Fixed-parameter tractability, definability, and model-checking[END_REF] for FOL (without annotation) and an analogous version it was given in [START_REF] Fedor | A compound logic for modification problems: Big kingdoms fall from within[END_REF].

Apex-projections of sentences. To define this translation, we first need to define the "projection" of a sentence with respect to an apex-tuple a (see Subsection 6.1). In fact, first we define the "projection" of the graph G with respect to an apex-tuple a, by removing all edges between the vertices in a and the rest of the vertices of the graph and "coloring" the neighborhood of each a ∈ a by a specific color. This transformation of the graph allows us to "isolate" the apex-tuple and encode its adjacencies with the rest of the graph using colors. In terms of sentences, we define the apex-projection ϕ l of a sentence ϕ ∈ FOL+DP, where l = |a|, as a sentence that uses these new colors in order to interpret the original sentence ϕ in the "projected" graph. We stress that the apex-projected sentence ϕ l has larger quantifier rank, i.e., we quantify more variables, since one has to guess which (colored) vertices are the entry and exit points of the paths using vertices in the apex-tuple (see Observation 9).

Partial signatures. The next step is to build "meta-collections" of partial patterns. For this, in Subsection 7.4, we define the notion of partial signatures. This is a recursive definition, that in the base case is the pattern of a boundaried graph (whose boundary is a tuple of vertices together with the "combing-points" of the railed annulus corresponding to the trace of the given tuple) and every recursive step asks for all possible partial signatures that can be obtained after fixing another (boundary) vertex (inside the annotated set) or its absence. Intuitively, given an annotated graph (G, R) that contains a sufficiently big flat railed annulus, the partial signature of G encodes the recursive collection of (partial) patterns in the "inner" part of the railed annulus.

Exchangability of graphs with the same partial signature. After defining partial signatures, we prove that in the presence of a railed annulus flatness pair inside an (annotated) graph (H, R), two (annotated) graphs (G, R), (G , R ) that yield the same partial signature when "glued in the inner part" of (H, R), have the same (global) signature when we additionally glue another (annotated) colored graph (F, R ) in the outer part of (H, R) (see Lemma 5). The main idea of the proof of Lemma 5 is to show that equivalence of partial signatures implies equivalence of (global) signatures. Here, we have to demand equality of partial signatures of "larger depth" than the one that we aim for, in order to be able to deal with the extra quantifiers obtained after apex-projecting the quantifier-free formulas given by the pattern. This translation (to the apex-projection) is essential, in order to obtain a flat structure (without edges to the apiecs) where our rerouting arguments for the linkages can work. In particular, proving equivalency of signatures boils down to formalizing all arguments mentioned in the above paragraph that use the Linkage Combing Lemma, using a double inductive argument, in order to deal with the recursive nature of the definitions. The main importance of Lemma 5 is that it guarantees exchangeability (in terms of signatures) of graphs with the same partial signature and allows to shift our pursue of graphs of same signature to pursue of graphs of same partial signature.

Computing representatives. Since the partial signature of an annotated graph depends only on adjacency and linkage questions inside the "inner" part of a given flat railed annulus of the given graph, we can express the partial signature of the annotated graph in MSOL. Also, as we mentioned before, we can ask the part of the graph, where we want to compute partial signature, to have bounded treewidth. Therefore, we can define equivalence between vertices of the same partial signatures and using Courcelle's Theorem we can compute representatives of these equivalence relations (see Subsection 8.1). Therefore, given an annotated graph (G, R), an apex-tuple a of G, and a "big enough" flat railed annulus of G \ V (a), where V (a) is the set of vertices in a, that "crops" a bounded treewidth graph, we can compute a set R such that R ⊆ R and the size of the intersection of R with the "left cropped part" of the railed annulus is upper-bounded by a function of k, and moreover (G, R) and (G, R ) have the same partial signature (see Lemma 6). Therefore, in the presence of a big enough flat wall (of bounded treewidth) inside an annotated graph, we can bound the number of annotated vertices in the inner part of the railed annulus, which, in turn, permits us to declare annotation-irrelevant the vertices of some "central" part of the flat wall that contains the railed annulus (Lemma 7).

Wrapping-up the proof of Theorem 3. As mentioned in the beginning of this section, the most demanding part of our proof is reducing the annotation set, i.e., to show Lemma 7. Then, given that the set R, in which we build the signatures, leaves some big enough bidimensional area "annotation-irrelevant", it remains to compute a vertex inside this area whose removal does not affect the existence (or not) of any linkage between the interpretations of the variables in the definition of signature. This is done using known irrelevant vertex technique arguments (see Subsection 8.2 and in particular Lemma 8). Therefore, we can find a vertex that is irrelevant for the signature (Lemma 9). This produces an equivalent instance (G , R ) as required for the application of the main procedure of our algorithm.

From disjoint to scattered paths. To deal with FOL+SDP and prove Theorem 4, we need a Linkage Combing Lemma for scattered linkages. Such kind of a result is known when we restrict ourselves to graphs of bounded Euler genus and is proved in [START_REF] Golovach | Combing a linkage in an annulus[END_REF] (Proposition 5; see also [START_REF] Kawarabayashi | A linear time algorithm for the induced disjoint paths problem in planar graphs[END_REF][START_REF] Mazoit | A single exponential bound for the redundant vertex theorem on surfaces[END_REF]). Then, using this result, we follow the same approach as in the proof of Theorem 3, and we prove tractability of model-checking for FOL+SDP for graphs of embedded in some fixed surface (Theorem 4). We refer the reader to Section 9 for more details.

Preliminaries

In this section we present some basic definitions and we state our main result (Theorem 3). In Subsection 3.1, we start with some definitions on graphs and in Subsection 3.2 we define first-order and monadic second-order logic. Then, in Subsection 3.3 we define the extension of FOL with disjoint paths predicates and we state our main result (Theorem 3).

Basic definitions

Integers, sets, and tuples. We denote by N the set of non-negative integers. Given two integers p and q, the set [p, q] refers to the set of every integer r such that p ≤ r ≤ q. For an integer p ≥ 1, we set [p] = [1, p] and

N ≥p = N \ [0, p -1]
. Given a non-negative integer x, we denote by odd(x) the minimum odd number that is not smaller than x. For a set S, we denote by 2 S the set of all subsets of S and, given an integer r ∈ [|S|], we denote by S r the set of all subsets of S of size r. Given two sets A, B and a function f : A → B, for a subset X ⊆ A we use f (X) to denote the set {f (x) | x ∈ X}. Given a set X and an r ∈ N, we use X r to denote the product

X × • • • × X of r copies of X.
Let S be a collection of objects where the operations ∪ and ∩ are defined. Given two tuples x = (x 1 , . . . , x l ) and y = (y 1 , . . . , y l ), where x i , y i ∈ S, we denote x ∪ y = (x 1 ∪ y 1 , . . . , x l ∪ y l ) and x ∩ y = (x 1 ∩ y 1 , . . . , x l ∩ y l ). Also, we denote S = X∈S X.

Basic concepts on graphs. All graphs considered in this paper are undirected, finite, and without loops or multiple edges. We use standard graph-theoretic notation and we refer the reader to [START_REF] Diestel | Graph Theory[END_REF] for any undefined terminology. Let G be a graph. Given a vertex v ∈ V (G), we denote by N G (v) the set of vertices of G that are adjacent to v in G. For S ⊆ V (G), we set G[S] = (S, E ∩ S 2 ) and use the shortcut G \ S to denote G[V (G) \ S]. The length of a path P of G is the number of edges of P .

Minors. The contraction of an edge e = {u, v} of a simple graph G results in a simple graph G obtained from G \ {u, v} by adding a new vertex uv adjacent to all the vertices in the set

N G (u) ∪ N G (v) \ {u, v}. A graph G is a minor of a graph G, denoted by G m G, if G can
be obtained from G by a sequence of vertex removals, edge removals, and edge contractions. Given a finite collection of graphs F and a graph G, we use the notation F m G to denote that some graph in F is a minor of G. Given a set of graphs F, we denote by Excl(F) the set containing every graph that excludes all graphs in F as minors. A graph class G is minor-closed if every minor of a graph in G is also a member of G. The Hadwiger number of a graph G, denoted by hw(G), is the minimum k where G ∈ Excl({K k }) and K k is the complete graph on k vertices. A minor-closed graph class is called proper if it is not the class of all graphs.

Treewidth. A tree decomposition of a graph G is a pair (T, χ) where T is a tree and χ :

V (T ) → 2 V (G) such that • t∈V (T ) χ(t) = V (G),
• for every edge e of G there is a t ∈ V (T ) such that χ(t) contains both endpoints of e, and

• for every v ∈ V (G), the subgraph of T induced by {t ∈ V (T ) | v ∈ χ(t)} is connected.
The width of (T, χ) is equal to max |χ(t)| -1 t ∈ V (T ) and the treewidth of G is the minimum width over all tree decompositions of G.

First-order logic and monadic second-order logic

In this subsection, we give the definition of first-order and monadic second-order logic. We define these logics on relational vocabularies with constant symbols and we work with structures of these vocabularies.

Structures. A vocabulary is a finite set of relation and constant symbols (we do not use function symbols). Every relation symbol R is associated with a positive integer that is called the arity of R, which we denote ar(R). A structure A of vocabulary τ , in short a τ -structure, consists of a non-empty set V (A), called the universe of A, an r-ary relation R A ⊆ V (A) r for each relation symbol R ∈ τ of arity r ≥ 1, and an element6 c A ∈ {␣} ∪ V (A) for each constant symbol c ∈ τ . We refer to R A (resp. c A ) as the interpretation of the symbol R (resp. c) in the structure A. A structure A is finite if its universe V (A) is a finite set. We denote by STR[τ ] the set of all finite τ -structures.

We say that a τ -structure A is isomorphic to a τ -structure B if there is a bijection V (A) ∪ {␣} to V (B) ∪ {␣}, such that π(␣) = ␣ and for every k ≥ 1, every relation symbol R ∈ τ of arity k, and every (a 1 , . . . , a k ) ∈ V (A) k , it holds that (a 1 , . . . , a k ) ∈ R A ⇐⇒ (π(a 1 ), . . . , π(a k )) ∈ R B and for every constant symbol c ∈ τ, it holds that π(c A ) = c B .

Given two τ -structures A and B, where for every constant symbol c ∈ τ either c A = c B or c A = ␣ ∨ c B = ␣, we define the disjoint union of A and B, and we denote it by A ∪B, as the τ -structure where

V (A ∪B) is the disjoint union of V (A) \ {␣}, V (B) \ {␣} and {␣}, for every relation symbol R ∈ τ, R A ∪B = R A ∪ R B , and for every constant symbol c ∈ τ , if c A = c B , then c A ∪B = c A = c B , and if c A = ␣ (resp. c B = ␣), then c A ∪B = c B (resp. c A ∪B = c A ).
An undirected graph without loops can be seen as an

{E}-structure G = (V (G), E G )
, where E G is a binary relation that is symmetric and anti-reflexive.

The Gaifman graph G A of a τ -structure A is the graph whose vertex set is V (A) and two vertices x, y are adjacent if there is an R ∈ τ and a v ∈ R A such that both x and y are elements of v.

First-order logic and monadic second-order logic. We now define the syntax and the semantics of first-order logic and monadic second-order logic of a vocabulary τ. We assume the existence of a countable infinite set of first-order variables, usually denoted by lowercase symbols x 1 , x 2 , . . . , and of a countable infinite set of set variables, usually denoted by uppercase symbols X 1 , X 2 , . . . . A first-order term is either a first-order variable or a constant symbol. A first-order logic formula, in short FOL-formula, of vocabulary τ is built from atomic formulas x = y and (x 1 , . . . , x r ) ∈ R, where R ∈ τ and has arity r ≥ 1, on first-order terms x, y, x 1 , . . . , x r , by using the logical connectives ∨, ∧, ¬ and the quantifiers ∀, ∃ on first-order variables. We denote by FOL[τ ] the set of all FOL-formulas of vocabulary τ.

A monadic second-order logic formula, in short MSOL-formula, of vocabulary τ is obtained by enhancing the syntax of FOL-formulas by allowing the atomic formulas x ∈ X, for some first-order term x and some set variable X, and allowing quantification on both first-order and set variables. We denote by MSOL[τ ] the set of all MSOL-formulas of vocabulary τ. We make clear that what we call here MSOL is what is commonly referred in the literature as MSO 1 , in which, for the vocabulary of graphs, first-order variables are interpreted as vertices and set variables are interpreted as sets of vertices.

The formulas in FOL[τ ] and MSOL[τ ] are evaluated on τ -structures by interpreting every symbol in τ as its interpretation in the structure and every first-order (resp. set) variable as an element (resp. set of elements) of the universe of the structure. Given a formula ϕ, the free variables of ϕ are its variables that are not in the scope of any quantifier. We write ϕ(x 1 , . . . , x k ) to indicate that the free variables of the formula ϕ are x 1 , . . . , x k . A sentence is a formula without free variables. Let ϕ = Q 1 x 1 . . . Q r x r ψ(x 1 , . . . , x r ) be a sentence, where for each i ∈ [r], Q i ∈ {∀, ∃}, x 1 , . . . , x r are first-order variables, and ψ(x 1 , . . . , x r ) is a quantifier-free formula with free variables x 1 , . . . , x r . We call r the quantifier rank of ϕ.

Given a τ -structure A, a formula ϕ(x 1 , . . . , x k ) ∈ FOL[τ ], and a 1 , . . . , a k in V (A), we write A |= ϕ(a 1 , . . . , a k ) to denote that ϕ(x 1 , . . . , x k ) holds in A if, for every i ∈ [k], the variable x i is interpreted as a i . Given a k ∈ N, two formulas ϕ(x 1 , . . . , x k ), ψ(x 1 , . . . , x k ) ∈ FOL[τ ] are equivalent if for every τ -structure A and every a 1 , . . . , a k ∈ V (A), we have A |= ϕ(a 1 , . . . , a k ) ⇐⇒ A |= ψ(a 1 , . . . , a k ).
We call the set {A ∈ STR[τ ] | A |= ϕ} the set of models of ϕ and we denote it by Mod(ϕ).

Disjoint paths logic

For the rest of this paper, we deal with colored graphs, i.e., we fix a vocabulary τ that contains a binary relation symbol E that is always interpreted as a symmetric and anti-reflexive binary relation (corresponding to the edges of the graph) and a collection of unary relation symbols Y 1 , . . . , Y h (corresponding to colors on the vertices of the graph). We call such a vocabulary a colored-graph vocabulary. Also, we always assume that the interpretations of Y 1 , . . . , Y c are always pairwise disjoint (if not, then we introduce extra unary relations symbols for each intersection).

Disjoint-paths logic. We define the 2k-ary predicate dp k (x 1 , y 1 , . . . , x k , y k ), which evaluates true in a τ -structure G if and only if there are paths P 1 , . . . , P k of (V (G), E G ) of length at least 2 between (the interpretations of) x i and y i for all i ∈ [k] such that for every i, j

∈ [k], i = j, V (P i )∩V (P j ) = ∅. We let τ + dp := τ ∪ {dp k | k ≥ 1},
where each dp k is a 2k-ary relation symbol. We use dp instead of dp k when k is clear from the context. Our main result is the following (slightly more general) version of Theorem 1: Theorem 3. For every colored-graph vocabulary τ and every sentence ϕ ∈ FOL[τ + dp], there exists an algorithm that, given a τ -structure G of size n, outputs whether

G |= ϕ in time O |ϕ|,hw(G) (n 2 ).

An alternative view to first-order logic model-checking

In this section we present an alternative way to interpret first-order logic model-checking, by embedding a given graph to a (rooted) tree. In Subsection 4.1, we translate the problem of whether a graph satisfies a formula ϕ to the search of a subtree of the tree in which the graph is embedded, such that the bifurcations of this subtree correspond to the quantifiers of ϕ and the vertices collected in each root-to-leaf path satisfy the quantifier-free "tail" of ϕ. We also formally define the notion of signature of a graph that encodes in a tree-like way how tuples of vertices satisfy quantifier-free formulas of FOL[τ +dp]. In Subsection 4.2, we define the notion of pattern of a colored graph G together with some vertices v 1 , . . . , v r ∈ V (G). This notion is used to encode the way all quantifierfree FOL[τ +dp]-formulas can be satisfied by G when interpreting the variables as v 1 , . . . , v r . This way, we also define the respective notion of patterns of quantifier-free FOL[τ +dp]-formulas and, in Subsection 4.3, we formulate model-checking in these terms (Observation 6). Finally, in Subsection 4.4, we prove the main result of this section (Lemma 2), which intuitively states that two graphs that have the same signatures (or, in other words, the same recursive patterns) satisfy the same sentences.

Embedding model-checking to trees

In this subsection we present a way to embed graphs to trees and how to trace the satisfaction of a sentence from the given graph, in terms of subtrees of the original tree.

Rooted trees. Let (T, t 0 ) be a rooted tree. Given a node x of T , we denote by T x the subtree of T rooted at x. We use L(T ) to denote the leaves of T . For every i ∈ [0, r], where r ∈ N is the height of T , we use D i (T ) to denote the set of nodes of T that are at distance i from t 0 . We say that a node t ∈ V (T )

has depth i if t ∈ D i (T ), i ∈ [0, r].
In this paper, for every rooted tree (T, t 0 ) of height r that we consider, we assume that L(T ) = D r (T ). We use Paths(T ) to denote the set of all root-to-leaf paths of T . We denote by children T (t) the set of all children of t in T . Also, when it is clear from the context, we use (t 0 , . . . , t r ) to denote a path P ∈ Paths(T ) such that V (P ) = {t 0 , . . . , t r } and E(P ) = i∈[0,r-1] {{t i , t i+1 }}. A rooted tree (T, t 0 ) of height r is called n-ary, if each node of depth at most r -1 has n children.

Trees expressing quantification of formulas. We now express how, given a rooted tree (T, t 0 ) and a sentence ϕ, where the height of the tree and the quantifier rank of ϕ are the same, use the quantifier alternation of ϕ to construct a subtree T of T . This is done in the following recursive way: the subtree starts from t 0 and, for every t ∈ V (T ), if the considered quantifier of ϕ is the universal one, then T spans to all children of t, while if we have the existential one, T arbitrarily choses one child of t. We proceed to formalize this idea.

Let τ be a colored-graph vocabulary. Let ϕ = Q 1 x 1 . . . Q r x r ψ(x 1 , . . . , x r ) be an FOL[τ + dp]sentence and let (T, t 0 ) be a rooted tree of height r (where each root-to-leaf path has r + 1 nodes). A ϕ-spanning triple of (T,

t 0 ) is a triple (T, t 0 , U ϕ ) such that U ϕ = {U 0 , U 1 , . . . , U r } where U 0 = {t 0 } and for every i ∈ [r], U i is a subset of D i (T ) such that • if Q i = ∀, then for each node v ∈ U i-1 , we add in U i all nodes u ∈ children T (v) and • if Q i = ∃, then for each node v ∈ U i-1 , we add in U i one node u ∈ children T (v).
A ϕ-spanning subtree of T is a rooted subtree (T , t 0 ) of (T, t 0 ) where T = T [ r i=0 U i ] for a ϕspanning triple (T, t 0 , {U 0 , U 1 , . . . , U r }) of (T, t 0 ). See Figure 3. Note that, given a rooted tree (T, t 0 ) of height zero and a quantifier-free formula ψ, (T, t 0 ) is the unique ψ-spanning subtree of T .

t 0 T Figure 3: A rooted tree (T, t 0 ) and a ϕ-spanning subtree T of T (depicted in red), for a sentence ϕ = ∀x 1 ∃x 2 ∀x 3 ψ(x 1 , x 2 , x 3 ).
Signatures of structures. Let τ be the vocabulary of graphs of h colors and roots (i.e., constants). We use Ψ r,h, FOL[τ +dp] to denote the set of all quantifier-free FOL[τ +dp]-formulas with r free variables. We treat equivalent formulas as equal (and choose one representative for each equivalence class, which is possible for quantifier-free formulas). Then the size of Ψ r,h, FOL[τ +dp] is upper-bounded by some constant depending only on r, h, and . Let G be a τ -structure, let R ⊆ V (G), and let r ∈ N. The atomic type of a tuple (v 1 , . . . , v r ) ∈ (R ∪ {␣}) r is the set of all atomic formulas that are true for

(v 1 , . . . , v r ) in G. Given (v 1 , . . . , v r ) ∈ (R ∪ {␣}) r , we define sig 0 (G, R, v 1 , . . . , v r ) to be the atomic type of (v 1 , . . . , v r ). Also, for each i ∈ [r -1] and every v 1 , . . . , v r-i ∈ V (R ∪ {␣}, we define sig i (G, R, v 1 , . . . , v r-i ) = sig i-1 (G, R, v 1 , . . . , v r-i , u) | u ∈ R ∪ {␣} Finally, we define sig r (G, R) = sig r-1 (G, R, v) | v ∈ R ∪ {␣} .
In the case where R = V (G), we omit R from the notation, i.e., we write

sig i (G, v 1 , . . . , v r-i ) and sig r (G) instead of sig i (G, R, v 1 , . . . , v r-i ) and sig r (G). Also, we set B r,h, sig := {sig r (G) | G ∈ STR[τ ]}.
Observation 1. Let τ be the vocabulary of graphs of h colors and roots and let r ∈ N. For every

β ∈ B r,h, sig , there is a ϕ β ∈ FOL[τ + dp] such that for every τ -structure G, sig r (G) = β if and only if G |= ϕ β .
Assigning graphs to rooted trees. Let r ∈ N. Given a graph G, we construct a rooted tree (T, t 0 ) (starting from a single root t 0 ) and a function λ : V (T ) \ {t 0 } → V (G) as follows. First, for every α ∈ sig r (G), we consider a vertex v α ∈ V (G) such that sig r-1 (G, v) = α. We add |sig r (G)| children to t 0 , while we define λ t 0 to be a bijection from children

T (t 0 ) to {v α | α ∈ sig r (G)}. Then, for every t ∈ V (T ), if t 0 , t 1 , . . . , t d = t is a path of T and (u 1 , . . . , u d ) = λ t 0 (t 1 ), . . . , λ t d-1 (t d )), then we add |sig r-d (G, u 1 , . . . , u d )|-many children to t. Also, for every α ∈ sig r-d (G, u 1 , . . . , u d ), we consider a vertex v α ∈ V (G) such that sig r-d-1 (G, u 1 , . . . , u d , v) = α and we define λ t to be a bijection from children T (t) to {v α | α ∈ sig r-d (G, u 1 , . . . , u d )}. We also define the function λ : V (T ) \ {t 0 } → V (G) such that for every t ∈ V (T ) \ {t 0 } λ(t) = λ t (t)
, where t is the parent of t. We call λ an assignment of G to (T, t 0 ).

We conclude this subsection by formulating model-checking of sentences in FOL[τ + dp] in terms of assignments and ϕ-spanning trees.

Observation 2. Let r ∈ N. Let τ be a colored rooted graph vocabulary. For every τ -structure G and every sentence ϕ

= Q 1 x 1 . . . Q r x r ψ(x 1 , . . . , x r ) where ψ(x 1 , . . . , x r ) ∈ FOL[τ + dp],
we have that G |= ϕ if and only if there is -an assignement λ of G to rooted tree (T, t 0 ) of height r and -a ϕ-spanning subtree (T , t 0 ) of (T, t 0 ) such that for every (t 0 , t 1 , . . . , t r ) ∈ Paths(T ), it holds that (G, λ(t 1 ), . . . , λ(t r )) |= ψ(x 1 , . . . , x r ), where x 1 , . . . , x r are interpreted as λ(t 1 ), . . . , λ(t r ).

We say that a ϕ-spanning tree (T , t 0 ) as above certifies that G |= ϕ.

Patterns of boundaried colored graphs

In this subsection, we define the notion of a pattern of a colored rooted graph. The pattern aims to encode all information of this colored graph that concern the boundary vertices: 1) if some elements of the "boundary" tuple are the same, 2) which boundary vertices are root-vertices, 3) what are the colors of boundary vertices, 4) what is the graph induced by the boundary vertices, and 5) which sets of pairs of boundary vertices can be connected with internally vertex-disjoint paths of lenght at least two. In other words, the pattern is defined in a way that, having it in hand, we can check which quantifier-free formulas of FOL[(τ + dp) ∪ c] are satisfied from (G, a) if we interpret their free variables as the boundary vertices.

Apex-tuples of structures. Let τ be a vocabulary, let A be a τ -structure, and let l ∈ N. A tuple a = (a 1 , . . . , a l ) where each a i is either an element of V (A) or ␣, is called a apex-tuple of A of size l. We use V (a) for the set containing the non-␣ elements in a. Also, if S ⊆ V (A), we define a ∩ S = (a 1 , . . . , a l ) so that if a i ∈ S, then a i = a i , and otherwise a i = ␣. We also define a \ S = a ∩ (V (A) \ S). For every apex-tuple a, we always assume that all non-␣ elements in a are distinct.

Intuitively, an apex-tuple of a graph is a tuple consisting of vertices and empty entries and every choice of vertices (and empty entries) can be seen as an apex-tuple of appropriate size. All definitions and results in this subsection are stated for general apex-tuples, although in our proofs, we will consider apex-tuples of a particular type, i.e., arbitrary orderings of the apex sets A given by the algorithmic version of the Flat Wall Theorem (Proposition 9) presented in Appendix B.

Boundaried colored graphs. Let t, h, l ∈ N. A t-boundaried (h, l)-colored graph is a tuple G = (G, X 1 , . . . , X h , a, v 1 , . . . , v t ) where (G, X 1 , . . . , X h ) is a colored graph, a is an apex-tuple of G of size l, and v 1 , . . . , v t ∈ V (G) ∪ {␣}. Intuitively, we use ␣ to encode the absence of a vertex of G of a certain index. The vertices v i , i ∈ [t] that belong to V (G) are called boundary vertices. v 5 v 4 v 2 v 1 a 1 a 3 Figure 4: An example of a 5-boundaried (3, 3)-colored graph (G, X 1 , X 2 , X 3 , a 1 , ␣, a 3 , v 1 , v 2 , ␣, v 4 , v 5 ),
where X 1 is the set of vertices depicted in red, X 2 is the set of vertices depicted in blue, and X 3 is the set of vertices depicted in green.

Given two t-boundaried (h, l)-colored graphs

G 1 = (G 1 , X 1 , . . . , X h , a, v 1 , . . . , v t ) and G 2 = (G 2 , X 1 , . . . , X h , a , u 1 , . . . , u t ), we say that G 1 and G 2 are isomorphic if G 1 is isomorphic to G 2 via a bijection η : V (G 1 ) ∪ {␣} → V (G 2 ) ∪ {␣} such that η(␣) = ␣, for every i ∈ [t], η(v i ) = u i , for every i ∈ [l], η(a i ) = η(a i )
, and for every i ∈ [h], η(X i ) = X i . We denote by B (t,h,l) the set of all (pairwise non-isomorphic) t-boundaried (h, l)-colored graphs and we set B (h,l) = t∈N B (t,h,l) .

Patterns. Let (G, X 1 , . . . , X h , a, v 1 , . . . , v r ) ∈ B (r,h,l) . Given a set I ⊆ [r], we denote

Ind G (I) = (I, {{a, b} ∈ I × I | {v a , v b } ∈ E(G)}). We set I = {i ∈ [r] | v i = ␣}.
We define the pattern of (G, X 1 , . . . , X h , a, v 1 , . . . , v r ), denoted by pattern(G, X 1 , . . . , X h , a, v 1 , . . . , v r ), to be the quintuple (V, κ, δ, H e , H P ), where • V is the partition of I into sets such that for every A ∈ I and every i, j

∈ A, v i = v j , • κ : I → [l] is the partial function mapping each i ∈ I to the integer j ∈ [l] such that v i = a j , • δ : I → [h] is the partial function mapping each i ∈ I to the integer j ∈ [h] such that v i ∈ X j ,
• H e = Ind G (I), and

• H P = E⊆I×I (I, E)
G contains vertex-disjoint paths of length at least two between the vertices v i , v j for all {i, j} ∈ E .

Intuitively, the pattern of (G, X 1 , . . . , X h , v 1 , . . . , v r ) encodes a partition V of the set I formed by grouping indices that correspond to the same vertices, a partial function κ mapping each index in I to the index of the apex vertex to which the vertex indexed i corresponds, and a partial function δ mapping every index in I to the index of the color class among X 1 , . . . , X h in which the corresponding vertex belongs. Also, it encodes some graphs with I as vertex set. These are [START_REF] Adler | Computing excluded minors[END_REF] the graph H e that corresponds to the graph induced by the vertices v i , i ∈ I and (2) the collection H P that has all graphs with vertex set I whose edge set corresponds to the existence of internally vertex-disjoint paths between the respective vertices. We set

G (r,h,l) pat = {pattern(G, X 1 , . . . , X h , a, v 1 , . . . , v r ) | (G, X 1 , . . . , X h , a, v 1 , . . . , v r ) ∈ B (r,h,l) }.
Also, by the definition of a pattern, we observe the following.

Observation 3. There is a function

f 1 : N 3 → N such that, for every r ∈ N, |G (r,h,l) pat | ≤ f 1 (r, h, l).

Expressing satisfiability of sentences using patterns

As mentioned in the previous subsection, patterns of boundaried colored graphs can be seen as encodings of the set of quantifier-free formulas of FOL[(τ +dp)∪c] that the given boundaried colored graph satisfies. Following this line, in this subsection, we also encode quantifier-free formulas of FOL[(τ +dp)∪c] in the setting of patterns. This will allow us to formulate model-checking questions in terms of pattern realization (see Observation 5 and Observation 6). Under this viewpoint, modelchecking can be formulated in purely graph-theoretical terms (through the information encoded in patterns) of boundaried colored graphs, whose boundary is rescursively obtained, following the assignment of the given graph to a rooted tree.

We start with some additional definitions on formulas.

Atomic formulas and literals. Let τ = {E, Y 1 , . . . , Y h } be a colored-graph vocabulary and let a collection c = {c 1 , . . . , c l } of constant symbols. An atomic formula is a formula of the form

x i = x j , or x i = c j , or x i ∈ Y j , or E(x i , x j ) or dp k (s 1 , t 1 , . . . , s k , t k ) for some k ∈ [r(r + 1)/2]
, where x i , x j , s 1 , . . . , s k , t 1 , . . . , t k are first-order variables. A literal is an atomic formula or the negation of an atomic formula.

Disjunctive normal form and full clauses. Let ψ(x 1 , . . . , x r ) be a quantifier-free FOL[(τ + dp) ∪ c]-formula. We say that ψ(x 1 , . . . ,

x r ) is in disjunctive normal form if there is some k ∈ N such that ψ = c 1 ∨ • • • ∨ c k , where for each i ∈ [k]
, c i is a conjunction of literals. We call each c i a clause of ψ. We say ψ is in full disjunctive normal form if every ψ is in disjunctive normal form and, additionally, for every clause c of ψ it holds that

• for every distinct i, j ∈ [r], either x i = x j or its negation are literals of c,

• for every i ∈ [r] and every j ∈ [l], either x i = c j or its negation are literals of c,

• for every i ∈ [r] and every j ∈ [h], either x i ∈ Y j or its negation are literals of c,

• for every distinct i, j ∈ [r], either E(x i , x j ) or its negation are literals of c, and

• for every ∈ [r(r + 1)/2] and every i 1 , i 2 , . . . , i , j 1 , j 2 , . . . , j ∈ [r], either the atomic formula dp(x i 1 , x j 1 , . . . , x i , x j ) or its negation are literals of c.

We say that a quantifier-free FOL[(τ + dp) ∪ c]-formula ψ extends ψ if every clause of ψ is a subformula of a clause of ψ . We now prove that, for every quantifier-free FOL[(τ + dp) ∪ c]-formula ψ, we can construct an equivalent quantifier-free formula ψ of the same vocabulary that is in full disjunctive normal form and extends ψ.

Lemma 1. For every quantifier-free FOL[(τ + dp) ∪ c]-formula ψ, there is a quantifier-free FOL[(τ + dp) ∪ c]-formula ψ that is in full disjunctive normal form, extends ψ, and is equivalent to ψ.

Proof. Given a quantifier-free FOL[(τ + dp) ∪ c]-formula ψ(x 1 , . . . , x r ), we construct the formula ψ as follows. For every clause c of ψ, if there are i, j ∈ [r] such that neither x i = x j nor x i = x j appear in c, then we replace c by c ∧

x i = x j ∨ c ∧ x i = x j .
By recursively applying this procedure for x i = c j for every i ∈ [r] and every j ∈ [l], for x i ∈ Y j for every i ∈ [r] and every j ∈ [h], for E(x i , x j ) for every distinct i, j ∈ [r], and for dp , for every ∈ [r(r + 1)/2] and every i 1 , i 2 , . . . , i , j 1 , j 2 , . . . , j ∈ [r], we obtain ψ .

In the rest of this paper we assume that every quantifier-free formula

ψ(x 1 , . . . , x r ) in FOL[(τ + dp) ∪ c] is in disjunctive normal form.
Patterns of quantifier-free formulas. We now define a notion of pattern of quantifier-free formulas. Let ψ(x 1 , . . . , x r ) be a quantifier-free FOL[(τ + dp) ∪ c]-formula in full disjunctive normal form. We assume that ψ is satisfiable, i.e., Mod(ψ) = ∅. For every clause c of ψ, we define the pattern of c, denoted by H c , as the quintuple (V c , κ c , δ c , H e c , H P c ), where

• V c is a partition of [r] into sets such that for every A ∈ V H and every i, j ∈ A either x i = x j appears as a literal of c or i = j,

• κ c = {(i, j) ∈ [r] × [l]
| the atomic formula x i = c j appears as a literal of c},

• δ c = {(i, j) ∈ [r] × [h] | the atomic formula x i ∈ Y j appears as a literal of c}, • H e c = ([r], {{i, j} ∈ [r] × [r]
| the atomic formula E(x i , x j ) appears as a literal of c}), and

• H P c = E⊆[r]×[r] ([r], E) if E = {(i 1 , j 1 ), .
. . , (i , j )} then the atomic formula dp(x i 1 , x j 1 , . . . , x i , x j ) appears as a literal of c .

Notice that the fact that V H is a partition of [r] follows from the fact that ψ is satisfiable. Intuitively, satisfiability of ψ is asked so as to rule out the cases where, for example, all three atomic formulas x 1 = x 2 , x 2 = x 3 , and ¬(x 2 = x 3 ) appear as literals in the same clause. Also, satisfiability of ψ and the fact that it is in full disjunctive normal form implies that for every {i, j} ∈ I × I \ E(H e c ), ¬E(x i , x j ) appears as a literal in c. If ψ is not satisfiable, then we set H c to be ∅.

Let ψ be a quantifier-free FOL[(τ + dp) ∪ c]-formula. We define

ext(ψ) = {c | c is a clause of a formula ψ in full disjunctive normal form that extends ψ}.
Following Lemma 1, we get the following observation.

Observation 4. For every quantifier-free FOL[(τ + dp) ∪ c]-formula ψ, the set ext(ψ) is non-empty.

We set H ψ to be the collection of patterns of all c ∈ ext(ψ), i.e., Observation 5. Let r ∈ N and let ψ(x 1 , . . . , x r ) be a quantifier-free FOL[(τ +dp)∪c]-formula. Then (G, v 1 , . . . , v r ) |= ψ(x 1 , . . . , x r ) if and only if (G, v 1 , . . . , v r ) realizes an element of H ψ .

H ψ = {H c | c ∈ ext(ψ)},
To conclude this subsection, we explain how to revisit the approach presented in Subsection 4.1, and, in particular, how to restate Observation 2 using patterns.

Pattern-coloring. Let r, h, l ∈ N. Let G be an h-colored l-rooted graph and let λ be an assignment of G to a rooted tree (T, t 0 ) of height r. We define the function pc λ :

L(T ) → G (r,h,l) pat such that for every t ∈ L(T ), if (t 0 , t 1 , . . . , t r = t) ∈ Paths(T ), then pc λ (t) = pattern(G, λ(t 1 ), . . . , λ(t)).
We call pc λ the pattern-coloring of L(T ) with respect to λ.

Using the definition of the pattern-coloring and Observation 5, we can now restate Observation 2 as follows.

Observation 6. Let r, l ∈ N. Let τ be a colored rooted graph vocabulary. For every τ -structure G and every sentence ϕ = Q 1 x 1 . . . Q r x r ψ(x 1 , . . . , x r ) where ψ(x 1 , . . . , x r ) ∈ FOL[τ + dp], we have that G |= ϕ if and only if there is -an assignment λ of G to a rooted tree (T, t 0 ) of height r and -a ϕ-spanning subtree (T , t 0 ) of (T, t 0 ) such that for every t ∈ L(T ), pc λ (t) ∈ H ψ .

Graphs with the same patterns satisfy the same sentences

In this subsection, we aim to prove that if two colored graphs give the same signatures, then these two colored graphs satisfy the same (annotated) sentences.

Lemma 2. Let τ be a colored rooted graph vocabulary and let G, G be two τ -structures. For every r ∈ N, if sig r (G) = sig r (G ), then for every sentence ϕ ∈ FOL[τ + dp] of quantifier rank at most r, it holds that

G |= ϕ ⇐⇒ G |= ϕ. Proof. Let ϕ = Q 1 x 1 . . . Q r x r ψ(x 1 , . . . , x r ), where ψ(x 1 , . . . , x r ) is a quantifier-free formula in FOL[τ + dp].
Let λ be an assignment of G to some rooted tree (T, t 0 ) of height r and let λ be an assignment of G to some rooted tree ( T , t0 ) of height r. Due to Observation 6, to prove that

G |= ϕ ⇐⇒ G |= ϕ, it suffices to show that there is a ϕ-spanning subtree (T , t 0 ) of (T, t 0 ) certifying that G |= ϕ ⇐⇒ (1)
there is a ϕ-spanning subtree ( T , t0 ) of ( T , t0 ) certifying that G |= ϕ.

For every i ∈ [0, r], we denote by ϕ i (x 1 , . . . , x i ) the formula Q i+1 x i+1 . . . Q r x r ψ(x 1 , . . . , x r ). We first prove an analogue of (1) for the quantifier-free formula ψ(x 1 , . . . , x r ). Recall that since ψ(x 1 , . . . , x r ) is quantifier-free, given a t ∈ L(T ), T t has a unique ψ(x 1 , . . . , x r )-spanning subtree, that is T t itself. Nevertheless, we formulate the next statement in terms of ψ(x 1 , . . . , x r )-spanning subtrees in order to use it as the base case of a recursive argument built in the course of the proof of (1). Claim 1. For every (t 0 , t 1 , . . . , t r ) ∈ Paths(T ) and every ( t0 , t1 , . . . , tr ) ∈ Paths( T ), such that for every i ∈ [r], sig r-i (G, λ(t 1 ), . . . , λ(t i )) = sig r-i (G , λ ( t1 ), . . . , λ ( ti )), it holds that there is a ψ(x 1 , . . . , x r )-spanning subtree T tr of T tr certifying that

(G, λ(t 1 ), . . . , λ(t r )) |= ψ(x 1 , . . . , x r ) ⇐⇒ there is a ϕ r (x 1 , . . . , x r )-spanning subtree T tr of Tt r certifying that G , λ ( t1 ), . . . , λ ( tr ) |= ψ(x 1 , . . . , x r ).
Proof of Claim 1: Since ψ(x 1 , . . . , x r ) is a quantifier-free formula, T tr has a unique ψ(x 1 , . . . , x r )spanning subtree, that is T tr , and the same holds for Tt r . By assumption, sig 0 (G, λ(t 1 ), . . . , λ(t r )) = sig 0 (G , λ ( t1 ), . . . , λ ( tr )). Therefore, pc λ (t r ) = pc λ ( tr ), which in turn implies that pc λ (t r ) ∈ H ψ ⇐⇒ pc λ ( tr ) ∈ H ψ .

We now prove the following. The case where i = 0 proves (1). Claim 2. For every i ∈ [0, r -1], for every (t 0 , t 1 , . . . , t i ) ∈ Paths(T ) and every ( t0 , t1 , . . . , ti ) ∈ Paths( T ), such that for every j ∈ [i], sig r-j (G, λ(t 1 ), . . . , λ(t j )) = sig r-j (G , λ ( t1 ), . . . , λ ( tj )), it holds that there is a ϕ i (x 1 , . . . , x i )-spanning subtree T t i of T t i certifying that

(G, λ(t 1 ), . . . , λ(t i )) |= ϕ i (x 1 , . . . , x i ) ⇐⇒ there is a ϕ i (x 1 , . . . , x i )-spanning subtree T ti of Tt i certifying that G , λ ( t1 ), . . . , λ ( ti ) |= ϕ i (x 1 , . . . , x i ).
Proof of Claim 2: In Claim 1, we already proved the statement for i = r. Let i ∈ [0, r -1]. We assume that the statement holds for i + 1. We will prove that it holds for i. We distinguish two cases, depending on whether

Q i+1 = ∃ or Q i+1 = ∀. Case 1 : Q i+1 = ∃. (⇐) Suppose that there is a ϕ i (x 1 , . . . , x i )-spanning subtree T ti of Tt i certifying that G , λ ( t1 ), . . . , λ ( ti ) |= ϕ i (x 1 , . . . , x i ) (in the case where i = 0, we suppose that T ti = T certifies that G |= ϕ). Since Q i+1 = ∃, there exists a node z ∈ children T ( ti ) that belongs to V ( T ti ). Also, observe that T z is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree of Tz certifying that G , λ ( t1 ), . . . , λ ( ti ), λ (z) |= ϕ i+1 (x 1 , . . . , x i+1 ).
Notice that, since sig r-i (G, λ(t 1 ), . . . , λ(t i )) = sig r-i (G , λ ( t1 ), . . . , λ ( ti )), there exists a t i+1 ∈ children T (t i ) such that sig r-i-1 (G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 )) = sig r-i-1 (G , λ ( t1 ), . . . , λ ( ti ), λ (z)).

Following our recursive assumption, there is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree T t i+1 of T t i+1 certifying that G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 ) |= ϕ i+1 (x 1 , . . . , x i+1 ).

Then, the graph

T t i := T [{t i } ∪ V (T t i+1 )] is a ϕ i (x 1 , . . . , x i )-spanning subtree of T t i certifying that G, λ(t 1 ), . . . , λ(t i ) |= ϕ i (x 1 , . . . , x i ).
In the case where i = 0, we have that

T t i = T certifies that G |= ϕ. (⇒) Suppose that there is a ϕ i (x 1 , . . . , x i )-spanning subtree T t i of T t i certifying that G, λ(t 1 ), . . . , λ(t i ) |= ϕ i (x 1 , . . . , x i )
(in the case where i = 0, we suppose that

T t i = T certifies that G |= ϕ). Since Q i+1 = ∃, there exists a node t i+1 ∈ children T (t i ) that belongs to V (T t i ). Also, observe that T t i+1 is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree of T t i+1 certifying that G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 ) |= ϕ i+1 (x 1 , . . . , x i+1 ).
Since sig r-i (G, λ(t 1 ), . . . , λ(t i )) = sig r-i (G , λ ( t1 ), . . . , λ ( ti )), there is a node ti+1 in children T ( ti ) such that sig r-i-1 (G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 )) = sig r-i-1 (G , λ ( t1 ), . . . , λ ( ti ), λ ( ti+1 )).

Following our recursive assumption, there is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree T ti+1 of Tt i+1 certifying that G , λ ( t1 ), . . . , λ ( ti ), λ ( ti+1 ) |= ϕ i+1 (x 1 , . . . , x i+1 ).

Now, observe that the graph

T ti = T [{ ti } ∪ V ( T ti+1
)] is a ϕ i (x 1 , . . . , x i )-spanning subtree of Tt i certifying that G , λ ( t1 ), . . . , λ ( ti ) |= ϕ i (x 1 , . . . , x i ).

In the case where i = 0, we have that

T ti = T certifies that G |= ϕ.
Case 2 : Q i+1 = ∀.

(⇐) Suppose that there is a ϕ i (x 1 , . . . ,

x i )-spanning subtree T ti of Tt i certifying that G , λ ( t1 ), . . . , λ ( ti ) |= ϕ i (x 1 , . . . , x i )
(in the case where i = 0, we suppose that

T ti = T certifies that G |= ϕ). Since Q i+1 = ∀, every z ∈ children T ( ti ) belongs to V ( T ti ). Now observe that, for every z ∈ children T ( ti ), T z is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree of Tz certifying that G , λ ( t1 ), . . . , λ ( ti ), λ (z) |= ϕ i+1 (x 1 , . . . , x i+1 ).
Also, since sig r-d (G, λ(t 1 ), . . . , λ(t i )) = sig r-d (G , λ ( t1 ), . . . , λ ( ti )), for every z ∈ children T ( ti ) the set

{t i+1 ∈ children T (t i ) | sig r-i-1 (G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 )) = sig r-i-1 (G , λ ( t1 ), . . . , λ ( ti ), λ (z))}
is non-empty and, also, z∈children T ( ti ) {t i+1 ∈ children T (t i ) | sig r-i-1 (G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 )) = sig r-i-1 (G , λ ( t1 ), . . . , λ ( ti ), λ (z))} = children T (t i ). Following our recursive assumption, for every t i+1 ∈ children T (t i ), there is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree T t i+1 of T t i+1 certifying that G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 ) |= ϕ i+1 (x 1 , . . . , x i+1 ).

Then, the graph

T [{t i } ∪ t i+1 ∈children T (t i ) V (T t i+1 )] is a ϕ i (x 1 , . . . , x i )-spanning subtree of T t i certifying that G, λ(t 1 ), . . . , λ(t i ) |= ϕ i (x 1 , . . . , x i )
In the case where i = 0, we have that

T t i = T certifies that G |= ϕ.
(⇒) Suppose that there is a ϕ i (x 1 , . . . , x i )-spanning subtree T t i of T t i certifying that G, λ(t 1 ), . . . , λ(t i ) |= ϕ i (x 1 , . . . , x i ) (in the case where i = 0, we suppose that

T t i = T certifies that G |= ϕ). Since Q i+1 = ∀, every t i+1 ∈ children T (t i ) belongs to V (T t i ). Now observe that, for every t i+1 ∈ children T (t i ), T t i+1 is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree of T t i+1 certifying that G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 ) |= ϕ i+1 (x 1 , . . . , x i+1 ).
Since sig r-d (G, λ(t 1 ), . . . , λ(t i )) = sig r-d (G , λ ( t1 ), . . . , λ ( ti )), for every t i+1 ∈ children T (t i ) there exists a node z ∈ children T ( ti ) such that sig r-i-1 (G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 )) = sig r-i-1 (G , λ ( t1 ), . . . , λ ( ti ), λ (z)).

Following our recursive assumption, for every z ∈ children T (t i ) there is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree T ti+1 of Tt i+1 certifying that G, λ(t 1 ), . . . , λ(t i ), λ(t i+1 ) |= ϕ i+1 (x 1 , . . . , x i+1 ). Also, note that for every ti+1 ∈ children T ( ti ), there exists a node

t i+1 ∈ children T (t i ) such that sig r-i-1 (G, λ(t 1 ), . . . , λ(t i ), λ(z)) = sig r-i-1 (G , λ ( t1 ), . . . , λ ( ti ), λ ( ti+1 )).
Restating what we mentioned above for the existence of a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree of T t i+1 for each t i+1 ∈ children T (t i ), we get that for every z ∈ children T ( ti ), there is a ϕ i+1 (x 1 , . . . , x i+1 )-spanning subtree T z of Tz certifying that

G, λ ( t1 ), . . . , λ ( ti ), λ (z) |= ϕ i+1 (x 1 , . . . , x i+1 ).
Now, observe that the graph

T [{ ti } ∪ z∈children T ( ti ) V ( T z )] is a ϕ i (x 1 , . . . , x i )-spanning subtree of Tt i certifying that G , λ ( t1 ), . . . , λ ( ti ) |= ϕ i (x 1 , . . . , x i ).
In the case where i = 0, we have that T ti = T certifies that G |= ϕ. This concludes the proof of the Claim.

Following Claim 2 for i = 0, we deduce (1), which completes the proof of the lemma.

A comment on the use of Lemma 2. Before concluding this section, we wish to stress the following. Suppose that we are given an (annotated) colored graph and one can find an (annotated) colored graph that has the same "meta-collection" of patterns (in the sense of equivalence of leaflabeled trees, as in the statement of Lemma 2). Lemma 2 indicates that model-checking for the original annotated colored graph can be reduced to model-checking for the second annotated colored graph and this is safe for every formula in FOL[τ + dp]. Therefore, if we were able to find a way to compute such an "equivalent" graph and if its size (or, the size of its annotated set) was smaller than the original one's, we could reduce the problem of model-checking to smaller instances and therefore report some progress. However, this is not straightforward and in the next three sections, i.e., Section 5, Section 6, and Section 7, we explain how to deal with this situation. From a highlevel point of view, our approach considers expressing partial patterns (and consequently, partial satisfaction of formulas in FOL[τ + dp]) inside a bounded treewidth part of the given graph. Then, using Courcelle's Theorem, we will be able to compute representatives of the vertices inside this bounded treewidth part with respect to equivalence of (partial) patterns. Using the fact that we know which vertices in this part "represent" the variety of patterns, we find some "irrelevant" vertices to discard from the annotation, without changing the signature.

Routing linkages through railed annuli

In Section 4, we presented how to encode questions expressed in FOL[τ +dp] in purely graphtheoretical terms, using patterns. Recall that a pattern of a boundaried colored graph encodes, by the collection H P , what disjoint paths can be routed through the boundary vertices. This is the only "non-local" information encoded in the pattern, as all other information can be determined by inspecting only the boundaried vertices and the adjacencies between them. Aiming to define a notion of "partial" pattern, we have to deal with the possible ways that boundary vertices can be connected through disjoint paths and this can be seen as a question about the variety of linkages that can be routed through the boundaried vertices. A crucial tool for handling linkages is the Linkage Combing Lemma (Proposition 2) proved in [START_REF] Golovach | Combing a linkage in an annulus[END_REF] (see also [START_REF] Golovach | Hitting topological minor models in planar graphs is fixed parameter tractable[END_REF]). This result is applied in the presence of a partially annulus-embedded graph and an annulus-embedded railed annulus, notions that are defined in Subsection 5.1. The definition of linkages and the Linkage Combing Lemma of [START_REF] Golovach | Combing a linkage in an annulus[END_REF] are presented in Subsection 5.2. Finally, in Subsection 5.3, we define linkages of boundaried graphs and we describe how to "encode" models of boundaried graphs using patterns.

Graphs partially embedded on an annulus and railed annuli

We say that a pair

(L, R) ∈ 2 V (G) × 2 V (G) is a separation of G if L ∪ R = V (G)
and there is no edge in G between a vertex in L \ R and a vertex in R \ L. We say that two separations

(X 1 , Y 1 ) and (X 2 , Y 2 ) of a graph G are laminar if Y 1 ⊆ Y 2 and X 2 ⊆ X 1 .

Disks and annuli

. A cycle is a set homeomorphic to the set {(x, y) ∈ R 2 | x 2 +y 2 = 1}. We define a closed disk (resp. open disk ) to be a set homeomorphic to the set {(x, y) ∈ R 2 | x 2 + y 2 ≤ 1} (resp. {(x, y) ∈ R 2 | x 2 + y 2 < 1}) and a closed annulus (resp. open annulus) to be a set homeomorphic to the set {(x, y) ∈ R 2 | 1 ≤ x 2 + y 2 ≤ 2} (resp. {(x, y) ∈ R 2 | 1 < x 2 + y 2 < 2}).
Given a closed disk or a closed annulus X, we use bd(X) to denote the boundary of X (i.e., the set of points of X for which every neighborhood around them contains some point not in X). Notice that if X is a closed disk then bd(X) is a cycle, while if X is a closed annulus then bd(X) = C 1 ∪ C 2 where C 1 , C 2 are the two unique connected components of bd(X) and C 1 , C 2 are two disjoint cycles. We call C 1 and C 2 boundaries of X. We call C 1 the left boundary of X and C 2 the right boundary of X. Also given a closed disk (resp. closed annulus) X, we use int(X) to denote the open disk (resp. open annulus) X \ bd(X). When we embed a graph G in the plane, in a closed disk, or in a closed annulus, we treat G as a set of points. This permits us to make set operations between graphs and sets of points.

Partially annulus-embedded graphs. Let ∆ be a closed annulus. We say that a graph G is partially ∆-embedded, if there is some subgraph K of G that is embedded in ∆ such that bd(∆) is the disjoint union of two cycles of K and there are two laminar separations

(X 1 , Y 1 ) and (X 2 , Y 2 ) of G such that X 1 ∩ Y 2 = V (G) ∩ ∆.
We also call the graph K compass of the partially ∆-embedded graph G and we always assume that we accompany a partially ∆-embedded graph G together with an embedding of its compass in ∆ that is the set G∩∆. See Figure 5 for an illustration of a partially annulus-embedded graph.

Let ∆ be a closed annulus with left boundary B 1 and right boundary B 2 . Also, let G be a partially ∆-embedded graph. We denote by

Left ∆ (G) the connected component of G \ int(∆) that contains B 1 and by Right ∆ (G) the graph G \ ((V (G) ∩ ∆) ∪ V (Left ∆ (G))).
∆ i , that is a subset of ∆ such that ∆ 2 ⊆ • • • ⊆ ∆ r = ∆.
We call C 1 the leftmost and C r the rightmost cycle of C. From now on, each ∆-parallel sequence C of cycles will be accompanied with the sequence [∆ 2 , . . . , ∆ r ] of the corresponding closed annuli. Given i, j ∈ [2, r], where i ≤ j, we call the set ∆ i \ int(∆ j ) (i, j)-annulus of C and we denote it by ann(C, i, j). Also, for every i ∈ [2, r], we set ∆ i to be the (1, i)-annulus of C and we also denote it by ann(C, 1, i).

Railed annuli. Let G be a graph. Also, let r ∈ N ≥3 and q ∈ N ≥3 and assume that r is an odd number. An (r, q)-railed annulus of G is a pair A = (C, P) where C = [C 1 , . . . , C r ] is a sequence of cycles of G and P = [P 1 , . . . , P q ] is a collection of pairwise vertex-disjoint paths in G such that • For every j ∈ [q], the endpoints of P j are vertices of C r and C 1 and

• for every (i, j) ∈ [r] × [q], C i ∩ P j is a non-empty path, that we denote P i,j .

See Figure 6 for an example. We refer to the paths of P as the rails of A and to the cycles of C as the cycles of A. We use V (A) to denote the vertex set i∈[r] V (C i ) ∪ j∈[q] V (P j ) and E(A) to denote the edge set i∈[r] E(C i ) ∪ j∈[q] E(P j ). We can see each path P j in P as being oriented towards the "inner" part of calA, i.e., starting from a vertex of C p and finishing to a vertex of P 1,j . For every (i, j) ∈ [r] × [q], we denote by s i,j (resp. t i,j ) the first (resp. last) vertex of P i,j when traversing P j according to this orientation. If (i, i ) ∈ [r] 2 with i < i then we define A i,i to be the railed annulus ([C i , • • • , C i ], P 1 , . . . , P q ), where for every j ∈ [q], P j is the subpath of P j between s i,j and t i ,j .

Annulus-embedded railed annuli. Let ∆ be a closed annulus and let G be a partially ∆embedded graph. Also, let r ∈ N ≥3 and q ∈ N ≥3 and assume that r is an odd number. A (r, q)-railed

annulus A = (C, P) of G is called ∆-embedded if C = [C 1 , . . . , C r ] is a ∆-parallel sequence of cycles of G. We use ann(A) to denote ann(C, 1, r).
The following proposition [14, Proposition 5.1] states that large railed annuli can be found inside a slightly larger wall and will be used in the next section. For the definition of a wall see Section B.1. Proposition 1. If x, z ≥ 3 are odd integers, y ≥ 1, and W is an odd(2x + max{z, y 4 -1})-wall, then

• there is a collection P of y paths in W such that if C is the collection of the first x layers of W, then (C, P) is an (x, y)-railed annulus of W where the first cycle of C is the perimeter of W, and

• the open disk defined by the x-th cycle of C contains the vertices of the compass of the central z-subwall of W.

Combing linkages

In this subsection we define linkages and we present the Linkage Combing Lemma from [START_REF] Golovach | Combing a linkage in an annulus[END_REF] (Proposition 2) -see also [START_REF] Golovach | Hitting topological minor models in planar graphs is fixed parameter tractable[END_REF].

Linkages. A linkage in a graph G is a subgraph L of G whose connected components are nontrivial paths. The paths of a linkage are its connected components and we denote them by P(L). We call |P| the size of P(L). The terminals of a linkage L, denoted by T (L), are the endpoints of the paths of L, and the pattern of L is the set {{s, t} | P(L) contains some (s, t)-path}. Two linkages L 1 , L 2 of G are equivalent if they have the same pattern and we denote this fact by L 1 ≡ L 2 . Let ∆ be a closed annulus or a closed disk, let G be a partially ∆-embedded graph, L be a linkage of G, and D be a subset of ∆. We say that L is D-avoiding if T (L) ∩ D = ∅ (see Figure 6). Also, let ∆ be a closed annulus and A = (C, P) be a ∆-embedded (p, q)-railed annulus of a partially ∆-embedded graph G. Given some I ⊆ [q], we say that a linkage

L of G is (s, I)-confined in A if L ∩ ann(C, t + 1 -t , t + 1 + t ) ⊆ i∈I P i .
Intuitively, the above definition demands that L traverses the "middle" (s, q)-annulus by intersecting it only at the rails of A.

We now state the Linkage Combing Lemma from [START_REF] Golovach | Combing a linkage in an annulus[END_REF] (see also [START_REF] Golovach | Hitting topological minor models in planar graphs is fixed parameter tractable[END_REF]). Intuitively, it says that in the presence of a "big enough" ∆-embedded railed annulus A in a partially ∆-embedded graph G, where ∆ is a closed annulus, every linkage of G can be "combed" through the rails of A in some central buffer inside A.

Proposition 2 (Linkage Combing). There exist two functions f 2 , f 3 : N → N, where the images of f 3 are even, such that for every odd s ∈ N ≥1 and every k ∈ N, if

• ∆ is a closed annulus,
• G is a graph that is partially ∆-embedded,

• A = (C, P) is a ∆-embedded (p, q)-railed annulus of G, where p ≥ f 3 (k)+s and q ≥ 5/2•f 2 (k),

• L is a ∆-avoiding linkage of size at most k, and

• I ⊆ [q], where |I| > f 2 (k), then G contains a linkage L where L ≡ L, L \ ∆ ⊆ L \ ∆, and L is (s, I)-confined in A. Moreover, f 3 (k) = O((f 2 (k)) 2 ).

Linkages in boundaried graphs

In this subsection, we aim to define the set of models of a boundaried graph, that is all linkages that can be routed inside this graph and contain the boundary vertices as terminals. This collection of graphs, can be encoded in abstract terms of collections of binary relations between indices of the boundaried vertices, representing the existence of (disjoint) paths between the corresponding boundary vertices. This encoding is, in fact, present in the encoding of the pattern (see Observation 7).

Linkages of boundaried graphs.

A pairing is a t-boundaried graph L = (L, v 1 , . . . , v t ) where L is a linkage and T (L) ⊆ {v 1 , . . . , v t }. We use B (t) pair to denote the set of all (pairwise non-isomorphic) t-boundaried graphs that are pairings. A path of a linkage L is non-trivial if it is not a single edge. Given a k-boundaried graph (G, u 1 , . . . , u k ), a linkage L of G and some v 1 , . . . , v t ∈ T (L) ∪ {␣} such that {u 1 , . . . , u k } ⊆ {v 1 , . . . , v t }, we say that (L, v 1 , . . . , v t ) is a boundaried linkage of (G, u 1 , . . . , u k ).

Let (G, v 1 , . . . , v t ) be a t-boundaried graph. We define the set of pairings of (G, v 1 , . . . , v t ), denoted by Pairings(G, v 1 , . . . , v t ), to be the set (r,h,l) . Given an L ∈ Pairings(G, v 1 , . . . , v r ), we define the imprint of L, denoted by imp(L), to be the graph whose vertex set is I = {i ∈ [r] | v i = ␣} and two vertices i, j ∈ I are adjacent if {v i , v j } belongs to the pattern of L. We define the compression of G, denoted by compression(G) to be the quintuple (V, κ, δ, H e , H P ), where • V is the partition of I to sets of pairwise equal vertices,

Pairings(G, v 1 , . . . , v t ) =    (L, v 1 , . . . , v t ) ∈ B (t) pair (L, v 1 , . . . , v t ) is a boundaried linkage of (G, v 1 , . . . , v t ) and every path of L is non-trivial    . Imprint of linkages. Let r, h, l ∈ N. Let G = (G, X 1 , . . . , X h , a, v 1 , . . . , v r ) ∈ B
• κ is the partial function mapping each i ∈ I to j ∈ [l] such that v i = a j ,

• δ is the partial function mapping each i ∈ I to j ∈ [h] such that v i ∈ X j ,

• H e = Ind G (I), and

• H P = {imp(L) | L ∈ Pairings(G, v 1 , . . . , v r )}.
It is easy to observe the following. Observation 7. For every G ∈ B (r,h,l) , compression(G) = pattern(G).

We stress that the only difference between the collection H P of imprints of all pairings of (G, v 1 , . . . , v r ) and the set Pairings(G, v 1 , . . . , v r ) is that the first is a collection of graphs whose vertex set is the set of indices I ⊆ [r], while graphs in Pairings(G, v 1 , . . . , v r ) are subgraphs of G. The distinction between the two is essential in order to 1) encode the patterns of linkages "abstractly" (in terms of graphs on indices) and 2) decode the presence of same variety of linkages inside graphs with the same pattern.

Before concluding this section, we present some additional definitions on linkages of boundaried colored graphs and the reason is the following. In Section 7, we describe how, given a colored graph partially embedded in a "big enough" railed annulus, construct (a series of) boundaried graphs whose boundary vertices will also be some vertices of the rails of the annuli. These boundary vertices will be chosen to be the "few" vertices in which every linkage can be combed, due to Proposition 2. Therefore, as we are about to prove in Section 7 (in particular, Lemma 4), after combing, linkages can be separated on a "left" and a "right" part. Therefore, we need to define a way to glue pairings.

Gluing pairings. We now define compatibility between pairings. Let , r ∈ N. Let L = (L, u 1 , . . . , u r+ ) and L = (L , v 1 , . . . , v r+ ) be two pairings. We say that L and L are -compatible if u r+1 , . . . , u r+ ∈ T (L), v r+1 , . . . , v r+ ∈ T (L ), for every i ∈ [r], u i = ␣ if and only if v i = ␣, and for every i, j ∈ [ ], {v r+i , v r+j } is in the pattern of L if and only if {v r+i , v r+j } is not in the pattern of L . Given two families F 1 , F 2 ⊆ B (r+ ) of pairings, we say that F 1 and F 2 are -compatible if for every L 1 ∈ F 1 and every L 2 ∈ F 2 , L 1 and L 2 are -compatible.

Let L 1 = (L 1 , u 1 , . . . , u r+ ) and L 2 = (L 2 , v 1 , . . . , v r+ ) be two -compatible pairings. We denote by (L 1 , u 1 , . . . , u r+ ) ⊕ (L 2 , v 1 , . . . , v r+ ) the pairing (L, c 1 , . . . , c r ), where • L is the linkage obtained from the disjoint union of L 1 and L 2 after identifying, for every i ∈ [r + 1, ], the vertices u i and v i , and

• c i = u i , if u i ∈ T (L 1 ), while c i = v i , if v i ∈ T (L 2
) (recall that by definition of compatibility, for every i ∈ [r], at least one of u i and v i is equal to ␣ but not both).

Given two -compatible families F 1 , F 2 ⊆ B (r+ ) of pairings, we denote by

F 1 ⊕ F 2 the collection {L 1 ⊕ L 2 | L 1 ∈ F 1 and L 2 ∈ F 2 }.

Dealing with apices

In this section, we show how to deal with apex vertices that can be adjacent to vertices in a flat area of the graph in a completely arbitrary way. In Subsection 6.1, we define a certain "transformation" from a colored graph to another colored graph (with more colors), interpreting neighborhoods of some predetermined vertices as new colors. Moreover, in Subsection 6.2, we describe how to get an equivalent version of a formula in this "projected" setting (see Lemma 3). This will allow us to define an equivalent version of any given formula in FOL[τ +dp] that will transform a question from a flat graph with apices to a flat graph without apices (where adjacencies with apices are interpreted as colors in the graph).

Projections of graphs with respect to some apex-tuple

In this subsection, we define a way to "project" a given colored graph with respect to a given apextuple and a way to define the "projected" version of a sentence such that the initial colored graph satisfies the initial sentence if and only if the "projected" colored graph satisfies the "projected" sentence (see Lemma 3). This transformation will allow us to work with the projected colored graphs, where the absence of apices in a graph of big enough treewidth implies a flat bidimensional structure (see Proposition 9 in Appendix B). Flatness is particularly critical for our techniques, as it will be explained in Section 7.

We proceed to formalize the idea of "projecting" a structure with respect to an apex-tuple. First, we describe what is the vocabulary of the "projected" structure.

Constant-projections of vocabularies. Let τ be a colored-graph vocabulary, let l ∈ N, and let c = {c 1 , . . . , c l } be a collection of l constant symbols. We define the constant-projection τ c of (τ ∪ c) to be the vocabulary (τ ∪ c ∪ {C 1 , . . . , C l }), where C 1 , . . . , C l are unary relation symbols not contained in τ .

Given a colored-graph vocabulary τ and some collection of constant symbols c, we proceed to define a way to construct a τ c -structure from a given (τ ∪ c)-structure (G, a). The obtained τ c -structure is the "projection" of (G, a) with respect to the apex-tuple a.

Projecting a colored graph with respect to an apex-tuple. Let τ be a colored-graph vocabulary, let l ∈ N, and let c = {c 1 , . . . , c l } be a collection of l constant symbols. Let also τ c be the constant-projection of (τ ∪ c). Given a (τ ∪ c)-structure (G, a), where a = (a 1 , . . . , a l ) is an apex-tuple of G of size l and, for every i ∈ [l], c (G,a) i = a i , we define the structure ap c (G, a) to be the τ c -structure obtained as follows:

• V (ap c (G, a)) = V (G), • for every i ∈ [l] c ap c (G,a) i = a i , • E ap c (G,a) = E G ∩ ((V (G) \ V (a)) 2 ∪ V (a) 2 ),
• every R ∈ τ \ {E} is interpreted in ap c (G, a) as in G, and

• for every i ∈ [l], C i is interpreted in ap c (G, a) as N G (a i ) \ V (a).
Notice that if a i = ␣, C i is interpreted in ap c (G, a) as the empty set. Intuitively, we introduce a color C i , i ∈ [a] for each a i . We keep the same universe, we keep only edges that are either between apices or between non-apices, and we color the neighbors of a i by color C i . See Figure 7 for an example.

Apex-projected sentences

Having defined the structure ap c (G, a), we now define for every sentence ϕ ∈ FOL[τ +dp] its l-apexprojected sentence ϕ l . This will be a sentence in FOL[τ c + dp] (see Observation 8) and can be seen as the equivalent (to ϕ) question that is asked to be satisfied by ap c (G, a).

Let τ be a colored-graph vocabulary, let l ∈ N, and let c = {c 1 , . . . , c l } be a collection of l constant symbols. Given a set S and an ∈ N ≥1 , we use P (S) to denote all partitions of S into parts, i.e., all collections of pairwise disjoint subsets S 1 , . . . , S of S such that i∈[ ] S i = S. a 1 a 2 a 3 a 4 Figure 7: An example of a graph G with an apex-tuple a = (a 1 , . . . , a 4 ). The set C 1 contains all cyan vertices (the neighbors of a 1 ), the set C 2 contains all green vertices, the set C 3 contains all orange vertices and the set C 4 contains all red vertices. Vertices that are neighbors to more than one a i are depicted with multiple colors. The structure ap c (G, a) is obtained from G after introducing colors C i , i ∈ [START_REF] Agrawal | Elimination distance to topological-minor-free graphs is FPT[END_REF] and after removing all edges between a vertex in {a 1 , . . . , a 4 } and a vertex in V (G) \ {a 1 , . . . , a 4 }.

For every sentence ϕ ∈ FOL[τ +dp], we define its l-apex-projected sentence ϕ l to be the sentence obtained from ϕ by replacing each atomic formula E(x, y) by

E(x, y) ∨ i∈[l] (x = c i ∧ y ∈ C i ) ∨ (y = c i ∧ x ∈ C i )
and each atomic formula dp(s 1 , t 1 , . . . , s k , t k ) by the formula ζ dp (s 1 , t 1 , . . . , s k , t k ) that we proceed to define. We set distinct(x 1 , . . . , x t ) := i,j∈[t],i =j (x i = x j ). We define ζ dp (s 1 , t 1 , . . . , s k , t k ) as follows (see next paragraph for an intuitive explanation): (2)

∃ x I 1 1 , . . . , x I 1 |I 1 | , . . . , x I d 1 , . . . , x I d |I d | : distinct(x I 1 1 , . . . , x I 1 |I 1 | , . . . , x I d 1 , . . . , x I d |I d | ) (3)
∧ i,i ∈[d], i =i j∈[2,|I i |-1] (x I i j = s ρ(I i ) ∧ x I i j = t ρ(I i ) ) (4)
∧ i∈[d] all bijections λ I i :[|I i |]→I i i∈[d] j∈[|I i |]
x

I i j = c λ I i (j) (5)
∧ i∈[d] J i ⊆[|I i |-1] i∈[d] j∈[|I i |-1]\J i E(x I i j , x I i j+1 ) (6)
∧ ∃ j∈J 1 y I 1 j , . . . , ∃ j∈J d y I d j , ∃ j∈J 1 z I 1 j , . . . , ∃ j∈J d z I d j , (7)
distinct((y I 1 j ) j∈J 1 , . . . , (y

I d j ) j∈J d , s 1 , t 1 , . . . , s k , t k ) (8)
∧ distinct((z I 1 j ) j∈J 1 , . . . , (z

I d j ) j∈J d , s 1 , t 1 , . . . , s k , t k ) (9)
∧ i,i ∈[d], i =i j∈J i , j ∈J i (y I i j = z I i j ) ∧ i∈[d] j,j ∈J i , j =j (y I i j = z I i j ) (10)
∧ i∈[d] j∈J i (y I i j ∈ C λ I i (j) ∧ z I i j ∈ C λ I i (j+1) ) ∧ (11)
(X i ,Y i ,Z i )∈P 3 (J i ) ( j∈X i (y I i j = z I i j ) ∧ j∈Y i E(y I i j , z I i j ) ∧ ψ I i ,ρ,Z i ) , (12)
where ψ I i ,ρ,Z i is the formula

s ρ(I i ) = x I i 1 ∧ t ρ(I i ) = x I i |I i | ∧ dp(ξ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l )) ∨ s ρ(I i ) = x I i 1 ∧ t ρ(I i ) = x I i |I i | ∧ ∃ sρ(I i ) ∈ C λ I i (1) ∧ distinct(s ρ(I i ) , (s j , t j ) j =ρ(I i ) ) ∧ dp(κ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l )) ∨ s ρ(I i ) = x I i 1 ∧ t ρ(I i ) = x I i |I i | ∧ ∃ tρ(I i ) ∈ C λ I i (|I i |) ∧ distinct( tρ(I i ) , (s j , t j ) j =ρ(I i ) ) ∧ dp(δ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l )) ∨ s ρ(I i ) = x I i 1 ∧ t ρ(I i ) = x I i |I i | ∧ ∃ sρ(I i ) ∈ C λ I i (1) ∧ distinct(s ρ(I i ) , (s j , t j ) j =ρ(I i ) ) ∧ ∃ tρ(I i ) ∈ C λ I i (|I i |) ∧ distinct( tρ(I i ) , (s j , t j ) j =ρ(I i ) ) ∧ dp(ζ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l )) ,
and

• ξ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l
) is used to denote the tuple obtained from the tuple (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ) after removing, for every i ∈ [ ], (s ρ(I i ) , t ρ(I i ) ) and adding (y I i j , z I i j+1 ), for all j ∈ Z i .

• κ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ) is used to denote the tuple obtained from the tuple (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ) after removing, for every i ∈ [ ], (s ρ(I i ) , t ρ(I i ) ) and adding (s ρ(I i ) , sρ(I i ) ) and (y I i j , z I i j+1 ), for all j ∈ Z i .

• δ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ) is used to denote the tuple obtained from the tuple (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ) after removing, for every i ∈ [ ], (s ρ(I i ) , t ρ(I i ) ) and adding (t ρ(I i ) , tρ(I i ) ) and (y I i j , z I i j+1 ), for all j ∈ Z i .

•

ζ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l
) is used to denote the tuple obtained from the tuple (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ) after removing, for every i ∈ [ ], (s ρ(I i ) , t ρ(I i ) ) and adding (s ρ(I i ) , sρ(I i ) ), (t ρ(I i ) , tρ(I i ) ), and (y I i j , z I i j+1 ), for all j ∈ Z i .

Intuitive explanation of the above formulas. We decode step by step the intuition behind the above formulas. First, we replace E(x, y) by E(x, y)

∨ i∈[l] (x = c i ∧ y ∈ C i ) ∨ (y = c i ∧ x ∈ C i )
in order to encode that, in the colored graph obtained after the removal of all edges between apexvertices and the rest vertices of the graph, two vertices x, y are adjacent if either the edge {x, y} is present in the modified graph or one of x and y is an apex-vertex a i (interpreting c i ) and the other is colored by the corresponding color C i , that is the color that all neighbors of a i receive.

For the the atomic formula ζ dp (s 1 , t 1 , . . . , s k , t k ), the intuition is the following. We want to separate the formula into many parts, i.e., many questions for disjoint paths or adjacencies, guessing whether the variables s 1 , t 1 , . . . , s k , t k are assigned to apex-vertices and/or whether the apex-vertices are internal vertices of the disjoint paths between s 1 , t 1 , . . . , s k , t k .

For this reason, in line (2) of the above definition, and in particular in " B⊆[l] ", we start by guessing the subset B of apex-vertices that are part of the disjoint paths (either as endpoints or as internal vertices). We will refer to this set as active apices. Then, with " d∈[k] ", we guess how many among the k disjoint paths contain active apices (and we call them active paths) and then, with " (I 1 ,...,I d )∈P d (B) " we guess how B is partitioned in d sets, each set corresponding to active apices that belong to the same active path and with " all injective functions ρ:{I 1 ,...,I d }→[k] ", we guess which active apices belong to each active path.

Having made all these guesses, in line (3), we ask for variables ("∃ x I 1 1 , . . . , x I 1 |I 1 | , . . . , x I d 1 , . . . , x I d |I d | ") that will be interpreted as the active apices and we ask these variables to be interpreted as pairwise disjoint vertices ("distinct(x I 1 1 , . . . ,

x I 1 |I 1 | , . . . , x I d 1 , . . . , x I d |I d | )"
). Also, in line (4), we ask that all vertices that interpret x

I i j for i ∈ [d] and j ∈ [2, |I i |-1] are different from the endpoints of all the other active paths (" i,i ∈[d],i =i j∈[2,|I i |-1] (x I i j = s ρ(I i ) ∧ x I i j = t ρ(I i ) )"
). The two later properties are necessary for the disjointness of the demanded paths. For the moment, we do not demand the interpretations of x I i 1 and

x I i |I i | , for any i ∈ [d],
to be distinct from the endpoints of the paths. To express that these variables correspond to apices, in line ( 5), first we guess to which element of B each x I i j corresponds (" i∈[d] all bijections λ I i :[|I i |]→I i "). We stress that the order of x I i j is fixed and implicitly corresponds to the order that active apices are transversed by the corresponding active path. For each i ∈ [d], the bijection λ I i is used to correspond the ascending indices j of the variables x I i j to the actual active apices. Then, with " i∈[d] j∈[|I i |] x I i j = c λ I i (j) ", we check whether this guess indeed corresponds to an interpretation of each x I i j with the appropriate active apex a λ I i (j) .

In line [START_REF] Agrawal | An FPT Algorithm for Elimination Distance to Bounded Degree Graphs[END_REF], we partition active apices into two sets. First, we have the active apices whose next neighbor on the corresponding active path is not an apex-vertex (we orient paths according to the ordering given by the ascending ordering of the indices of x I i j ). These active apices are guessed using " ∈[d] J i ⊆[|I i |-1] ". These, we call them shifting active apices. For the remaining ones (" i∈[d] j∈[|I i |-1]\J i "), we check if indeed their next neighbor on the corresponding active path is an apex-vertex ("E(x I i j , x I i j+1 )"). Now, in line ( 7), we deal with the shifting active apices (apices that would be transversed by path that would be routed through at least one non-apex vertex before entering again the set of apex vertices). For each shifting active apex, we ask for the existence of two extra vertices, corresponding to the first vertex after this shifting active apex and the last vertex before the next apex in a supposed path. This is done in "∃ j∈J 1 y I 1 j , . . . ,

∃ j∈J d y I d j , ∃ j∈J 1 z I 1 j , . . . , ∃ j∈J d z I d j ". The variables y I i j , i ∈ [d], j ∈ J i and the variables z I i j , i ∈ [d]
, j ∈ J i should be interpreted as pairwise disjoint vertices that are also different from the endpoints of all the other (active or not) paths. We check this in lines ( 8) and ( 9) using "distinct((y I 1 j ) j∈J 1 , . . . , (y

I d j ) j∈J d , s 1 , t 1 , . . . , s k , t k )" and "distinct((z I 1 j ) j∈J 1 , . . . , (z I d j ) j∈J d , s 1 , t 1 , . . . , s k , t k )"
. Also, we demand that variables y I i j and z

I i j
are interpreted as disjoint vertices if they correspond to different paths (i.e., i = i ) or if they belong to the same path but they are not consecutive (i.e., j = j ). This is done in line [START_REF] Balabán | Twin-width is linear in the poset width[END_REF].

For every i ∈ [d], the vertices interpreting y I i j , j ∈ J i should appear in the corresponding active path directly after the corresponding shifting active apex a λ I i (j) and the vertices interpreting z I i j , j ∈ J i should appear in the corresponding active path directly before the next corresponding apex a λ I i (j+1) . Since edges between apices and non-apices are no longer present in the graph, we encode this "succession" by using the colors of the neighborhood of the apices. This is done in

" i∈[d] j∈J i (y I i j ∈ C λ I i (j) ∧ z I i j ∈ C λ I i (j+1)
)", in line [START_REF] Bartier | On girth and the parameterized complexity of token sliding and token jumping[END_REF]. At this point, we have dealt with the internal part of the paths (we have not yet discussed what happens with the endpoints; we will do so in the next paragraph) for what concerns the apices. In fact, we already explained how to guess which part of the apices will be part of the supposed disjoint paths (lines (2)-( 5)), how to guess which part of the paths is routed only through apices (line ( 6)), and where the paths "exit" and "enter" the set of apices (lines ( 7)- [START_REF] Bartier | On girth and the parameterized complexity of token sliding and token jumping[END_REF]). What remains is to describe how to formulate the question on the graph without the apices and how we deal with the endpoints of the paths.

In fact, we already mentioned that, for every i ∈ [d] and every j ∈ [d], y I i j and z I i j are interpreted as two vertices that are not apices and for the supposed path corresponding to index i, the part between the interpretations of y I i j and z I i j is a maximal path that does not contain apices. Having this in mind, in line [START_REF] Bartier | Galactic token sliding[END_REF], we guess what is the relation between y I i j and z I i j , for all j ∈ J i . We partition J i to three sets X i , Y i , and Z i (" (X i ,Y i ,Z i )∈P 3 (J i ) "). The set X i contains all indices j for the demanded path that passes through the apices a λ I i (j) and a λ I i (j+1) has to be routed through a single vertex between a λ I i (j) and a λ I i (j+1) , or, in other words, y I i j and z I i j are asked to be interpreted as the same vertex. (" j∈X i (y I i j = z I i j )"). The set Y i contains all indices j for which the demanded path that passes through the apices a λ I i (j) and a λ I i (j+1) has to be routed through an edge connecting the interpretations of y I i j and z I i j (" j∈Y i E(y I i j , z I i j )"). Finally, Z i contains all remaining j ∈ J i , i.e., all indices j for which the demanded path has to be routed through path of length two between the interpretations of y I i j and z I i j . To finish the description of the formula ζ dp (s 1 , t 1 , . . . , s k , t k ), we have to discuss how the final new demands for disjoint paths are formulated. This is encoded in the formula ψ I i ,ρ,Z i . There, for each active path, say indexed by ρ(I i ), we have to "update" the demand for a path from s ρ(I i ) to t ρ(I i ) to the demand for paths between y I i j and z I i j+1 ), for all j ∈ Z i and this update has to be done for all active paths.

In the last argument of the previous paragraph, we omitted some important detail. The aforementioned update is correct (in the sense that the two questions for disjoint paths are equivalent) only if, for all active paths, its first and last active apex are its endpoints, i.e., if s ρ(I i ) = x I i 1 and t ρ(I i ) = x I i |I i | are true. This is why the first disjunctive term of ψ

I i ,ρ,Z i is "s ρ(I i ) = x I i 1 ∧ t ρ(I i ) = x I i |I i | ∧ dp(ξ i,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ))", where ξ I i ,ρ,Z i (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l )
is the tuple obtained from (s 1 , t 1 , . . . , s k , t k , c 1 , c 1 , . . . , c l , c l ) after removing, for every i ∈ [ ], (s ρ(I i ) , t ρ(I i ) ) and adding (y I i j , z I i j+1 ), for all j ∈ Z i . Since all non-shifting active apices are adjacent (see line ( 6)) and for all j ∈ J i \ Z i , the interpretations of y I i j and z I i j+1 ) are either identical or adjacent (see line [START_REF] Bartier | Galactic token sliding[END_REF]), what remains is to find disjoint paths between the interpretations of y I i j and z I i j+1 ), for every j ∈ Z i . Of course, having dealt with the case that paths contains apices, we want the new paths that we search to be disjoint from all apices. To express this, we add "c 1 , c 1 , . . . , c l , c l " to the above tuples, asking that the rest (disjoint) paths are also disjoint from the path of zero lenght that starts and finishes to the intepretation of c i , for every i ∈ [l].

To deal with the case where, for an active paths, either its first or last active apex are not its endpoints, we have to guess the existence of an extra "entering" or "exiting" point, respectively, and ask for some supplementary disjoint path between this new guessed vertex and the corresponding endpoint (see last three disjunctive terms of ψ I i ,ρ,Z i ). This concludes the intuitive explanation of the formula Also, note that in the definition of ϕ l , we add some extra quantified first-order variables (see the definition of ζ dp (s 1 , t 1 , . . . , s k , t k ); line (3), line [START_REF] Agrawal | On the parameterized complexity of clique elimination distance[END_REF], and the definition of ψ I i ,ρ,Z i ).

ζ dp (s 1 , t 1 , . . . , s k , t k ). Note that if ϕ ∈ FOL[τ +dp] and c is a collection of l constant symbols, then ϕ l ∈ FOL[τ c + dp].
Observation 9. Let τ be a colored-graph vocabulary and let r, l ∈ N. There is a function f 4 : N 2 → N such that for every ϕ ∈ FOL[τ +dp], if ϕ has quantifier rank r, then ϕ l has quantifier rank f 4 (r, l).

The definition of the l-apex-projected sentence ϕ l implies the following lemma, which can be seen as a generalization of [START_REF] Flum | Fixed-parameter tractability, definability, and model-checking[END_REF]Lemma 26] that deals with graphs to also "interpret" the vertex-disjoint paths predicates.

Partial signatures and exchangability

As explained in the end of Subsection 4.4, after proving Lemma 2 our strategy is, given an annotated colored graph to find a way to construct another annotated colored graph that is equivalent to the original one in the sense that they have the same signature. In this section, we describe how, in the presence of a big enough flat railed annulus in the given graph, we can define a way to encode only patterns of "one side" of the annulus. In fact, in Subsection 7.1, we define stamps of vertices with respect to some given railed annulus, which will help us to group vertices in a way that encodes their relative position to the cycles of the railed annulus. Then, in Subsection 7.2, in order to facilitate reading, we establish some conventions for boundaried colored graphs in flat railed annuli. Using the notation introduced in these first two subsections, in Subsection 7.3, we show how to reformulate Proposition 2 and how linkages of the given graph (that contains a big enough railed annulus) are "combed" inside boundaried graphs whose boundary vertices are either some particular vertices of the railed annulus, or vertices of appropriate stamps (Lemma 4). Then, to capture the "pattern-behavior" of the considered series of boundaried graphs in the railed annulus, we define the notion of partial signature of a graph as a "meta-collection" of patterns of boundaried graphs (as the ones described in Subsection 7.2) for boundary vertices of particular stamps. Finally, in Subsection 7.5, we show that boundaried (annotated) colored graphs with the same partial signature can be "replaced", maintaining the same (global) signature (see Lemma 5).

Stamps of vertices with respect to annuli

In this subsection, we describe how to attribute stamps to the vertices of a given graph G with a flat railed annulus A that encode the relative position of these vertices with respect to the cycles of A. The definition of a flat railed annulus is given in Appendix B, and, in particular, in Subsection B.3. Intuitively, it is the analogue of flat walls but in terms of railed annuli.

Let r ∈ N. Let G be a graph, let (A, R) be a (p, q)-railed annulus flatness pair of G, where p = 2 r + 1. For every w ∈ {0, 1} r , we denote by C w the cycle C n w of C, where

n w = 1 + i∈[r] w i 2 r-i+1 .
Given an i ∈ [r] and a w ∈ {0, 1} i-1 , for every vertex v ∈ V (G) we define the w-stamp of v as follows: Trace of tuples of vertices with respect to annuli. Let r ∈ N. Let G be a graph, let (A, R) be a (p, q)-railed annulus flatness pair, where p = 2 r + 1. Given a tuple (v 1 , . . . , v r ) of vertices of G, we define the trace of (v 1 , . . . , v r ) with respect to (A, R), denoted by trace (A,R) (v 1 , . . . , v r ), to be the pair (w 1 . . . w r , ω 1 . . . ω r ) where (w 1 , ω 1 ) = stamp ε (v 1 ) and for every i ∈ [2, r], we set (w i , ω i ) = stamp w 1 ...w i-1 (v i ).

stamp w(v) =            (0, •), if v ∈ V (Influence R (C w00 r-i )), (0, •), if v ∈ V (Influence R (C w11 r-i )) \ V (Influence R (C w10 r-i )), (1, •), if v ∈ V (Influence R (C w10 r-i )) \ V (Influence R (C w00 r-i )), and (1, •), if v / ∈ V (Influence R (C w11 r-i )). C w00 r-i C w10 r-i C w11 r-i A w0 A w1

Some conventions for boundaried graphs in flat railed annuli

We proceed to define a series of boundaried graphs in a given railed annulus flatness pair (A, R).

In fact, we define these boundaried graphs in the leveling Leveling (A,R) (G) of (A, R), that is the "planar representation" of (A, R), as defined in Subsection B.7. In order (A, R) to has this "planar representation" property, it has to be well-aligned (see also Subsection B.7).

Let G be a graph and let (A, R) be a well-aligned (p, q)-railed annulus flatness pair of G. We consider the graph Leveling (A,R) (G) and keep in mind that Leveling (A,R) (G) contains the representation R A of A, that is a ∆-embedded (p, q)-railed annulus. Let R A = (C, P) and keep in mind that |C| = p and p is an odd integer in N ≥3 . Intuitively, the cycle C (p+1)/2 is the "middle" cycle of C. We can see each path P j in P as being oriented towards the "inner" part of R A , i.e., starting from an endpoint of P p,j and finishing to an endpoint of P 1,j . For every j ∈ [q], we define r j as the first vertex of P j that appears in P (p+1)/2,j (recall that P (p+1)/2,j is the intersection of the cycle C (p+1)/2 and the rail P j ) while traversing P j according to this orientation. Given a t ∈ [q], we define the t-boundaried graph

G (t) A = (G , r 1 . . . , r t ), where G is the graph Leveling (A,R) (G) \ V (Right ∆ (p+1)/2 (Leveling (A,R) (G))) (recall that ∆ (p+1)/2 is
the closed annulus cropped by C 1 and C (p+1)/2 ). We call r 1 , . . . , r t the boundary vertices of G (t)

A . Assume now that A is a well-aligned (2 r • (p -1) + 1, q)-railed annulus flatness pair of G. We set

C (p) = C 1 , . . . , C 2 r +1 , where for every i ∈ [2 r + 1], C i = C 1+(p-1)•(i-1)
. Intuitively, we pick C (p) in a way that every two consecutive cycles C i and C i+1 of C (p) crop a (p, q)-railed annulus. For every w ∈ {0, 1} r , we use A w to denote the (p, q)-annulus that is cropped by the cycles C n w and C n w +1 of C (p) , where n w = 1 + i∈[r] w i 2 r-i+1 (i.e., A w = A 1+(p-1)•(n w -1),1+(p-1)•n w ). See Figure 9 for an example. Given a w ∈ {0, 1} r , we define

A 000 A 001 A 010 A 011 A 100 A 101 A 110 A 111 A C 1 C 2 C 3 C 4 C 5 C 6 C 7 C 8 C 9
G (t)
w to be the graph G (t)

A w . In the rest of the paper, given an r ∈ N and a w ∈ {0, 1} r , we denote by G w the -boundaried graph G ( ) w , where := f 2 ( r 2 ) + 1 (where f 2 is the first of the two functions of Proposition 2), we use G w to denote its underlying graph, and v r+1 , . . . , v r+ to denote its boundary vertices. Also, we denote by G out w the graph G \ (V (G w) \ {v r+1 , . . . , v r+ }) and by G out w the -boundaried graph (G out w , v r+1 , . . . , v r+ ).

Combing linkages in levelings of flat annuli

We now formulate Proposition 2 in terms of pairings of the graphs G w and G out w . That is, for every linkage with terminals v 1 , . . . , v r , we prove that another equivalent linkage can be found, being combed through the extra boundary vertices of G w and G out w (see Lemma 4). Before presenting Lemma 4 and its proof, we introduce some additional notation.

Let G be a graph and let (A, R) be a well-aligned (2 r • (p -1) + 1, q)-railed annulus flatness pair of G, for some odd p ∈ N ≥3 , and some q ∈ N ≥3 . Let v 1 , . . . , v r ∈ V (G) and let ( w, ω 1 . . . ω r ) be the trace of (v 1 , . . . , v r ). We use v• to denote the tuple

(v • 1 , . . . , v • r ), where for every i ∈ [r], v • i = v i , if ω i = •, and v • i = ␣, if ω i = •. Also, we use v• to denote the tuple (v • 1 , . . . , v • r ), where for every i ∈ [r], v • i = v i , if ω i = •, and v • i = ␣, if ω i = •. We use (G w, v• ) to denote (G w, v• , v r+1 , . . . , v r+ ) and (G out w , v• ) to denote (G out w , v• , v r+1 , . . . , v r+ ).
Lemma 4. There is a function f 5 : N → N such that for every r ∈ N, if G is a graph, (A, R) is a well-aligned (f 5 (r), )-railed annulus flatness pair of G, and

(L, v 1 , . . . , v r ) ∈ Pairings(G, v 1 , . . . , v r ), where v 1 , . . . , v r ∈ V (G), then there exists a ( L, v 1 , . . . , v r ) ∈ Pairings(G, v 1 , . . . , v r ) such that L ≡ L and ( L, v 1 , . . . , v r ) ∈ Pairings(G w, v• ) ⊕ Pairings(G out w , v• ), where ( w, ω) = trace (A,R) (v 1 , . . . , v r ).
Proof. We set f 5 (r) = 2 r • (p -1) + 1, where p = f 3 ( r 2 ) + 5. Recall that G w and G out w are (r + )-boundaried graphs where = f 2 ( r 2 ) + 1 and whose boundary vertices are v

1 , . . . , v r+ . Let (L, v 1 , . . . , v r ) ∈ Pairings(G, v 1 , . . . , v r ).
We set ( w, ω 1 . . . ω r ) = trace (A,R) (v 1 , . . . , v r ) and we consider the (p, q)-railed annulus A w of G. Observe that v 1 , . . . , v r / ∈ Influence R (A w) and therefore, by Lemma 12, we have that Leveling (A w ,R) (G) contains a linkage L that is equivalent to L and it is ann(R A w )-avoiding. We set ∆ = ann(R A w ) and we note that R A w is a ∆-embedded (p, q)-railed annulus of Leveling (A,R) (G). By applying Proposition 2 for the (p, q)-railed annulus R A w , for s = 3, and for I = [ ], we have that Leveling (A w ,R) (G) contains a linkage L that is equivalent to L (and, therefore, equivalent to L) and is (3, I)-confined in R A w .

We set L• := L∩G w and L

• := L∩G out w . Observe that ( L• , v• , v r+1 , . . . , v r+ ) ∈ Pairings(G w, v• ) and ( L• , v• , v r+1 , . . . , v r+ ) ∈ Pairings(G out w , v• ). Also, the pairings ( L• , v• , v r+1 , . . . , v r+ ) and ( L• , v• , v r+1 , . . . , v r+ ) are -compatible and ( L, v 1 , . . . , v r ) = ( L• , v• , v r+1 , . . . , v r+ ) ⊕ ( L• , v• , v r+1 , . . . , v r+ ). Since ( L• , v• , v r+1 , . . . , v r+ ) ∈ Pairings(G w, v• ) and ( L• , v• , v r+1 , . . . , v r+ ) ∈ Pairings(G out w , v• ), we have that ( L, v 1 , . . . , v r ) ∈ Pairings(G w, v• ) ⊕ Pairings(G out w , v• ).

Partial signatures of tuples of vertices

We now present the definition of partial signatures. It is a recursive definition, that in the base case captures the pattern of a boundaried graph and for every recursive step, asks for all possible partial signatures that can be obtained after fixing another (boundary) vertex or its absence. Intuitively, the symbol "␣" expresses the absence of a vertex for this entry, or, in other words, that this vertex should be picked inside some boundaried graph that should be glued to our considered boundaried graph. In this sense, partial signatures express "partial" patterns (see Observation 10).

Let τ be a colored-graph vocabulary and let c = {c 1 , . . . , c l } be a collection of l constant symbols. Let r ∈ N. Recall that = f 2 ( r 2 ) + 1, where f 2 is the second function of Proposition 2. Let G be a τ -structure, let R ⊆ V (G), and let (A, R) be a well-aligned (2 r + 1, )-railed annulus flatness pair of G. For every i ∈ [r] and every w ∈ {0, 1} i , we define

R w = {v ∈ R | stamp w 1 ...w i-1 (v) = (w i , •)} and V w = {v ∈ V (G) | stamp w 1 ...w i-1 (v) = (w i , •)}. Partial signature. Let d ∈ N and r ∈ [d -1]. Given a w ∈ {0, 1} d and v 1 , . . . , v d such that for every i ∈ [r], v i ∈ R w 1 ...w i ∪ {␣} and for every i ∈ [r + 1, d], v i ∈ V w 1 ...w i ∪ {␣}, we define partial-sig 0 r (G, R, w, v 1 , . . . , v d ) = pattern(G w, ␣ l , v 1 , . . . , v d ). Also, for each i ∈ [d -r], every w ∈ {0, 1} d-i and every v 1 , . . . , v d-i ∈ V (G) ∪ {␣} such that for every j ∈ [min{r, d -i}], v j ∈ R w 1 ...w j ∪ {␣} and for every j ∈ [min{r, d -i} + 1, d -i], v j ∈ V w 1 ...w j ∪ {␣}, we define partial-sig i r (G, R, w, v 1 , . . . , v d-i ) = {partial-sig i-1 r (G, R, w0, v 1 , . . . , v d-i , v) | v ∈ V w0 } ∪ {partial-sig i-1 r (G, R, w1, v 1 , . . . , v d-i , v) | v ∈ V w1 } ∪ {partial-sig i-1 r (G, R, w0, v 1 , . . . , v d-i , ␣)} ∪ {partial-sig i-1 r (G, R, w1, v 1 , . . . , v d-i , ␣)} Also, for each i ∈ [d -r + 1, d -1], every w ∈ {0, 1} d-i and every v 1 , . . . , v d-i ∈ V (G) ∪ {␣} such that for every j ∈ [min{r, d -i}], v j ∈ R w 1 ...w j ∪ {␣}, and for every j ∈ [min{r, d -i} + 1, d -i], v j ∈ V w 1 ...w j ∪ {␣}, we define partial-sig i r (G, R, w, v 1 , . . . , v d-i ) = {partial-sig i-1 r (G, R, w0, v 1 , . . . , v d-i , v) | v ∈ R w0 } ∪ {partial-sig i-1 r (G, R, w1, v 1 , . . . , v d-i , v) | v ∈ R w1 } ∪ {partial-sig i-1 r (G, R, w0, v 1 , . . . , v d-i , ␣)} ∪ {partial-sig i-1 r (G, R, w1, v 1 , . . . , v d-i , ␣)} Finally, we define partial-sig d r (G, R) = {partial-sig d-1 r (G, R, 0, v) | v ∈ R 0 } ∪ {partial-sig d-1 r (G, R, 1, v) | v ∈ R 1 } ∪ {partial-sig d-1 r (G, R, 0, ␣)} ∪ {partial-sig d-1 r (G, R, 1, ␣)}
We use P(A) to denote the powerset of a set A and for every d ∈ N, we use P d (A) to denote the set P(P(• • • P d-times (A))). We observe the following.

Observation 10. Let d ∈ N and r ∈ [d -1]. For every i ∈ [0, d -1], every w ∈ {0, 1} d-i
, and every v ∈ (V (G) ∪ {␣}) r-i , where for every j ∈ [min{r, d -i}], v j ∈ R w 1 ...w j ∪ {␣}, and for every

j ∈ [min{r, d -i} + 1, d -i], v j ∈ V w 1 ...w j ∪ {␣}, it holds that partial-sig i r (G, R, w, v) ∈ P i (G (d+ ,h,l) pat ) and partial-sig d r (G, R) ∈ P d (G (d+ ,h,l) pat
).

Following the above definition, we also define (global) signatures where some vertices, up to some index, are asked to belong to R while the rest of them can belong in V (G). More formally, given some d ∈ N and some r ∈ [0, d], for every (v 1 , . . . , v d ) ∈ (V (G) ∪ {␣}) d , where v 1 , . . . , v r ∈ R, we define sig 0 r (G, R, v 1 , . . . , v d ) to be the atomic type of (v 1 , . . . , v d ). Also, for each i ∈ [d -r], and every v 1 , . . . , v d-i ∈ V (G) ∪ {␣}, where v 1 , . . . , v min{r,d-i} ∈ R, we define

sig i r (G, R, v 1 , . . . , v d-i ) = sig i-1 r (G, R, v 1 , . . . , v d-i , u) | u ∈ V (G) ∪ {␣} . Also, for each i ∈ [d -r + 1, d -1] and every v 1 , . . . , v d-i ∈ V (V (G) ∪ {␣}, where v 1 , . . . , v min{r,d-i} ∈ R, we define sig i r (G, R, v 1 , . . . , v d-i ) = sig i-1 r (G, R, v 1 , . . . , v d-i , u) | u ∈ V (G) ∪ {␣} , while for each i ∈ [d -r] and every v 1 , . . . , v d-i ∈ V (V (G) ∪ {␣}, where v 1 , . . . , v min{r,d-i} ∈ R, we define sig i r (G, R, v 1 , . . . , v d-i ) = sig i-1 r (G, R, v 1 , . . . , v d-i , u) | u ∈ R ∪ {␣} . Finally, we define sig d r (G, R) = sig d-1 r (G, R, v) | v ∈ R ∪ {␣} .

Exchangeability of graphs with the same partial signature

The goal of this section is to present Lemma 5 and its proof. This result states that in the presence of a railed annulus flatness pair in side an (annotated) colored graph (D, R), two (annotated) colored graphs (G, R), (G , R ) that yield the same partial signature when "glued in the inner part" of (D, R), satisfy the same formulas when we additionally glue another (annotated) colored graph (F, R ) in the outer part of (D, R). We now formalize the idea of "gluing".

Compatible colored graphs. Let G = (G, X 1 , . . . , X h ), G = (G , X 1 , . . . , X h ) be two colored graphs and let a partial function η : V (G) → V (G ). We say that G and G are η-compatible if for every

i ∈ [h] and every v ∈ X i , v ∈ X i ⇐⇒ η(v) ∈ X i .
Gluing colored graphs. Let G, D be two colored graphs and let a partial function η : V (G) → V (H) such that G and D are η-compatible. We denote by G ⊕ η D the colored graph obtained from the disjoint union of G and D after identifying

vertices v ∈ V (G) and u ∈ V (H) if η(v) = u.
Inner-and outer-compatibility functions. Let two colored graphs G, H, let a be an apextuple of G, and let (A, R) be a railed annulus flatness pair of

G \ V (a). Given that R = (X 1 , Y 1 , X 2 , Y 2 , Z 1 , Z 2 , Γ, σ, π), we call a partial function η : V (X 1 ∩ Y 1 ) ∪ V (a) → V (H) (resp. ξ : V (X 2 ∩ Y 2 ) ∪ V (a) → V (H)
) such that G and H are η-compatible (resp. ξ-compatible) an inner-compatibility (resp. outer-compatibility) function of G and H.

Lemma 5. Let τ be a colored-graph vocabulary and let r, l ∈ N and let d = f 4 (r, l). Let (D, R) be a colored graph, let a be an apex-tuple of D of size l, and let (A, R) be a well-aligned (f 5 (r), )railed annulus flatness pair of D \ V (a). Also, let (G, R), (G , R ) be two colored graphs and let two inner-compatibility functions η, η of (D, R) and

(G, R) (resp. (G , R )). If partial-sig d r (ap c ((G, R) ⊕ η (D, R), a)) = partial-sig d r (ap c ((G , R ) ⊕ η (D, R), a)
), then for every (τ ∪{R})-structure (F, R ), every outer-compatibility function ξ of (D, R) and (F, R ), it holds that

sig r (G, R) ⊕ η (D, R) ⊕ ξ (F, R ) = sig r (G , R ) ⊕ η (D, R) ⊕ ξ (F, R ) . ap c (G ⊕ η D ⊕ ξ F, a)
there are no edges between V (a) and V (ap c (G ⊕ η D ⊕ ξ F, a) \ V (a)), we can update R by adding V (a) to X2 and observe that after this modification of R, (A, R) is a railed annulus flatness pair of ap c (G ⊕ η D ⊕ ξ F, a). For the same reasons, we can assume that (A, R ) is a railed annulus flatness pair of ap c (G ⊕ η D ⊕ ξ F, a). We set

• (Z, R) := (G, R) ⊕ η (D, R) ⊕ ξ (F, R ), • (Z , R ) := (G , R ) ⊕ η (D, R) ⊕ ξ (F, R ),
• (H, R, a) := ap c (Z, R, a), and

• (H , R , a) := ap c (Z , R , a).
Our goal is to prove that sig r (Z, R) = sig r (Z , R ). To achieve this, it will suffice to show that

sig d r (H, R, a) = sig d r (H , R , a). Let us first prove that sig d r (H, R, a) = sig d r (H , R , a) implies sig r (Z, R) = sig r (Z , R ).
For this, we will prove that for every quantifier-free formula ψ(x 1 , . . . , x r ) of FOL[τ + dp] on r free variables, the following holds

: if v 1 , . . . , v r ∈ R and v 1 , . . . , v r ∈ R such that sig i (Z, R, v 1 , . . . , v r-i ) = sig i (Z , R , v 1 , . . . , v r-i ), for every i ∈ [r -1], then it holds that (Z, v 1 , . . . , v r ) |= ψ(x 1 , . . . , x r ) ⇐⇒ (Z, v 1 , . . . , v r ) |= ψ(x 1 , . . . , x r ). Let ψ(x 1 , . . . , x r ) be such a formula and let v 1 , . . . , v r ∈ R and v 1 , . . . , v r ∈ R such that sig i (Z, R, v 1 , . . . , v r-i ) = sig i (Z , R , v 1 , . . . , v r-i ), for every i ∈ [r -1]. Assuming that sig d r (H, R, a) = sig d r (H , R , a), it holds that sig d-r r (H, R, a, v 1 , . . . , v r ) = sig d-r r (H , R , a, v 1 , . . . , v r ). Therefore, by Lemma 2, we have (H, a, v 1 , . . . , v r ) |= ψ l ⇐⇒ (H , a, v 1 , . . . , v r ) |= ψ l ,
where ψ l is the apex-projection of ψ (see Subsection 6.2). Also, by Lemma 3,

(Z, v 1 , . . . , v r ) |= ψ ⇐⇒ (H, a, v 1 , . . . , v r ) |= ψ l and (Z, v 1 , . . . , v r ) |= ψ ⇐⇒ (H , a, v 1 , . . . , v r ) |= ψ l . Combining these last three logical equivalences, we get (Z, v 1 , . . . , v r ) |= ψ ⇐⇒ (Z, v 1 , . . . , v r ) |= ψ.
We devote the rest of the proof to show that sig d r (H, R, a) = sig d r (H , R , a). Let λ be an assignment of (H, R) to a rooted tree (T, t 0 ) and let λ be an assignment of (H , R ) to a rooted tree (T , t 0 ).

To prove that sig d r (H, R, a) = sig d r (H , R , a), it suffices to prove that for every i ∈ [0, d] and every γ ∈ P d-i (G (t,h) pat ), the two following statements hold:

(i) For every (t 0 , . . . , t i ) ∈ Paths(T ) there exist (t 0 , . . . , t i ) ∈ Paths(T ) such that sig d-i r (H, R, a, λ(t 1 ), . . . , λ(t i )) = sig t (H , R , a, λ (t 1 ), . . . , λ (t i )).

(ii) for every (t 0 , . . . , t i ) ∈ Paths(T ) there exist (t 0 , . . . , t i ) ∈ Paths(T ) such that

sig d-i r (H, R, a, λ(t 1 ), . . . , λ(t i )) = sig t (H , R , a, λ (t 1 ), . . . , λ (t i )).
We will show only a proof for (i), since the proof of (ii) will be totally symmetric to the one of (i).

In fact, we will prove the following statement, which is equivalent to (i). pat , it holds that: For every (t 0 , . . . , t i ) ∈ Paths(T ) there is a (t 0 , . . . , t i ) ∈ Paths(T ) such that for every t d ∈ L(T t i ), where (t 0 , . . . , t d ) ∈ Paths(T ), there is a t d ∈ L(T t i

), where (t 0 , . . . , t d ) ∈ Paths(T ), such that

sig 0 r (H, R, a, λ(t 1 ), . . . , λ(t d )) = sig 0 r (H , R , a, λ (t 1 ), . . . , λ (t d )).
there is a t d ∈ L(T t i ), where (t 0 , . . . , t d ) ∈ Paths(T ), such that sig 0 r (H, a, λ(t 1 ), . . . , λ(t d )) = sig 0 r (H , a, λ (t 1 ), . . . , λ (t d )). This concludes the proof of the claim. By Claim 3, we have that for every i ∈ [0, d] and every (t 0 , . . . , t i ) ∈ Paths(T ) there exist (t 0 , . . . , t i ) ∈ Paths(T ) such that sig d-i r (H, R, a, λ(t 1 ), . . . , λ(t i )) = sig d-i r (H , R , a, λ (t 1 ), . . . , λ (t i )). Symmetrically, one can prove that for every i ∈ [0, d] and every (t 0 , . . . , t i ) ∈ Paths(T ) there exist (t 0 , . . . , t i ) ∈ Paths(T ) such that sig d-i r (H, R, a, λ(t 1 ), . . . , λ(t i )) = sig d-i r (H , R , a, λ (t 1 ), . . . , λ (t i )). These two imply that sig d r (H, R, a) = sig d r (H , R , a).

Proof of Theorem 3

In this section, we aim to show Theorem 3. In this direction, in Subsection 8.1, we define representatives of vertices, following the notion of partial signatures defined in the previous section. Using Courcelle's theorem, we are able to compute these representatives and therefore obtain a "reduced" colored graph that has the same signature as the initial one (Lemma 6). Using this and in the presence of a big enough flat wall, in Subsection 8.2 we argue how to safely remove vertices from a bidimensional area of the graph where no variables of the sentence are quantified and obtain a "reduced" equivalent instance of the (annotated) problem. This will allow us to apply iteratively this procedure in order to reduce the treewidth of the given colored graph. We wrap-up the proof of Theorem 3 in Subsection 8.3.

Representatives

Let d ∈ N and r ∈ [d -1]. Let (G, R
) be an (annotated) colored graph and let (A, R) be a well-aligned (f 5 (d), )-railed annulus flatness pair of G. Recall that for every i ∈ [d] and every w 1 , . . . ,

w i ∈ {0, 1}, R w 1 ...w i = {v ∈ R | stamp w 1 ...w i-1 (v) = (w i , •)} and V w 1 ...w i = {v ∈ V (G) | stamp w 1 ...w i-1 (v) = (w i , •)}.
Given an i ∈ [d] and v 1 , . . . , v i-1 ∈ V (G) ∪ {␣} such that for every j ∈ [min{r, d -i}], v j ∈ R w 1 ...w j ∪ {␣}, and, for every j ∈ [min{r, d -i} + 1, d -i], v j ∈ V w 1 ...w j ∪ {␣}, where (w 1 , . . . , w i-1 , ω) = trace (A,R) (v 1 , . . . , v i-1 ), we say that two vertices

v, v ∈ V (G) such that v, v ∈ R w 1 ...w i-1 0 ∪ R w 1 ...w i-1 1 if i ∈ [min{r, d -i}], and v, v ∈ V w 1 ...w i-1 0 ∪ R w 1 ...w i-1 1 if i ∈ [min{r, d -i} + 1, d -i], are ((v 1 , . . . , v i-1 ), i)-equivalent, which we denote by v ∼ (v 1 ,...,v i-1 ) i v , if stamp w 1 ...w i-1 (v) = stamp w 1 ...w i-1 (v ) = (w i , •) and sig d-i r (G, R, w 1 . . . w i-1 w i , v 1 , . . . , v i-1 , v) = sig d-i r (G, R, w 1 . . . w i-1 w i , v 1 , . . . , v i-1 , v
). Following Observation 3 and Observation 10, we can easily derive an upper bound to the number of equivalence classes of each equivalence relation above.

Observation 11. There is a function f 6 : N → N such that for every i ∈ [d] and every v 1 , . . . , v i-1 ∈ V (G) ∪ {␣}, such that for every j ∈ [i -1], v j ∈ V (G) w 1 ...w j ∪ {␣}, where (w 1 , . . . , w i-1 , ω) = trace (A,R) (v 1 , . . . , v i-1 ), it holds that the number of equivalence classes of

∼ (v 1 ,...,v i-1 ) i is at most f 6 (d).
We can now prove the main result of this subsection. Proof. We set f 7 = f 6 (d) • d. First observe that partial-sig d r can be expressed in MSOL. The fact that tw(G[Y 2 ]) ≤ tw and that for every w ∈ {0, 1} d , V (G w) is a subset of X 2 implies that, by using Courcelle's theorem, we can compute, in time O d,tw (n), a subset R of R such that Y 2 ∩ X 2 ⊆ R and for every i ∈ [d] and every v 1 , . . . , v i-1 ∈ V (G), it holds that for every v in R such that v ∈ Z, if v ∼ (v 1 ,...,v i-1 ) i u, for some u ∈ R, then u = v. Intuitively, we obtain R from R by keeping only one representative from each equivalence class (that itself can be expressed in MSOL) inside Z. By Observation 11, it follows that |R ∩ Z| ≤ f 7 (d).

To conclude this subsection, we next show how to combine Lemma 6 and Lemma 5 in order to compute an equivalent colored graph with reduced annotation. Let two colored graphs G, H, let a be an apex-tuple of G, and let (W, R) be a flatness pair of G\V (a). Given that R = (X, Y, P, C, Γ, σ, π), we call a partial function ξ : V (X ∩ Y ) ∪ V (a) → V (H) such that G and H are ξ-compatible a compatibility function of G and H. Lemma 7. Let τ be a colored-graph vocabulary. There is a function f 8 : N 3 → N and an algorithm that, given • r, l, q ∈ N,

• a τ -structure G,

• an apex-tuple a of G of size l,

• a regular flatness pair (W, R) of G \ V (a) of height at least f 8 (r, l, q) whose compass has treewidth at most tw, and

• a set R ⊆ V (G),
outputs, in time O r,l,q,tw (n), a set R ⊆ R and a flatness pair ( W , R ) of G \ V (a) that is a Wtilt of (W, R) for some q-subwall W of W such that R ∩ V (Compass R ( W )) = ∅ and for every (τ ∪ {R})-structure (F, R ) and every compatibility function ξ of (G, R) and (F, R ), it holds that

sig r ((F, R ) ⊕ ξ (G, R)) = sig r ((F, R ) ⊕ ξ (G, R )).
Proof. We set and let d = f 4 (r, l), p = f 5 (d), y = , g = f 17 (f 7 (d) + 1, q), and f 8 (d, y) = odd(2p + max{g, y 4 -1}). We first apply Proposition 1, and obtain a (p, y)-railed annulus A of G \ V (a). We set (X, Y, P, C, Γ, π, σ) = R. Let Σ be the union of all W (g+1) -internal cells of R. By setting

Y 2 := Y , X 2 := X, Y 1 = Σ ∪ {V (σ) | c is a W (g+1) -marginal cell of R}, and X 1 = V (G) \ Σ, we obtain a tuple R = (X 1 , Y 1 , X 2 , Y 2 , Z 1 , Z 2 , Γ , π , σ )
, where Γ , π , σ are the restrictions of Γ, π, σ, respectively to Γ \ Σ.

Observe that since (W, R) is a flatness pair of G \ V (a), then (A, R ) is a railed annulus flatness pair of G \ V (a). Also, since (W, R) is regular, it is also well-aligned (Proposition 10), which implies that (A, R ) is also well-aligned. Moreover, since Compass R (W ) has treewidth at most tw, we have that tw(G[Y 2 ]) ≤ tw. Therefore, by applying the algorithm of Lemma 6, we find, in time

O d,tw (n), a set R ⊆ V (G) such that R ⊆ R, |R ∩ Y 1 | ≤ f 7 (d),
-tilt ( W , R ) of (W, R) such that R ∩ V (Compass R ( W )) = ∅.
Since partial-sig d r (ap c ((G, R), a)) = partial-sig d r (ap c ((G, R ), a)), by Lemma 5, we have that for every (τ ∪ {R})-structure (F, R ), every compatibility function ξ of (G, R) and (F, R ), it holds that sig r ((

F, R ) ⊕ ξ (G, R)) = sig r ((F, R ) ⊕ ξ (G, R )).

Reducing the instance

In this subsection we describe how to remove problem-irrelevant vertices inside a "big enough" annotation-irrelevant bidimensional area of our instance. In order to achieve this, we have to argue that a linkage whose terminals are not intersecting a big enough bidimensional area can be rerouted away from some central part of this area. This is guaranteed by the following version of the Unique Linkage Theorem that can be derived from [START_REF] Baste | Hitting minors on bounded treewidth graphs[END_REF]Theorem 23] (see also [START_REF] Adler | Irrelevant vertices for the planar Disjoint Paths Problem[END_REF][START_REF] Kawarabayashi | A shorter proof of the graph minor algorithm: the unique linkage theorem[END_REF][START_REF] Mazoit | A single exponential bound for the redundant vertex theorem on surfaces[END_REF][START_REF] Robertson | Graph minors. XXI. Graphs with unique linkages[END_REF][START_REF] Robertson | Graph Minors. XXII. Irrelevant vertices in linkage problems[END_REF]). Proposition 3. There exists a function f 9 : N 3 → N such that, for every l, z, k ∈ N, if G is a graph, a is an apex-tuple of G of size l, if (W, R) is flatness pair of G \ V (a) of height f 9 (l, z, k) then for every linkage L of size at most k such that T (L) ∩ V (Compass R (W )) = ∅, there is a linkage L such that L ≡ L and L ∩ V (Compass R ( W )) = ∅, where ( W , R ) is a W (z) -tilt of (W, R).

Using Proposition 3, we can easily prove the following result that allows us to remove problemirrelevant vertices inside a "big enough" annotation-irrelevant bidimensional area of our instance. Lemma 8. Let τ be a colored-graph vocabulary. There is a function

f 10 : N 2 → N such that, if • r, l, z ∈ N, • G is a τ -structure,
• a is an apex-tuple of G of size l,

• (W, R) is a flatness pair of G \ V (a) of height f 10 (r, l) + z, and

• R ⊆ V (G), where R ∩ V (Compass R (W )) = ∅,
then for every flatness pair ( W , R ) of G\V (a) that is a W -tilt of (W, R) for some f 10 (q, l)-internal subwall W of W of height z, for every (τ ∪ {R})-structure (F, R ), every compatibility function ξ of (G, R) and (F, R ), and every Y ⊆ V (Compass R ( W )), it holds that

sig r ((F, R ) ⊕ ξ (G, R)) = sig r ((F, R ) ⊕ ξ (G \ Y, R)).
Proof. We set f 10 (r, l) = f 9 (l, z, r). Let G be a τ -structure, let a be an apex-tuple of G of size l, let (W, R) be regular flatness pair of G \ V (a) of height f 10 (r, l) + z, and let R ⊆ V (G), where R∩V (Compass R (W )) = ∅. Also, let ( W , R ) be a flatness pair of G\V (a) that is a W -tilt of (W, R) for some f 10 (q, l)-internal subwall W of W of height z. Let also Y ⊆ V (Compass R ( W )). Observe that, for every k ∈ r/2 and every s 1 , t

1 . . . , s k , t k ∈ R, by Proposition 3, if G is the Gaifman graph of (G, R), then (G, s 1 , t 1 , . . . , s k , t k ) |= dp k (x 1 , y 1 , . . . , x k , y k ) if and only if (G \ Y, s 1 , t 1 , . . . , s k , t k ) |= dp k (x 1 , y 1 , . . . , x k , y k ). This implies that sig r ((F, R ) ⊕ ξ (G, R)) = sig r ((F, R ) ⊕ ξ (G \ Y, R)).
By applying Lemma 7 and then Lemma 8, we get the following: Lemma 9. Let τ be a colored-graph vocabulary. There is a function f 11 : N 3 → N and an algorithm that, given r, l, q ∈ N, a τ -structure G, an apex-tuple a of G of size l, a regular flatness pair (W, R) of G \ V (a) of height h ≥ f 11 (r, l, q) whose compass has treewidth at most tw, and a set R ⊆ V (G), outputs, in time O r,l,q,tw (n), a set R ⊆ V (G) and a flatness pair ( W , R ) of G \ V (a) that is a W -tilt of (W, R) for some q-subwall W of W such that R ⊆ R, R ∩ V (Compass R ( W )) = ∅, and for every (τ ∪ {R})-structure (F, R ), every compatibility function ξ of (G, R) and (F, R ), and every

Y ⊆ V (Compass R ( W )), it holds that sig r ((F, R ) ⊕ ξ (G, R)) = sig r ((F, R ) ⊕ ξ (G \ Y, R )).

Proof of Theorem 3

We conclude this section by presenting the proof of Theorem 3.

Proof of Theorem 3. Given a sentence ϕ ∈ FOL[τ + dp] of quantifier rank q, we set c := hw(G), l := f 19 (c) where f 19 is the function of Proposition 9, and r := f 11 (q, l, 3).

Our algorithm consists of three steps.

Step 1: Run the algorithm of Proposition 9 for G, r, and c. This algorithm outputs, in linear time, either a tree decomposition of G of width at most f 20 (c) • r, or a set A ⊆ V (G), where |A| ≤ l, a regular flatness pair (W, R) of G \ A of height r, and a tree decomposition of compass R (W ) of width at most f 20 (c) • r. In the first possible output, i.e., a tree decomposition of G of width at most f 20 (c) • r, proceed to Step 3. In the second possible output, proceed to Step 2.

Step 2: We run the algorithm of Lemma 9 for q, l, 3, G, R, a, and (W, R), and we obtain, in linear time, a set R ⊆ V (G) and a flatness pair ( W , R ) of G \ V (a) that is a W -tilt of (W, R) for some subwall W of W of height 3 such that V (compass R ( W )) ∩ R = ∅, R ⊆ R, and sig q (G, R) = sig q (G \ V (compass R ( W )), R ). Then, we set G := G \ V (compass R ( W )), R := R , and we run again Step 1.

Step 3: Given a tree decomposition of G of width at most f 20 (c) • r, and since sig q is expressible in MSOL[τ ], by using Courcelle's theorem, in linear time we can compute sig q (G, R) and check the existence of a ϕ-spanning subtree of the tree obtained by sig q (G, R) and therefore decide whether G |= ϕ.

Observe that the first and the second step of the algorithm are executed in linear time and they can be repeated no more than a linear number of times. Therefore, the overall algorithm runs in quadratic time, as claimed.

Logic for s-scattered paths

In this section we define a class of extensions of FOL, in the same spirit as the disjoint paths logic.

Definition of s-scattered paths logic

Let r ∈ N. We define the 2k-ary predicate s-sdp k (x 1 , y 1 , . . . , x k , y k ), which evaluates true in a τstructure G if and only if there are paths P 1 , . . . , P k of (V (G), E G ) of length at least 2 between (the interpretations of) x i and y i for all i ∈ [k] such that for every i, j

∈ [k], j = i, V (P i ) ∩ N (≤s) (V (G),E G ) (V (P j )) = ∅. We let τ + s-sdp := τ ∪ {i-sdp k | k ≥ 1, i ≤ s},
where each s-sdp k is a 2k-ary relation symbol. We use s-sdp instead of s-sdp k when k is clear from the context. It is easy to see that for every k ∈ N and every x 1 , y 1 , . . . , x k , y k ∈ V (G),

G |= 0-sdp k (x 1 , y 1 , . . . , x k , y k ) ⇐⇒ G |= dp k (x 1 , y 1 , . . . , x k , y k ).
Therefore, we can observe the following.

Observation 12. For every colored-graph vocabulary τ , it holds that {Mod(ϕ

) | ϕ ∈ FOL[τ +dp]} = {Mod(ϕ) | ϕ ∈ FOL[τ + 0-sdp]}.
Our main result is the following: Theorem 4. For every colored-graph vocabulary τ , every s ∈ N, and every sentence ϕ ∈ FOL[τ + s-sdp], there exists an algorithm that, given a τ -structure G of size n, outputs whether G |= ϕ in time O |ϕ|,k (n 2 ), where k is the Euler genus of G.

Proof of Theorem 4

In this subsection, we sketch how to prove Theorem 4. Our strategy is the same as for the proof of Theorem 3 and in what follows we discuss how to recreate definitions and results of the previous sections in the setting of s-scattered paths. We use s-sig to denote the signature obtained from sig where we replace the atomic types concerning disjoint paths predicates with scattered disjoint path predicates.

First of all, we stress that since we work with graphs of bounded Euler genus, we can avoid the use of the framework of flat walls. In fact, using [102, Lemma 6.2] (see also [START_REF] Hans | A c k n 5-approximation algorithm for treewidth[END_REF][START_REF] Cabello | Finding shortest non-trivial cycles in directed graphs on surfaces[END_REF][START_REF] Demaine | Subexponential parameterized algorithms on bounded-genus graphs and H -minor-free graphs[END_REF][START_REF] Demaine | Subexponential parameterized algorithms on bounded-genus graphs and H -minor-free graphs[END_REF][START_REF] Demaine | The bidimensional theory of bounded-genus graphs[END_REF][START_REF] Demaine | Linearity of grid minors in treewidth with applications through bidimensionality[END_REF][START_REF] Fedor | Contraction obstructions for treewidth[END_REF][START_REF] Geelen | Embedding grids in surfaces[END_REF]), we can find a disk-embedded wall of bounded treewidth compass in a surface-embedded of large enough treewidth. Before presenting this result, we give some additional definitions. Given a closed disk ∆ and an integer q ∈ N ≥3 , a ∆-embedded q-wall of G is a q-wall W that is embedded on ∆ and whose perimeter is the boundary of ∆. The compass of W , denoted by Compass(W ), is the graph G ∩ ∆. Proposition 4. There exists a constant c 1 and an algorithm that given an n-vertex graph G of Euler genus at most g and an integer q ∈ N ≥3 , outputs either a closed disk ∆ and a ∆-embedded q-wall W of G whose compass has treewidth at most c 1 • q or a tree decomposition of G of width at most c 1 • q. Moreover, this algorithm runs in 2 Og(q 2 ) • n time.

Patterns for s-scattered linkages. Next step is to define patterns that encode s-scattered linkages. Given an s ∈ N, we say that a linkage L of G is s-scattered if for every v ∈ V (L) it holds that

N (≤s) G (v) ∩ (V (L) \ V (C v )) = ∅, where C v is the connected component of L that contains v.
Observe that, since N (≤0) G (v) = {v}, every linkage is 0-scattered. To define patterns that encode s-scattered linkages, the definition of a pattern of a boundaried colored graph in Subsection 4.2 has to be modified as follows: the collection H P is defined as all graphs (I, E), where E ⊆ I × I, such that G contains s-scattered paths of length at least two between the vertices v i , v j for all {i, j} ∈ E. Also, as in Subsection 4.3, we define the pattern of a quantifier-free formula in FOL[τ + s-sdp] by modifying the corresponding definition for formulas in FOL[τ +dp]. We do this by replacing, in both definitions of full clauses and in the definition of the collection H P c , every appearance of the atomic formula dp with the atomic formula s-sdp.

After the above modifications, Observation 6 holds also for sentences ϕ ∈ FOL[τ + s-sdp]. Based on this observation (for s-scattered linkages), we can then prove Lemma 2 for any sentence

ϕ ∈ FOL[τ + s-sdp].
Routing s-scattered linkages through railed annuli. Having Lemma 2 in hand, our next goal is to prove Lemma 4 for the case of s-scattered linkages. Recall that Lemma 4 intuitively states that, in the presence of a flat railed annulus A inside a given graph G, every linkage L of G can be combed through some paths of A in some "buffer" (obtained by some hierarchical refinement of A; see Subsection 7.2) of A corresponding to the position of the terminals of L. In the case of FOL[τ +dp], this is essentially a reformulation of Proposition 2 to the setting of pairings and flat railed annuli. Therefore, to generalize Lemma 4 to s-scattered linkages, one has to prove the analogue of Proposition 2 for s-scattered linkages. This was done in [START_REF] Golovach | Combing a linkage in an annulus[END_REF] and is stated below. However, this result is proven for graphs embeddable in some fixed surface and this is the reason why Theorem 4 holds up to graphs of bounded-genus. Proposition 5. There exist two functions f 12 , f 13 : N 3 → N such that for every odd ∈ N and every s, k, g ∈ N, if

• Σ is a surface of Euler genus g, • ∆ is a closed annulus of Σ, • G is a graph embedded in Σ • A = (C, P) is a ∆-embedded (p, q)-railed annulus of G, where p ≥ f 12 (s, k, g) + and q ≥ 2s+5 2 • f 13 (s, k, g)
• L is a ∆-avoiding s-scattered linkage of size at most k, and

• I ⊆ [q], where |I| > f 13 (s, k, g) • (s + 1), then G contains an s-scattered linkage L where L ≡ L, L \ ∆ ⊆ L \ ∆, and L is ( , I)-confined in A. Moreover, f 12 (s, k, g) = O((f 13 (s, k, g)) 2 ) and f 13 (s, k, g) = s • 2 O(k+g) .
Using Proposition 5 and adjusting the definitions in Subsection 5.3 for the s-scattered linkages setting (this is done by just modifying the definition of pairings to consider (boundaried) linkages that are s-scattered), we can prove the analogue of Lemma 4.

Partial signatures and exchangeability for FOL[τ + s-sdp].

The next important task is to define partial signatures of colored graphs (equipped with a disk-embedded railed annulus) that encode the (recursive) containment of "meta-collections" of s-scattered linkages in a recursively obtained collection of boundaried (sub)graphs. This is done as for FOL[τ +dp] (see Subsection 7.4) by building the recursive definition of partial signatures using the "s-scattered" patterns, as defined two paragraphs above, for the base of the recursion. Using this definition, one can formulate Lemma 5 for FOL[τ + s-sdp]. The proof of this analogous version of Lemma 5 is actually the same as the one in Subsection 7.5 and uses the "s-scattered" versions of Lemma 2 and Lemma 4. Let us stress that since Proposition 5 demands that the given graph G is embedded on a fixed surface, this also holds for the "s-scattered" version of Lemma 4 and therefore, in the "s-scattered" version of Lemma 5, all considered colored graphs G, G , H, and F should be embedded on some fixed surface and their "gluing" should also preserve embeddability. Also, since we deal with graphs of bounded Euler genus and using Proposition 4 we can directly obtain a disk-embedded wall if our input graph has large enough treewidth, there are no apices to deal with. Therefore, for FOL[τ + s-sdp], we do not need to apply the transformations of Section 6.

Finding representatives and proof of Theorem 4. From this point on, the steps towards the proof of Theorem 4 are completely analogous to the ones in Section 8 for the proof of Theorem 3. With the "s-scattered" version of Lemma 5 in our toolbox, we have to find an (annotated) colored graph with the same partial signature as the original one. This will allow us to reduce the annotation of the original colored graph. To do this, we define representatives of vertices with the same recursive "s-scattered" partial signature as in Subsection 8.1 and we deduce the "s-scattered" analogue of Lemma 6. In turn, Lemma 6, when combined with Lemma 5, implies Lemma 7 for sentences in FOL[τ + s-sdp]. Last remaining piece is to prove the following analogue of Lemma 8 for sentences in FOL[τ + s-sdp]. Given two colored graphs G, H and a disk-embedded wall W of G, a perimeter-compatibility function of G and H is any partial function ξ : V (D(W )) → V (H) such that G and H are ξ-compatible. Lemma 10. Let τ be a colored-graph vocabulary. There is a function f

14 : N 3 → N such that, if • s, g, r, q ∈ N,
• G is a τ -structure embedded in a surface Σ of Euler genus g,

• ∆ is a closed disk of Σ,
• W is a ∆-embedded (f 14 (s, r, g) + q)-wall of G, and

• R ⊆ V (G), where R ∩ V (Compass(W )) = ∅,
then for every f 14 (s, r, g)-internal q-subwall W of W , every (τ ∪ {R})-structure (F, R ), every compatibility function ξ of (G, R) and (F, R ), and every Y ⊆ V (Compass(W )), it holds that

s-sig r ((F, R ) ⊕ ξ (G, R)) = s-sig r ((F, R ) ⊕ ξ (G \ Y, R)).
The proof of Lemma 10 is obtained by the proof of Lemma 8 (see Subsection 8.2) by replacing the application of Proposition 3 by Proposition 5 combined with an "s-scattered" version of Lemma 12 (for the proof of the latter, it is easy to observe that it can be directly generalized to s-scattered linkages).

Then, using the "s-scattered" version of Lemma 7 and Lemma 10, we obtain the analogue of Lemma 9, which we state below.

Lemma 11. There are two functions f 15 : N 3 → N and f 16 : N 4 → N and an algorithm that, given • s, g, r, q ∈ N,

• a τ -structure G of Euler genus at most g,

• a closed disk ∆,

• a ∆-embedded wall W of G of height at least f 15 (s, r, q) whose compass has treewidth at most tw, and

• a set R ⊆ V (G),
outputs, in time O s,g,t,q,tw (n), a set R ⊆ V (G) and a q-subwall W of W such that for every

Y ⊆ V (Compass(W )), every (τ ∪ {R})-structure (F, R ), every compatibility function ξ of (G, R) and (F, R ), s-sig r ((F, R ) ⊕ ξ (G, R)) = s-sig r ((F, R ) ⊕ ξ (G \ Y, R )).
The proof of Theorem 4 is obtained from the one of Theorem 3 (see Subsection 8.3), by plugging Proposition 4 and Lemma 11 instead of Proposition 9 and Lemma 9, respectively.

Conclusions and open problems

In this paper we proved two AMT's for the logic FOL+DP and its newly introduced extension FOL+SDP on graphs of bounded Hadwiger number and Euler genus respectively. These two logics can be seen as non-trivial extensions of FOL, as they may express a wide range of problems (and meta-problems) that are not FOL-expressible. (See Appendix A for an exposition of the expressivity potential of FOL+DP and FOL+SDP.)

Open problems

Recall that FOL+DP is an extension of the separator logic FOL+conn, introduced in [START_REF] Bojańczyk | Separator logic and star-free expressions for graphs[END_REF][START_REF] Schirrmacher | First-Order Logic with Connectivity Operators[END_REF]. The combinatorial condition given in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF] for this logic is having bounded Hajós number. As minor excluding graphs classes are also topological-minor excluding classes, the combinatorial condition of [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF] is more general that the one that we give for FOL+DP in this paper. This makes the AMT of [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF] non-comparable to ours. Moreover it is shown in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF] that, under certain complexity assumptions, the bounded Hajós number demand is actually demarking the combinatorial horizon of FOL+conn. The open question is whether having bounded Hajós number is also the combinatorial horizon of the more expressive FOL+DP. We are not in position to make a positive or negative conjecture on this. We wish only to comment that the algorithmic/combinatorial tools that where used in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF] are quite different than the ones used in this paper.

Another open question is to what extend one may further strengthen the expressibility dp k (•) (resp. s-sdp k (•)) predicate, while maintaining the combinatorial condition of bounded Hadwiger number (resp. bounded Euler genus). A possible candidate might be to ask for paths of guided disjointness, that is to consider the predicate gdp H (x 1 , y 1 , . . . , x k , y k ) where H is a graph where V (H) = {1, . . . , k} and where we ask that, for every edge (i, j) ∈ E(H), the (x i , y i )-path and the (x j , y j )-path are disjoint. Clearly, dp k (x 1 , y 1 , . . . , x k , y k ) = gdp K k (x 1 , y 1 , . . . , x k , y k ), therefore this would provide a more general logic than FOL+DP. To our knowledge, even the parameterized complexity of the evaluation of dp H (x 1 , y 1 , . . . , x k , y k ), when parameterized by k = |H|, is an interesting open problem.

Limitations

In the beginning of Appendix A we comment that FOL+DP, on multicolored (by z colors) graphs, may express the predicate dp k,λ (s 1 , t 1 , . . . , s k , t k ) equipped with a list function λ : [k] → 2 [z] , where we demand that, for every i ∈ [k], λ(i) is a subset of the set of all colors assigned to the vertices of the path between the (valuations) of s 1 and t 1 . Interestingly this permits us to demand certain colors to be traversed by the disjoint paths. However, on the negative side, we may not expect that FOL+DP may exclude colors. From the empirical point of view, such a demand obstructs the application of the irrelevant vertex technique. Moreover, we may have more solid evidence of this by picking a typical example of such a problem. In Subsection C.2, we present a colored variant of the Topological Minor Containment problem, namely the Monochromatic Path Topological Minor problem that we prove (Theorem 6) that is W[1]-hard on planar graphs.

A.2 Linkability problems

We now consider families of problems expressible by some ϕ k = ∀x ψ(x) ∈ FOL+SDP. Such problems involve disjoint path queries for every choice of terminals in the graph.

Unordered Linkability problems. Given a graph G, a set R ⊆ V (G), and a k ∈ N, we say that R is k-cyclable in G if every k vertices of R belong in some cycle of G (see [START_REF] Robert | Cycles through 23 vertices in 3-connected cubic planar graphs[END_REF][START_REF] Andrew | In abstrakten graphen vorhandene vollständige 4-graphen und ihre unterteilungen[END_REF][START_REF] Flandrin | A generalization of Dirac's Theorem on cycles through k vertices in k-connected graphs[END_REF][START_REF] Michael | A nine vertex theorem for 3-connected claw-free graphs[END_REF][START_REF] Watkins | Cycles and connectivity in graphs[END_REF] for the combinatorial properties of k-cyclable sets). The Cyclability problem asks, given a triple G, R, and k as above, whether R is k-cyclable in G. The algorithmic properties of Cyclability have been studied in [START_REF] Golovach | The parameterized complexity of graph cyclability[END_REF] where it was proven that the standard parametrization of Cyclability is FPT for planar graphs, while the general problem is co-W[1]-hard.

For this, given a graph H, we say that R is H-linkable if for every subset S ∈ R k there is a P ∈ S 2 and a collection of internally vertex disjoint paths in G between the pairs in P that, when contracted to single edges, give a graph that is isomorphic to H. We now consider the following problem.

Unordered Linkability

Input: a graph G, R ⊆ V (G), and a graph H where k = |H|. Question: is R H-linkable in G?

Notice that above problem is expressible by a sentence ϕ H = ∀x ψ(x), where ψ consists of k! disjunctions of the dp |E(H)| predicate. Moreover, when H is a cycle of k vertices the above problem yields the Cyclability problem, that is already co-W[1]-hard. Theorem 1 automatically implies that the standard parameterization of Unordered Linkability is FPT, when restricted to graphs of bounded Hadwiger number.

Ordered Linkability problems. Let G be a graph and let R ⊆ V (G). Given a k ∈ N we say that R is k-linked in G if for every (ordered) set {s 1 , . . . , s k , t 1 , . . . , t k } of 2k distinct vertices in R there are k vertex disjoint paths in G joining the pairs (s i , t i ), i ∈ [k]. This notion has introduced by [START_REF] Watkins | On the existence of certain disjoint arcs in graphs[END_REF] in the late 60s and its graph-theoretical properties have been extensively studied in [START_REF] Bollobás | Highly linked graphs[END_REF][START_REF] Egawa | Vertex-disjoint cycles containing specified edges[END_REF][START_REF] Jung | Eine verallgemeinerung desn-fachen zusammenhangs für graphen[END_REF][START_REF] Kawarabayashi | On sufficient degree conditions for a graph to be k-linked[END_REF][START_REF] Larman | On the existence of certain configurations within graphs and the 1-skeletons of polytopes[END_REF][START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF]. For instance, Thomas and Wollan proved in [START_REF] Thomas | An improved linear edge bound for graph linkages[END_REF] that if a graph G is 10k-connected, then V (G) is k-linked in G. This notion has been extended to the one of a H-linked set as follows: given some graph H with V (H) = {x 1 , . . . , x k }, we say that G is H-linked in R if, for every sequence v 1 , . . . , v k of vertices in R there is a P ∈ {v 1 ,...,v k } 2 and a collection of internally vertex disjoint paths in G between the pairs in P that, when contracted to single edges, give a graph with vertex set S that is isomorphic to H via the isomorphism that maps x i to v i , i ∈ [k]. The combinatorics of H-linked sets has been studied in [73, [START_REF] Ferrara | On H-linked graphs[END_REF][START_REF] Gould | Subdivision extendibility[END_REF][START_REF] Gould | On minimum degree implying that a graph is h-linked[END_REF][START_REF] Kostochka | An extremal problem for h-linked graphs[END_REF]. However, to our knowledge, nothing is known about the algorithmic properties of k-linked sets or the more general concept of H-linked sets. For this, we consider the following general problem.

Ordered Linkability

Input: a graph G, R ⊆ V (G), and a graph H where k = |H|. Question: is R H-linked in G?
It is easy to verify that the above problem is expressible by a sentence ϕ H = ∀x ψ(x), for some suitable choice of the quantification-free formula ψ. In Subsection C.1 we prove that the Ordered Linkability problem, even for the case where H is the disjoint union of k edges, is not FPT, unless FPT = W[1] (Theorem 5). Theorem 1 automatically implies that the standard parameterization of Ordered Linkability is FPT, when restricted to graphs of bounded Hadwiger number. express the replacement action, we define φ to be the formula obtained from ϕ after "forgetting" all edges between v 1 , . . . , v k (" (i,j)∈( [k]

2 ) (x = v i ∨ y = v j )") and after "adding" all edges given by the replacement action L, i.e., for each graph H ∈ H k , if H = µ -1 (G), then "add" the edges of µ(L(µ -1 (G))) in G. This is expressed using the formula " H∈H k

(i,j)∈E(H) (x = v i ∧ y = v j ) =⇒ (i,j)∈E(L(H)) (x = v i ∧y = v j ) ".
Additionally, in order to deal with disjoint paths that pass through v 1 , . . . , v k , we use the trick in Subsection A.4 to replace the atomic formulas (s)dp(s 1 , t 1 , . . . , s t , t t ). For this reason, we define the formula φ as a modified version of ϕ from Subsection A.4 by only replacing each atomic formula ζ = (x, y) by x = y and each atomic formula ζ E (x, y) (even the ones that appear in the "translation" of the atomic formulas (s)dp) by ξ E (x, y). Observe that if ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP), then ξ k ∈ FOL+DP (resp. ξ k ∈ FOL+SDP).

According to the above, if ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP), then L-ϕ-Replacement is FPT on graphs of bounded Hadwiger number (resp. bounded genus). Again in case where the models of ϕ have bounded Hadwiger number then we obtain problems of Category A that belong FPT in general and this already includes the results of [START_REF] Fedor | Modification to Planarity is Fixed Parameter Tractable[END_REF] where the target property was planarity. In fact using the above setting we may extend the definition of replacement actions so to permit the substitution of subgraphs of the input graph with new graphs of different (but still bounded) sizes. This would make it possible to define more flexible types of modifications such as edge contractions or Δ-Y transformations.

A.6 Elimination distance problems

Given a graph G, we use cc(G) to denote the connected components of G. We say that a graph class is non-trivial if it contains at least one non-empty graph and does not contain all graphs. Given a graph class G, we define the connected closure of G as

C(G) = {G | ∀C ∈ cc(G), C ∈ G}. Also, we use A(G) to denote the set {G | ∃v ∈ V (G)G \ v ∈ G}.
Let G be a non-trivial graph class. We say that a graph G has elimination distance at most k to G if

G ∈ k times C(A(• • • C(A(C(G))))).
The elimination distance from a graph class was defined by Bulian and Dawar in [START_REF] Bulian | Graph isomorphism parameterized by elimination distance to bounded degree[END_REF] as an alternative graph modification measure (see [START_REF] Agrawal | Elimination distance to topological-minor-free graphs is FPT[END_REF][START_REF] Agrawal | Deleting, eliminating and decomposing to hereditary classes are all fpt-equivalent[END_REF][START_REF] Agrawal | An FPT Algorithm for Elimination Distance to Bounded Degree Graphs[END_REF][START_REF] Agrawal | On the parameterized complexity of clique elimination distance[END_REF][START_REF] Eva-Maria | Elimination Distances, Blocking Sets, and Kernels for Vertex Cover[END_REF][START_REF] Bart | FPT algorithms to compute the elimination distance to bipartite graphs and more[END_REF][START_REF] Bart | Vertex deletion parameterized by elimination distance and even less[END_REF][START_REF] Lindermayr | Elimination distance to bounded degree on planar graphs[END_REF] for algorithmic results concerning elimination distance). Given a ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP) we define the following problem: ϕ-Elimination distance Input: a graph G and a k ∈ N. Question: is the elimination distance of G from Mod(ϕ) at most k?

Bulian and Dawar in [START_REF] Bulian | Fixed-parameter tractable distances to sparse graph classes[END_REF] considered the above problem for the case where ϕ expresses the minor-exclusion of some finite set of graphs and they proved that this problem is (constructively) FPT. In [START_REF] Fedor | Parameterized complexity of elimination distance to first-order logic properties[END_REF] considered ϕ-Elimination distance when ϕ ∈ FOL and proved that for particular instantiations of ϕ the problem, parameterized by k, is W[2]-hard. According to the recent metaalgorithmic results in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF], when ϕ ∈FOL+conn, ϕ-Elimination distance is FPT for graphs of bounded Hajós number (see [START_REF] Schirrmacher | First-Order Logic with Connectivity Operators[END_REF]). According to our results if ϕ ∈ FOL+SDP (resp. ϕ ∈ FOL+DP), then ϕ-Elimination distance is FPT on graphs of bounded Hadwiger number (resp. bounded genus).

The problem ϕ-Block Elimination Distance. Another parameter similar to elimination distance is the block elimination distance, introduced in [START_REF] Öznur | Block elimination distance[END_REF], that is obtained if we replace the connected closure operator C in the above definition by the operator B, defined as

B(G) = {G | ∀B ∈ bc(G), B ∈ B},
where bc(G) is the set of all blocks of G. Similar to ϕ-Elimination distance, we can define the problem ϕ-Block Elimination Distance. According to our results, if ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP), then ϕ-Block Elimination Distance is FPT on graphs of bounded Hadwiger number (resp. bounded genus). We remark, that when ϕ ∈FOL+conn, ϕ-Elimination distance is FPT for graphs of bounded Hajós number because of the results in [START_REF] Pilipczuk | Algorithms and data structures for first-order logic with connectivity under vertex failures[END_REF].

A.7 Reconfiguration problems

Intuitively, reconfiguration problems ask, given two feasible solutions S and T of a problem, whether there is a step-by-step transformation between S and T where all intermediate sets are also feasible solutions.

Reconfiguration sequences. Let ϕ be a sentence that is satisfied in structures of the form (G, S), i.e., structures of the colored-graph vocabulary {E, S}. A sequence S 1 , . . . , S , ∈ N of subsets of V (G) is called a ϕ-reconfiguration sequence if

• for every i ∈ [ ], (G, S i ) |= ϕ and • for every i ∈ [ ], there is a v ∈ S i and a u ∈ V (G) \ S i such that S i+1 = (S i \ {v}) ∪ {u}.

We call the lenght of the ϕ-reconfiguration sequence.

Given a ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP), whose models are of the form (G, S), we define the following problem: ϕ-Reconfiguration Input: a graph G, two sets S, T ⊆ V (G), and an ∈ N. Question: is there a ϕ-reconfiguration sequence S, . . . , T of length at most ? Reconfiguration problems have received a lot of attention in the literature [START_REF] Bonsma | Finding paths between graph colourings: Pspacecompleteness and superpolynomial distances[END_REF][START_REF] Bousquet | A survey on the parameterized complexity of the independent set and (connected) dominating set reconfiguration problems[END_REF][START_REF] Gopalan | The connectivity of boolean satisfiability: Computational and structural dichotomies[END_REF][START_REF] Hearn | Pspace-completeness of sliding-block puzzles and other problems through the nondeterministic constraint logic model of computation[END_REF][START_REF] Van Den | The complexity of change[END_REF][START_REF] Ito | On the complexity of reconfiguration problems[END_REF][START_REF] Ito | Reconfiguration of list edge-colorings in a graph[END_REF][START_REF] Lokshtanov | Reconfiguration on sparse graphs[END_REF][START_REF] Lokshtanov | On the parameterized complexity of reconfiguration of connected dominating sets[END_REF][START_REF] Amer | On the parameterized complexity of reconfiguration problems[END_REF][START_REF] Amer | On the parameterized complexity of reconfiguration problems[END_REF][START_REF] Mouawad | On Reconfiguration Problems: Structure and Tractability[END_REF][START_REF] Mynhardt | Reconfiguration of colourings and dominating sets in graphs: a survey[END_REF][START_REF] Nishimura | Introduction to reconfiguration[END_REF][START_REF] Siebertz | Reconfiguration on nowhere dense graph classes[END_REF]). A vibrant branch of research on reconfiguration problems deals with other reconfiguration models (apart from removing/adding vertices) like token sliding, (perfect) matching flipping, spanning tree flipping [11, 12, 16, 24, 25, 39-42, 59, 74, 211]. Also, the tractability of reconfiguration problems has been studied under different structural parameterizations of the input graph [START_REF] Belmonte | Independent set reconfiguration parameterized by modular-width[END_REF][START_REF] Hans | Parameterized problems complete for nondeterministic FPT time and logarithmic space[END_REF][START_REF] Hans | Parameterized Complexities of Dominating and Independent Set Reconfiguration[END_REF][START_REF] Amer | Vertex cover reconfiguration and beyond[END_REF][START_REF] Wrochna | Reconfiguration in bounded bandwidth and tree-depth[END_REF].

Known AMTs for reconfiguration problems. Also, there are some konwn algorithmic metatheorems for reconfiguration problems. In fact, [START_REF] Amer | Reconfiguration over tree decompositions[END_REF] proved that for every ϕ ∈ MSO 2 , the problem ϕ-Reconfiguration is FPT parameterized by tw + + |ϕ|, where tw is the treewidth of the input graph. Also, their framework can be used to derive an FPT algorithm for the parameterization of the problem ϕ-Reconfiguration for ϕ ∈ MSO 1 by + cw + |ϕ|, where cw is the cliquewidth of the input graph. For formulas ϕ ∈ MSOL, in [START_REF] Gima | Algorithmic meta-theorems for combinatorial reconfiguration revisited[END_REF], they considered two parameterizations of ϕ-Reconfiguration: the first is by the neighborhood diversity of the input graph and the second is, when restricted to feasible solutions of size k, by the treewidth of the input graph and k. For these two parameterized (meta)problems, they give an FPT algorithm.

For ϕ ∈ FOL, the variant of ϕ-Reconfiguration where the size of all sets in the reconfiguration sequence is k, is FPT parameterized by + k + |ϕ| on nowhere dense classes [START_REF] Lokshtanov | Reconfiguration on sparse graphs[END_REF]. This result also holds for any reconfiguration model (for example, token sliding) that can be expressed by a formula in FOL.

Expressing ϕ-Reconfiguration. Let ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP). We claim that there is a sentence φ ∈ FOL+DP ( φ ∈ FOL+SDP) such that (G, S, T, ) is a yes-instance of ϕ-Reconfiguration if and only if (G, S, T ) |= φ . To see this, first, we consider the formula ψ (0) S (z) = (z ∈ S) and, for every i ∈ [ -1], we consider the formula ψ (i) S (x 1 , y 1 , . . . , x i , y i , z) = ψ (i-1) S (x 1 , y 1 , . . . , x i-1 , y i-1 , z) ∧ z = x i ∨ z = y i .

Intuitively, for every i ∈ N, given a graph G, a set S ⊆ V (G) that interprets S, and some vertices x 1 , y 1 , . . . , x i , y i , z ∈ V (G) that interpret the variables x 1 , y 1 , . . . , x i , y i , z, ψ (i) S (x 1 , y 1 , . . . , x i , y i , z) expresses that z ∈ S i , where S 0 = S and for every j ∈ [i], S j = (S j-1 \ {x j }) ∪ {y j }.

Also, for every i ∈ N, we define ϕ (i) S (x 1 , y 1 , . . . , x i , y i ) to be the formula obtained from ϕ after replacing each atomic term x ∈ S with the formula ψ (i) S (x 1 , y 1 , . . . , x i , y i , x). Intuitively, the formula ϕ (i) S demands that the variables of ϕ are picked inside the set S i , instead of the set S, where S i is defined as above. We define φ as follows.

φ = ∃v 1 , u 1 , . . . , v , u i∈[ ] ψ (i-1) S (v 1 , u 1 , . . . , v i-1 , u i-1 , v i ) ∧ ¬ψ (i-1) S (v 1 , u 1 , . . . , v i-1 , u i-1 , u i ) ∧ ϕ (i) S (v 1 , u 1 , . . . , v i , u i ).
Observe that if ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP), then φ ∈ FOL+DP (resp. φ ∈ FOL+SDP). According to our results, if ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP), then ϕ-Reconfiguration is FPT, parameterized by and |ϕ|, on graphs of bounded Hadwiger number (resp. bounded genus).

A.8 Planarizer game

We would like to finish this section with a new problem that we consider worth mentioning here. We call it Planarizer Game and it is played by two players, the blocker and the planarizer. The two players play in rounds. In each round each player places tokens on the vertices of the graph and the blocker plays first. None of the players can move his/her token on a vertex that is already occupied by a token. The planarizer wins if the removal from G of the vertices that are occupied by his/her tokens yields a planar graph. The Planarizer Game problem asks, given a graph G and a non-negative integer k, whether the planarizer has a victory strategy against the blocker that uses at most k rounds. To prove that Planarizer Game is NP-hard we conside the Edge Planarizer problem asking, give a graph G and a non-negative integer k, whether there is set of at most k edges of G whose removal produces a planar graph. In [START_REF] Faria | On the complexity of the approximation of nonplanarity parameters for cubic graphs[END_REF], Fariaa, Herrera de Figueiredo, Mendonça, proved that this problem is NP-hard for graphs of maximum degree three. We reduce this restricted version of Edge Planarizer to Planarizer Game as follows.

Let (G, k) be an input of Edge Planarizer. We transform (G, k) to an input (G , k) of Planarizer Game by replacing each edge by a path of length k and by removing every vertex v of degree three and making N G (v) a clique (i.e., a triangle). Then (G, k) is a yes instance of Edge Planarizer iff (G , k) is a yes instance of Planarizer Game because each edge-choice of Edge Planarizer corresponds to a choice of a vertex of a joining path and the length of joining paths is big enough to "neutralize" the potential of the blocker during the game.

(4) for every cell c ∈ C(Γ), V (σ(c)) ∩ c ∈C(Γ)\{c} V (σ(c )) ⊆ π(c), and

(5) π(N (Γ) ∩ bd(∆)) = V (Ω), such that the points in N (Γ) ∩ bd(∆) appear in bd(∆) in the same ordering as their images, via π, in Ω.

Similarly, we define annulus (Ω 1 , Ω 2 )-renditions as follows. Let G be a graph and let X 1 , X 2 be two subsets of V (G), and let Ω 1 (resp. Ω 2 ) be a cyclic permutation of X 1 (resp. X 2 ). By an (Ω 1 , Ω 2 )-rendition of G we mean a triple (Γ, σ, π), where (Γ, σ, π), is defined as for disk Ω-renditions but Γ is a ∆-painting for some closed annulus ∆ (instead of a closed disk) and as for item [START_REF] Agrawal | Deleting, eliminating and decomposing to hereditary classes are all fpt-equivalent[END_REF], π(N (Γ) ∩ bd(∆)) = X 1 ∪ X 2 , such that, if bd(∆) = B 1 ∪ B 2 , then the points in N (Γ) ∩ B i appear in B i in the same ordering as their images, via π, in Ω i , for i ∈ {1, 2}.

B.3 Flatness pairs

In this subsection we define the notion of a flat wall, originating in the work of Robertson and Seymour [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF] and later used in [START_REF] Kawarabayashi | A new proof of the flat wall theorem[END_REF]. Here, we define flat walls as in [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF].

Flat walls. Let G be a graph and let W be an r-wall of G, for some odd integer r ≥ 3. We say that a pair (P, C) ⊆ D(W ) × D(W ) is a choice of pegs and corners for W if W is the subdivision of an elementary r-wall W where P and C are the pegs and the corners of W , respectively (clearly, C ⊆ P ). To get more intuition, notice that a wall W can occur in several ways from the elementary wall W , depending on the way the vertices in the perimeter of W are subdivided. Each of them gives a different selection (P, C) of pegs and corners of W.

We say that W is a flat r-wall of G if there is a separation (X, Y ) of G and a choice (P, C) of pegs and corners for W such that: We say that W is a flat wall of G if it is a flat r-wall for some odd integer r ≥ 3.

Flatness pairs. Given the above, we say that the choice of the 7-tuple R = (X, Y, P, C, Γ, σ, π) certifies that W is a flat wall of G. We call the pair (W, R) a flatness pair of G and define the height of the pair (W, R) to be the height of W. We use the term cell of R in order to refer to the cells of Γ.

We call the graph G[Y ] the R-compass of W in G, denoted by Compass R (W ). It is easy to see that there is a connected component of Compass R (W ) that contains the wall W as a subgraph. We can assume that Compass R (W ) is connected, updating R by removing from Y the vertices of all the connected components of Compass R (W ) except of the one that contains W and including them in X (Γ, σ, π can also be easily modified according to the removal of the aforementioned vertices from Y ). We define the flaps of the wall W in R as flaps R (W ) := {σ(c) | c ∈ C(Γ)}. Given a flap F ∈ flaps R (W ), we define its base as ∂F := V (F ) ∩ π(N (Γ)).

Flat railed annuli. Let G be a graph and let A be an (r, q)-railed annulus of G, for some odd integer r ≥ 3 and q ∈ N ≥3 . We say that A is a flat (r, q)-railed annulus of G if there are two laminar separations (X 1 , Y 1 ), (X 2 , Y 2 ) of G, a set Z 1 of degree-two vertices in V (C 1 ), and a set Z 2 of degree-two vertices in V (C 2 ) such that: Claim 4. Let H be a complete graph with k = 4r + 1 vertices for r ≥ 1. Then there is a partition of E(H) into = (4r + 1)r pairs {e i , e i } for i ∈ [ ] such that e i and e i have no common endpoints.

Proof of Claim 4. The proof is by induction on r. If r = 1, then the partition is shown in Figure 12 (a). If r ≥ 2, then we select four arbitrary vertices v 1 , v 2 , v 3 , v 4 of H and partition the edges incident to them using the pattern shown in Figure 12 (b). The remaining edges are partitioned into pairs using the inductive assumption. Suppose that G contains a clique H of size k as a subgraph. By Claim 4, the set of edges of H can be partitioned into = (4r + 1)r = k -1 pairs {e i , e i } for i ∈ [ ] such that e i and e i have no common endpoints. Let e i = {x i , y i } and e i = {x i , y i } for i ∈ [ ]. We consider the vertices s i = e x i y i and t i = e x i y i of G for i ∈ [ ]. We also define s k = w x and t k = w y for arbitrary distinct x, y ∈ V (H). The k -tuples (s 1 , . . . , s k ) and (t 1 , . . . , t k ) are disjoint and consist of distinct vertices of R. Because e i and e i have no common endpoints for every i ∈ [ ], any path between s i and t i in G contains two edges incident to s i and t i , respectively. Because x and y are distinct, the same holds for any path in G between s k and t k . Suppose that G has vertex-disjoint paths between s i and t i , for i ∈ [k ]. Then the edges of the paths incident to the vertices s 1 , . . . , s k and t 1 , . . . , t k should form a matching. However, N G ({s 1 , . . . , s k } ∪ {t 1 , . . . , t k }) = x∈V (H) S x and | x∈V (H) S x | = k(k -1)/2 < 2k . Therefore, by Hall's theorem [START_REF] Hall | An existence theorem for Latin squares[END_REF], G has no matching saturating the vertices of {s 1 , . . . , s k } ∪ {t 1 , . . . , t k }, i.e., G has no matching M such that the set of the endpoints of the edges in M contains {s 1 , . . . , s k } ∪ {t 1 , . . . , t k }). Thus, there are no vertex-disjoint paths between s i and t i for i ∈ [k ] in G . Now we show that if G has no clique with at least k/5 vertices, then for all pairs of disjoint k -tuples of distinct vertices (s 1 , . . . , s k ) and (t 1 , . . . , t k ), the graph G has vertex-disjoint paths between s i and t i , for all i ∈ [k ]. Consider arbitrary (s 1 , . . . , s k ) and (t 1 , . . . , t k ) and set X = {s 1 , . . . , s k } ∪ {t 1 , . . . , t k }. We prove the following claim.

Claim 5. The graph G has a matching M saturating every vertex of X.

Proof of Claim 5. We set Y = X ∩ L. For every x ∈ V (G), let S x ⊂ S x be an arbitrary subset of S x of size (k -1)/2 -1. We define S = x∈V (G) S x . We claim that H = G[Y ∪ S ] has a matching M saturating every vertex of Y . Because Y is an independent set, we can apply Hall's theorem [START_REF] Hall | An existence theorem for Latin squares[END_REF] and observe that it is sufficient to show that for every Z ⊆ Y , Consider a (kD × kD)-grid Γ. Also define {Γ i,j | (i, j) ∈ [k] 2 } to be the (unique) collection of k 2 pairwise vertex disjoint (D × D)-grids of Γ. We define the black and green color sets, namely B and C so that for every (i, j) ∈ [k] 2 we include, for every pair (x, y) ∈ M (i, j), the intersection vertex of the x-th column and the y-th row of Γ i,j in the set B (if i + j = 0 (mod 2)) or in the set C (if i + j = 1 (mod 2)).

The graph G is obtained by subdividing every vertex of Γ once. Clearly, G consists of kD vertical paths and kD horizontal paths. The orange and the turquoise color sets, namely O anf T are defined so that O contains every vertex of a vertical path and T contains every vertex of an horizontal path. We now consider the (k × k)-grid H and λ is a proper two coloring of H in black and green.

It now remains to see that (D, k, M ) is a yes-instance of Grid Tiling if and only if the tuple (G, B, C, O, T, H, λ) is a yes-instance of Monochromatic Path Topological Minor. Just observe that the orange (resp. turquoise) colors force all vertical (resp. horizontal) paths of H to be mapped to vertical (resp. horizontal) paths and that the black and green colors force each edge of H to be mapped to a path in some neighboring Γ i,j 's joining a black vertex and a green vertex of G.

Figure 5 :

 5 Figure 5: An illustration of a partially annulus-embedded graph.

Figure 6 :

 6 Figure 6: An example of a ∆-embedded railed annulus A and a linkage L (depicted in red) that is ∆-avoiding.

  B⊆[l] d∈[k] (I 1 ,...,I d )∈P d (B) all injective functions ρ:{I 1 ,...,I d }→[k]

Observation 8 .

 8 Let τ be a colored-graph vocabulary. For every ϕ ∈ FOL[τ +dp], every l ∈ N, and every collection c of l constant symbols, ϕ l ∈ FOL[τ c + dp].

Lemma 3 .

 3 Let τ be a colored-graph vocabulary, let l ∈ N, and let c be a collection of l constant symbols. For every ϕ ∈ FOL[τ +dp], every τ -structure G, and every apex-tuple a of G of size l, it holds that G |= ϕ ⇐⇒ ap c (G, a) |= ϕ l (where c is interpreted as a).

Figure 8 :

 8 Figure 8: An illustration of some vertices of a graph which contains a flat railed annulus A = (C, P), colored with respect to their stamps. The white-colored vertices have w-stamp equal to (0, •), the blue-colored vertices have w-stamp equal to (1, •), the red-colored vertices have w-stamp equal to (0, •), and the green-colored vertices have w-stamp equal to (1, •).

Figure 9 :

 9 Figure 9: An illustration of the railed annuli A w, for every w ∈ {0, 1} 3 , of a railed annulus A. For each w ∈ {0, 1} 3 , the yellow vertices inside A w are the boundary vertices of G (t) w .

Claim 3 .

 3 For every i ∈ [0, d] and every β ∈ G (d,h)

Lemma 6 .

 6 There is a function f 7 : N → N and an algorithm that, given d, r, tw ∈ N, where r ∈ [d -1], an n-vertex colored graph G, an apex-tuple a of G of size l, a well-aligned (f 5 (d), )railed annulus flatness pair (A, R) of G \ V (a), where tw(G[Y 2 ]) ≤ tw, a set Z ⊆ Y 1 , and a set R ⊆ V (G), outputs, in time O d,tw (n), a set R ⊆ V (G) such that R ⊆ R, |R ∩ Z| ≤ f 7 (d), and partial-sig d r (ap c ((G, R), a)) = partial-sig d r (ap c ((G, R ), a)).

  and partial-sig d r (ap c ((G, R), a)) = partial-sig d r (ap c ((G, R ), a)). By using Proposition 6, we can compute, in linear time, a q-subwall W of W such that V (Influence R (W )) ⊆ Y 1 and R ∩ V (Influence R (W )) = ∅. Then, by applying the algorithm of Proposition 7 we compute, in linear time, a W

•

  V (W ) ⊆ Y, • P ⊆ X ∩ Y ⊆ V (D(W )),and • if Ω is the cyclic ordering of the vertices X ∩ Y as they appear in D(W ), then there exists an Ω-rendition (Γ, σ, π) of G[Y ].

Figure 12 :

 12 Figure 12: Pairing edges of H; the edges incident to v 3 and v 4 are not shown and are partitioned in pairs in the same pattern as the edges incident to v 1 and v 2 .

  |N H (Z)| ≥ |Z|. Consider a set Z ⊆ Y . Let F = {{x, y} ∈ E(G) : e xy ∈ Z} and let U be the set of vertices of G incident to the edges of F .

Figure 13 :

 13 Figure 13: An example of the reduction of Theorem 6. On the left an instance of Grid Tiling is depicted where D = 4 and k = 3. On the right the corresponding instance (G, B, C, O, T , H, λ) of Monochromatic Path Topological Minor is depicted, where H is the (k × k)-grid. The solution for the Grid Tiling, depicted by the red pairs, corresponds to a realization of the (k × k)grid on the right, depicted by the (long) orange and blue rectangles.

Let t = (x1, . . . , x l ) ∈ N l and f, g : N → N. We adopt the notation f (n) = Ot(g(n)) in order to denote that there exists a computable function :N l → N such that f (n) = O( (t) • g(n)).

More generally, we say that a computational problem, parameterized by k, is FPT (Fixed Parameter Tractable) when it admits an algorithm running in O k (n O(1) ) time. We assume that the reader is familiar with the basic concepts of parameterized algorithms and parameterized complexity classes -see[START_REF] Cygan | Parameterized Algorithms[END_REF][START_REF] Flum | Parameterized Complexity Theory[END_REF][START_REF] Niedermeier | Invitation to Fixed-Parameter Algorithms[END_REF].

The Hajós number is the maximum h for which G contains a subivision of K h as a subgraph.

In the definition of FOL+DP we insist that the paths are disjoint while in[START_REF] Schirrmacher | First-Order Logic with Connectivity Operators[END_REF] paths are required to be internally disjoint (certainly, these two variants define equivalent formulas). We insist on the "complete disjointness" as this permits us to see FOL+DP as a special case of the more general FOL+SDP that we introduce in this paper.

Given two graphs G and H, H is a minor of G if G contains a contraction of H as a subgraph.

We stress that we allow constant symbols to be interpreted as the element ␣, where ␣ is an element that is not in V (A). Throughout this paper, we assume that the universe of every given structure is extended by adding the extra element ␣, while all relation symbols are interpreted as tuples of elements of V (A), not containing ␣. Moreover, we assume that for every formula that we consider, quantified first-order variables are interpreted as elements of the original universe of the structure (and not ␣).

Acknowledgements. We would like to thank Anuj Dawar and the anonymous reviewers of previous versions of this paper. Their comments led to an improvement of the presentation of our results.

Supported by the Research Council of Norway via the project BWCA (314528). Supported by the ANR projects DEMOGRAPH (ANR-16-CE40-0028), ESIGMA (ANR-17-CE23-0010), and the French-German Collaboration ANR/DFG Project UTMA (ANR-20-CE92-0027).

See Figure 10 for a simplified visualization of the statement of Lemma 5. Proof. Let F be a colored graph, let R ⊆ V (F), and let ξ be an outer-compatibility function of (D, R) and (F, R ).

Given that R = (X 1 , Y 1 , X 2 , Y 2 , Z 1 , Z 2 , Γ, σ, π), we set R = ( X1 , Ỹ1 , X2 , Ỹ2 , Z 1 , Z 2 , Γ, σ, π) and R = ( X 1 , Ỹ1 , X 2 , Ỹ2 , Z 1 , Z 2 , Γ, σ, π), where • Ỹ1 (resp. Ỹ2 ) is the vertex set obtained from the union of Y 1 (resp. Y 2 ) and V (G) after identifying the vertices in (X 1 ∩ Y 1 ) ∪ V (a) with their images via η,

• Ỹ 1 (resp. Ỹ 2 ) is the vertex set obtained from the union of Y 1 (resp. Y 2 ) and V (G ) after identifying the vertices in (X 1 ∩ Y 1 ) ∪ V (a) with their images via η , and • X1 (resp. X2 ) is the vertex set obtained from the union of X 1 (resp. X 2 ) and V (F) after identifying the vertices in (X 2 ∩ Y 2 ) ∪ V (a) with their images via ξ.

Observe that (A, R) is a railed annulus flatness pair of (G ⊕ η D ⊕ ξ F) \ V (a) and (A, R ) is a railed annulus flatness pair of (G ⊕ η D ⊕ ξ F) \ V (a).

We now consider the τ c -structures ap c (G ⊕ η D ⊕ ξ F, a) and ap c (G ⊕ η D ⊕ ξ F, a). Note that (A, R) is also a railed annulus flatness pair of ap c (G ⊕ η D ⊕ ξ F, a) \ V (a). Also, since in Proof of Claim 3. Let i ∈ [0, d]. Let t 0 , . . . , t i ∈ Paths(T ), let (v 1 , . . . , v i ) = (λ(t 1 ), . . . , λ(t i )). We will prove that there is a (t 1 , . . . , t i ) ∈ Paths(T ) such that for every (t i+1 , . . . , t d ) ∈ Paths(T ), where t i+1 ∈ children T (t i ), there is a (t i+1 , . . . , t d ) ∈ Paths(T ), where t i+1 ∈ children T (t i ), such that sig 0 r (H, R, a, λ(t 1 ), . . . , λ(t d )) = sig 0 r (H , R , a, λ (t 1 ), . . . , λ (t d )).

For every j ∈ [i], let (w j , ω j ) = stamp w 1 ...w j-1 (v j ). For every j ∈ [i], we set

Since partial-sig d r (ap c ((G, R) ⊕ η (D, R), a)) = partial-sig d r (ap c ((G , R ) ⊕ η (D, R), a)), there is a t i ∈ D i (T ), such that if t 0 , . . . , t i ∈ Paths(T ) and (u 1 , . . . , u i ) = (λ (t 1 ), . . . , λ (t i )), then it holds that trace(v 1 , . . . , v i ) = trace(u 1 , . . . , u i ) and

where for every j

, where for each j ∈ [i + 1, r], v j ∈ R. For every j ∈ [i + 1, d], let (w j , ω j ) = stamp w 1 ...w j-1 (v j ). For every j ∈ [i + 1, d], we set

Therefore, for every j ∈ [i+1, r], v • j ∈ Rw 1 ...w j ∪{␣} and for every j ∈ [r+1, d], v • j ∈ V (H) w 1 ...w j ∪{␣}. Following [START_REF] Baste | Hitting minors on bounded treewidth graphs[END_REF], there are u • i+1 , . . . , u • d ∈ V (ap c ((G, R) ⊕ η (D, R), a)) ∪ {␣} where for every j ∈ [i+1, r], u • j ∈ (R ∪ R) w 1 ...w j ∪{␣}, and for every j ∈ [r+1, d], u • j ∈ V (ap c ((G, R)⊕ η (D, R), a)) w 1 ...w j ∪ {␣}, such that pattern(G w, ␣ l , v We now define a sequence of vertices u i+1 , . . . , u d ∈ V (H ), as follows:

and we aim to show that sig 0 r (H, a, v 1 , . . . , v d ) = sig 0 r (H , a, u 1 , . . . , u d ). To prove this, intuitively, we have to show that (P1)-(P5) also hold for the tuples (v 1 , . . . , v d ) and (u 1 , . . . , u d ). Keep in mind that trace

First observe that, by (P1) and by the definition of u j , j ∈ [d], the partition of [d] with respect to the equal vertices in (v 1 , . . . , v d ) is the same as the one with respect to the equal vertices in (u 1 , . . . , u d ).

Also, observe that using the definition of H and H , the fact that a is an apex-tuple of D, together with the properties (P2) and (P3), we have that, when modifiying the functions κ, δ to map the indices of (v 1 , . . . , v d ) to [l] and [h] (before they mapped the indices of (v • 1 , . . . , v • d )) and the functions κ , δ to map the indices of (u 1 , . . . , u d ) (before they mapped the indices of (u • 1 , . . . , u • d )), for every j ∈ [d], κ(j) = κ (j) and for every j ∈ [d], δ(j) = δ (j).

We next show that

implies that there is no edge neither in H nor in H between vertices indexed by I and J. Therefore, both Ind H ([d]) and Ind H ([d]) are equal to the disjoint union of Ind H (I) and Ind H (J).

We conclude the proof of the claim by showing that

Recall that, by definition,

, we follow the same arguments. We consider an (L , u 1 , . . . , u d ) ∈ Pairings(H , u 1 , . . . , u d ), we apply Lemma 4 and we obtain a

This, by (P5), implies the existence of an L ∈ Pairings(G w, v• ) such that imp( L • ) = imp(L), which, in turn, implies that there exists an

Therefore, for every i ∈ [0, d] and every β ∈ G

pat , it holds that: For every (t 0 , . . . , t i ) ∈ Paths(T ) there is a (t 0 , . . . , t i ) ∈ Paths(T ) such that for every t d ∈ L(T t i ), where (t 0 , . . . , t d ) ∈ Paths(T ),

A Problems expressible in FOL+DP and in FOL+SDP

In this section we present some (families) of parameterized problems where Theorem 1 and Theorem 2 are applicable. In all cases, we consider the standard parameterization (by the integer k of the input). Also for each (meta)-problem we comment on their general parameterized complexity status, their possible classification on the families A, B, and C, given in the introduction.

First of all observe that Disjoint Paths is the prototypical problem of this category as it is expressed by the "trivial" sentence ϕ k = dp k (s 1 , t 1 , . . . , s k , t k ). This problem is FPT because of [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF]. If instead we consider the Induced Disjoint Paths, that is ϕ k = sdp k (s 1 , t 1 , . . . , s k , t k ), then the corresponding parameterized problem becomes para-NP-hard because checking whether (G, s 1 , t 1 , s 2 , t 2 ) |= ϕ 2 is already NP-complete [START_REF] Kawarabayashi | The induced disjoint paths problem[END_REF]. More generally, we may also consider problems where the input graph is accompanied with a fixed number of colors X 1 , . . . , X z , i.e., we consider structures of the form (G, X 1 , . . . , X z ), and we may consider the more general predicates (s)dp k,λ (s 1 , t 1 , . . . , s k , t k ) equiped with a list function λ : [k] → 2 [z] , where we demand that, for every i ∈ [k], λ(i) is a subset of the set of colors of the vertices of the path between the (valuations) of s 1 and t 1 . For instance we may demand that all disjoint paths are colorful, i.e., they contain vertices of all available colors.

A.1 Graph containment problems

We first consider families of problems expressible by some ϕ k = ∃x ψ(x) ∈ FOL+SDP. Such problems are defined by some partial ordering relation on graphs. We say that H is a contraction of G if H can be obtained from G after contracting edges, H is an (induced ) minor of G if H is the contraction of an (induced) subgraph of G. Finally we say that H is an (induced ) topological minor of G if G contains a subdivision of H is an (induced) subgaph.

The general setting is the following.

- [START_REF] Grohe | Finding topological subgraphs is fixed-parameter tractable[END_REF]. In the case where is the induced minor or the induced topological minor relation, -Contrainment is definable in FOL+SDP and Theorem 2 yields that Induced Minor and Induced Topological Minor Containment are FPT on bounded genus graphs. Moreover as observed in [START_REF] Kamiński | Contraction checking in graphs on surfaces[END_REF], it is possible ro reduce the Contraction Containment problem on bounded genus graphs to Topological Minor Containment. These last three problems belong in category C because they are all NP-hard for particular instantiations of H due to the results of [START_REF] Brouwer | Contractibility and NP-completeness[END_REF][START_REF] Michael | The complexity of induced minors and related problems[END_REF][START_REF] Lévêque | Detecting induced subgraphs[END_REF][START_REF] Levin | The computational complexity of graph contractions I: Polynomially solvable and NP-complete cases[END_REF][START_REF] Levin | The computational complexity of graph contractions II: Two tough polynomially solvable cases[END_REF] (using the parameterized complexity terminology, their standard parmeterizatins are para-NP-hard). Certain rooted variants of all these problems can be also expressed by the corresponding logics if we ask that the "models" certifying each of the aforementioned relations meet certain vertices or sets of vertices (colors) of the input graph.

Clearly both Unordered Linkability and Ordered Linkability belong category B and it is an open question whether it is FPT for other graph classes more general (or different) than those of bounded Hadwiger number. Notice that we may further consider that the disjoint paths in the definition of being H-linked and H-linkable are induced paths. This would define the Induced Unordered Linkability and Induced Ordered Linkability problems whose standard parameterizations are not expected to be FPT (by easy reductions from the problems Cyclability and Ordered Linkability) and they are FPT in bounded genus graphs, because of Theorem 2.

A.3 Vertex deletion problems

We give now a wide variety of FOL+SDP-expressible problems, typically correspond to formulas of the type ϕ k = ∃x 1 ∀x 2 ψ(x 1 , x 2 ). We present below those that we consider more relevant.

Vertex deletion to exclusion. This family of problems can be seen as a natural extension of those mentioned in Subsection A.1. Let be a partial ordering relation on graphs and let F be a finite set of graphs. Given a graph G, we say that F G if for some F ∈ F it holds that F G. We define the following meta-problem.

F--Deletion

Input: a graph G and a k ∈ N. Question: is there an

Notice that the above yields the problems F-Minor-Deletion and F-Topological Minor-Deletion are expressible by some

It is easy to see that yes-instance of F-Minor-Deletion have bounded Hadwiger number, therefore it belongs in Category A. The standard parameterization of F-Minor-Deletion is known to be FPT in general because of [START_REF] Fedor | Planar F-Deletion: Approximation, Kernelization and Optimal FPT Algorithms[END_REF][START_REF] Bart | A near-optimal planarization algorithm[END_REF][START_REF] Kociumaka | Deleting vertices to graphs of bounded genus[END_REF][START_REF] Marx | Obtaining a planar graph by vertex deletion[END_REF][START_REF] Sau | Thilikos. k-apices of minor-closed graph classes. II. Parameterized algorithms[END_REF]. On the other hand, the standard parameterization of F-Topological Minor Deletion was proved to be FPT in general [START_REF] Fedor | Hitting topological minors is FPT[END_REF] and belongs to Category C, as extra machinery was used for 1st phase of the irrelevant vertex technique.

By applying Theorem 1 on bounded genus graphs and combining it with the duality trick of [START_REF] Kamiński | Contraction checking in graphs on surfaces[END_REF] it is possible to give an FPT-reduction of the standard parameterization of F-Contraction Deletion on bounded genus graphs to the standard parameterization of F-Topological Minor Deletion. Furthermore, F-Induced Minor Deletion and F-Induced Topological Minor Deletion are expressible in FOL+SDP using sdp k instead of dp k in the above expressibility argument. Therefore both parameterized problems are in FPT on graphs of bounded genus because of Theorem 2. It is easy to see that these last three parameterized problems are para-NP-hard in general, therefore they are classified in Category B.

Annotation and subset variants. Another direction is to consider Annotated F--Deletion where the input comes with an annotated set of vertices R ⊆ V (G) and we further demand that S ⊆ R. Another variant is the Subset F--Deletion where again the input comes an annotated set R of vertices but now we ask that for every Z ⊆ V (G) where F G[Z] and Z ∩ R = ∅, it holds that Z ∩ S = ∅. Intuitively, we demand that only the certificates of the containment of a graph in F that intersect R are required to be intersected by the solution S.

All results mentioned above for the five aforementioned partial relations on graphs hold also for the corresponding Annotated F--Deletion and the Subset F--Deletion meta-problems when restricted either to graphs of bounded Hadwiger number or of bounded genus. For general graphs, the Subset F-Minor-Deletion problem has been treated in [START_REF] Cygan | Subset feedback vertex set is fixed-parameter tractable[END_REF][START_REF] Ichi | Fixed-parameter tractability for the subset feedback set problem and the s-cycle packing problem[END_REF] for F = {K 3 }.

General vertex deletion. Deviating from the ∃ ∀ scheme of this subsection we wish to mention that all above problems can be seen as modification problems where we want to achieve some particular target property by removing vertices. The target property is the exclusion of some pattern graphs (the graphs in F) under some partial relation (the relation ). The application of Theorem 1 and Theorem 2 was made possible because because the -exclusion is, depending on the choice of , either FOL+DP or FOL+SDP-expressible. In fact we can see all above results as special cases of the following meta-problem defined given a ϕ ∈ FOL+SDP.

ϕ-Deletion

Input: a graph G and a k ∈ N. Question: is there an

According to Theorem 1 and Theorem 2 if ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+SDP), then ϕ-Deletion is FPT on graphs of bounded Hadwiger number (resp. bounded genus). The special case where ϕ corresponds to the property of being planar and satisfying some FOL property is treated in [START_REF] Fedor | An algorithmic meta-theorem for graph modification to planarity and FOL[END_REF].

A.4 Amalgamation problems

The input of an amalgamation problem consists of two graphs and asks for a way to identify their vertices so that the new graph satisfies some particular property. The notion of amalgamation dates back to [START_REF] Nešetřil | Amalgamation of graphs and its applications[END_REF] and its combinatorial study includes [START_REF] Gross | Genus distribution of graph amalgamations: self-pasting at root-vertices[END_REF][START_REF] Hilton | Amalgamations of connected k-factorizations[END_REF][START_REF] Leach | Hamilton decompositions of complete multipartite graphs with any 2-factor leave[END_REF][START_REF] Yang | The thickness of amalgamations and cartesian product of graphs[END_REF].

Given two graphs G 1 and G 2 we define G 1 ⊗ k G 2 as the set containing every graph obtained if for some

and a bijection σ : S 1 → S 2 we take the disjoint union of G 1 and G 2 and then identify each vertex v ∈ S 1 with σ(v). Consider the following problem, defined given a ϕ ∈ FOL+DP (ϕ ∈ FOL+SDP).

ϕ-Amalgamation

To see this, consider the sentence

where ϕ is a formula with v 1 1 , . . . , v 1 k , v 2 1 , . . . , v 2 k as free variables obtained from ϕ after replacing each of its atomic formulas as follows:

• Each atomic formula x = y, is replaced by the formula ζ = (x, y), defined as

• Each atomic formula E(x, y) is replaced by the formula ζ E (x, y), defined as

• Each atomic formula (s)dp(s replace every atomic formula of the form "y j ∈ C i " by ζ E (x i , y j ), and replace all atomic formulas x = y and E(x, y) by ζ = (x, y) and ζ E (x, y), respectively.

We make clear that we assume that the collection c in the definitions in Subsection 6.1 is replaced by

k " asks for the existence of sets S 1 (corresponding to the interpretations of v 1 1 , . . . , v 1 k ) and S 2 (corresponding to the interpretations of v 2 1 , . . . , v 2 k ) each of size k, and a bijection σ : S 1 → S 2 , given by the ordering of the variables (i.e., mapping the interpretation of

Then, to express the identification of each v ∈ S 1 to σ(v) and the satisfaction of ϕ from the graph G 1 ⊗ k G 2 , we define the formula ϕ with v 1 1 , . . . , v 1 k , v 2 1 , . . . , v 2 k as free variables. For this formula, we use the idea from Subsection 6.1 for the definition of the apex-projection of a formula, in order to deal with S 1 and S 2 separately and ask a modified version of ϕ in the resulting graph. First feature of ϕ is to consider the interpretations of v 1 i and v 2 i as the same vertex. To incorporate this, we "re-define" equality as ζ = (x, y). The respective configuration has to be done to the adjacency predicate E and all atomic formulas (s)dp(s 1 , t 1 , . . . , s t , t t ) in ϕ. For this reason, we define ζ E (x, y) in a way that, for example, v 1 i is adjacent to y adjacent if and only if v 2 i is adjacent to y. Then, each atomic formula (s)dp(s 1 , t 1 , . . . , s t , t t ) is "splitted" to the part that concerns v 1 1 , . . . , v 1 k , v 2 1 , . . . , v 2 k and the rest of the graph, and "guessing" where the supposed paths should enter or exit the sets S 1 and S 2 . This idea is the same as the one in Subsection 6.1 and for this reason we use the formula ζ (s)dp (s 1 , t 1 , . . . , s t , t t ). However, here we do not need to remove the edges between the apex-tuple and the rest of the graph, so we may just ask for adjacencies between the "apex set" and the rest of the graph. This is why we can write ζ E (x i , y j ) instead of "y j ∈ C i " and avoid using the toolbox of "apex-projection" and "backwards-translation". Also, to be consistent to the identification given by σ, we have to replace all atomic formulas x = y and E(x, y) by ζ = (x, y) and

According to the above, if ϕ ∈ FOL+DP (resp. ϕ ∈ FOL+DP), then ϕ-Amalgamation is FPT on graphs of bounded Hadwiger number (resp. bounded genus). In [START_REF] De | Graph amalgamation under logical constraints[END_REF], de Oliveira Oliveira considered, given a pattern graph H on k vertices, the alternative amalgamation operation G 1 ⊗ H G 2 where the subgraphs of G 1 and G 2 induced by S 1 and S 2 are also asked to be isomorphic to H. Clearly, this operation can also be treated by above machinery by introducing the isomorphism of G 1 [S 1 ] and G 2 [S 2 ] in the formula χ k . For this operation, de Oliveira Oliveira [START_REF] De | Graph amalgamation under logical constraints[END_REF]Theorem 4.3] proves that there is an algorithm that, given a sentence ϕ ∈ CMSOL, three (connected) graphs G 1 , G 2 , H of treewidth at most t and maximum degree at most ∆, reports whether

This result is incomparable with our results.

Note that if the models of ϕ have bounded Hadwiger number, then we define problems of Category A that are in FPT in general. As an example of such a problem we mention Planar Amalgamation.

A.5 Actions and replacements

In [START_REF] Fedor | Modification to Planarity is Fixed Parameter Tractable[END_REF] a general local graph modification framework was defined where we consider a set of ways, called actions, that locally replace small size subgraph patterns of a graph. The problem treated in [START_REF] Fedor | Modification to Planarity is Fixed Parameter Tractable[END_REF] is whether such a replacement (or a sequence of such replacements) may modify the graph so to satisfy some graph property. In [START_REF] Fedor | Modification to Planarity is Fixed Parameter Tractable[END_REF] this property was planarity (and some modifications of it). Here we will consider a way more general setting.

Replacement actions. We start with some necessary definitions. We use the notation inj([k], G) for all the injections of [k] to the set of vertices of G. A k-numbered-graph is any graph H where V (H) = [k], i.e., the vertices of H are the numbers {1, . . . , k}. We denote the set of all k-numbered graphs by H k and we set H = k∈N H k . A replacement action is any function L : H → H, where for every H ∈ H, |L(H)| = |H|, i.e., graphs in H are mapped to same-size graphs.

Let G be a graph and let

Let G be a graph and let G be an other graph where

)∪G , i.e., G G occurs if we remove from G the edges between vertices in G and then add all edges of G . Given a graph G,

, in other words, we consider the part of G that is delimited by µ and then we replace this part by its image via L.

An action L may be seen as prescribed way to locally change a graph. It might be the complementation of the edges of a subgraph G of G, their removal, or the addition of a clique on the vertices of G , or the removal of a matching from G .

We now have all ingredients we need for defining a general local replacement problem. Let L be an action and let ϕ ∈ FOL+DP (ϕ ∈ FOL+SDP). We define the following problem.

L-ϕ-Replacement

Input: a graph G and a k ∈ N. Question:

Expressing L-ϕ-Replacement. We claim that, for every action L and every sentence ϕ ∈ FOL+DP (ϕ ∈ FOL+SDP), there is a sentence

where φ is the formula obtained from ϕ of Subsection A.4, after replacing each atomic formula ζ = (x, y) by x = y, each atomic formula ζ E (x, y) by the formula

Intuitively, the sentence ξ k asks the existence of an µ ∈ inj([k], V (G)) ("∃v 1 , . . . , v k ") such that the modified graph L µ (G) satisfies ϕ. We use v 1 , . . . , v k to denote the interpretation of v 1 , . . . , v k . To According to Theorem 1 and given that yes-instances of Planarizer Game have bounded Hadwiger number, the problem belongs in Category A and, when parameterized by the number of rounds, is FPT. Of course the same result can be generalized if, instead of planarity, the planarizer pursues some other graph property whose graphs have bounded Hadwiger number (resp. genus) and is expressible in FOL+DP (resp. FOL+SDP).

B Flat walls and flat annuli framework

Here we present the framework on flat walls that was introduced in [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]. In Subsection B.1 we define walls, subwalls, and other notions related to walls. Next, in Subsection B.2, we give the definitions of renditions and paintings, that are used in Subsection B.3 to define flatness pairs. In Subsection B.3, apart from the definition of flatness pairs, we present notions like influence, regularity, and tilts.

B.1 Walls and subwalls

Dissolutions and subdivisions. Given a vertex v ∈ V (G) of degree two with neighbors u and w, we define the dissolution of v to be the operation of deleting v and, if u and w are not adjacent, adding the edge {u, w}. Given an edge e = {u, v} ∈ E(G), we define the subdivision of e to be the operation of deleting e, adding a new vertex w and making it adjacent to u and v. Given two graphs H, G, we say that H is a subdivision of G if H can be obtained from G after subdividing edges of G.

Walls. Let k, r ∈ N. The (k × r)-grid is the graph whose vertex set is [k] × [r] and two vertices (i, j) and (i , j ) are adjacent if and only if |i -i | + |j -j | = 1. An elementary r-wall, for some odd integer r ≥ 3, is the graph obtained from a (2r × r)-grid with vertices (x, y) ∈ [2r] × [r], after the removal of the "vertical" edges {(x, y), (x, y + 1)} for odd x + y, and then the removal of all vertices of degree one. Notice that, as r ≥ 3, an elementary r-wall is a planar graph that has a unique (up to topological isomorphism) embedding in the plane such that all its finite faces are incident to exactly six edges. The perimeter of an elementary r-wall is the cycle bounding its infinite face, while the cycles bounding its finite faces are called bricks. Also, the vertices in the perimeter of an elementary r-wall that have degree two are called pegs, while the vertices (1, 1), (2, r), (2r-1, 1), (2r, r) are called corners (notice that the corners are also pegs).

An r-wall is any graph W obtained from an elementary r-wall W after subdividing edges. A graph W is a wall if it is an r-wall for some odd r ≥ 3 and we refer to r as the height of W. Given a graph G, a wall of G is a subgraph of G that is a wall. We insist that, for every r-wall, the number r is always odd.

We call the vertices of degree three of a wall W 3-branch vertices. A cycle of W is a brick (resp. the perimeter ) of W if its 3-branch vertices are the vertices of a brick (resp. the perimeter) of W . We denote by C(W ) the set of all cycles of W. We use D(W ) in order to denote the perimeter of the wall W. A brick of W is internal if it is disjoint from D(W ).

Subwalls. Given an elementary r-wall W , some odd i ∈ {1, 3, . . . , 2r -1}, and i = (i + 1)/2, the i -th vertical path of W is the one whose vertices, in order of appearance, are (i, 1), (i, 2), (i + 1, 2), (i + 1, 3), (i, 3), (i, 4), (i + 1, 4), (i + 1, 5), (i, 5), . . . , (i, r -2), (i, r -1), (i + 1, r -1), (i + 1, r). Also, given some j ∈ [2, r -1] the j-th horizontal path of W is the one whose vertices, in order of appearance, are (1, j), (2, j), . . . , (2r, j).

A vertical (resp. horizontal ) path of W is one that is a subdivision of a vertical (resp. horizontal) path of W . Notice that the perimeter of an r-wall W is uniquely defined regardless of the choice of the elementary r-wall W . An r -subwall (or simply subwall ) of W is any subgraph W of W that is an r -wall, with r ≤ r, and such the vertical (resp. horizontal) paths of W are subpaths of the vertical (resp. horizontal) paths of W.

Layers. The layers of an r-wall W are recursively defined as follows. The first layer of W is its perimeter. For i = 2, . . . , (r -1)/2, the i-th layer of W is the (i -1)-th layer of the subwall W obtained from W after removing from W its perimeter and removing recursively all occurring vertices of degree one. We refer to the (r -1)/2-th layer as the inner layer of W. The central vertices of an r-wall W are its two branch vertices that do not belong to any of its layers and are connected by a path of W that does not intersect any layers of W .

Central walls. Given an r-wall W and an odd q ∈ N ≥3 where q ≤ r, we define the central qsubwall of W, denoted by W (q) , to be the q-wall obtained from W after removing its first (r -q)/2 layers and all occurring vertices of degree one. Given an h ∈

Tilts. The interior of a wall W is the graph obtained from W if we remove from it all edges of D(W ) and all vertices of D(W ) that have degree two in W. Given two walls W and W of a graph G, we say that W is a tilt of W if W and W have identical interiors.

B.2 Paintings and renditions

In this subsection we present the notions of renditions and paintings, originating in the work of Robertson and Seymour [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF]. The definitions presented here were introduced by Kawarabayashi, Thomas, and Wollan [START_REF] Kawarabayashi | A new proof of the flat wall theorem[END_REF] (see also [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]). We use the notation U (Γ) := U, N (Γ) := N and denote the set of cells of Γ by C(Γ). For convenience, we may assume that each cell of Γ is an open disk of ∆. Notice that, given a ∆-painting Γ, the pair (N (Γ), {c | c ∈ C(Γ)}) is a hypergraph whose hyperedges have cardinality at most three and Γ can be seen as a plane embedding of this hypergraph in ∆.

Disk and annulus renditions. Let G be a graph and let Ω be a cyclic permutation of a subset of V (G) that we denote by V (Ω). By a disk Ω-rendition of G we mean a triple (Γ, σ, π), where

We say that A is a flat railed annulus of G if it is a flat (r, q)-railed annulus for some odd integer r ≥ 3 and some q ∈ N ≥3 .

Railed annuli flatness pairs. Given the above, we say that the choice of the 9-tuple

We call the pair (A, R) an railed annulus flatness pair of G. We use the term cell of R in order to refer to the cells of Γ.

We call the graph

It is easy to see that there is a connected component of Compass R (A) that contains the cycles and the paths of A as subgraphs. We can assume that Compass R (A) is connected, updating R by removing from X 1 ∩ Y 2 the vertices of all the connected components of Compass R (A) except of the one that contains A and including them in X 2 (Γ, σ, π can also be easily modified according to the removal of the aforementioned vertices from X 1 ∩ Y 2 ). We define the flaps of the railed annulus

B.4 Influence of cycles in flat walls and flat railed annuli

Let G be a graph and let (W, R) be either a flatness pair or a railed annulus flatness pair of G.

A cell c of R is untidy if π(c) contains a vertex x ∈ V (W ) such that two of the edges in E(W ) that are incident to x are edges of σ(c). Notice that if c is untidy then |c| = 3. A cell c of R is tidy if it is not untidy. The notion of tidy/untidy cell as well as the notions that we present in the rest of this subsection have been introduced in [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF].

Cell classification. Given a graph G and a set X ⊆ V (G), we denote by ∂ G (X) the set of vertices in X that are adjacent to vertices of G \ X.

Given a cycle C of Compass R (W ), we say that

Notice that if c is C-perimetric, then π(c) contains two points p, q ∈ N (Γ) such that π(p) and π(q) are vertices of C where one, say P in c , of the two (π(p), π(q))-subpaths of C is a subgraph of σ(c) and the other, denoted by P out c , (π(p), π(q))-subpath contains at most one internal vertex of σ(c), which should be the (unique) vertex z in ∂σ(c) \ {π(p), π(q)}. We pick a (p, q)-arc A c in ĉ := c ∪ c such that π -1 (z) ∈ A c if and only if P in c contains the vertex z as an internal vertex. We consider the circle K C = {A c | c is a C-perimetric cell of R} and we denote by ∆ C the closed disk bounded by K C that is contained in ∆ (in the case of a railed annulus flatness pair, ∆ C the closed annulus bounded by K C and

Notice that the cells of R are partitioned into C-internal, C-perimetric, and C-external cells.

Let c be a tidy C-perimetric cell of R where |c| = 3. Notice that c\A c has two arcwise-connected components and one of them is an open disk D c that is a subset of ∆ C . If the closure D c of D c contains only two points of c then we call the cell c C-marginal. We refer the reader to [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF] for figures illustrating the above notions.

We conclude this subsection by presenting a corollary of [START_REF] Sau | Thilikos. k-apices of minor-closed graph classes. I. Bounding the obstructions[END_REF]Lemma 12]. Proposition 6. There exists a function f 17 :

and W can be constructed in linear time.

B.5 Regular flatness pairs and tilts

Notice that every wall of W (and hence every subwall of W ) is an R-normal wall of Compass R (W ). We denote by S R (W ) the set of all R-normal walls of Compass R (W ). Given a wall W ∈ S R (W ) and a cell c of R, we say that c is W -perimetric/internal/external/marginal if c is D(W )-perimetric/internal/external/marginal, respectively. We also use K W , ∆ W , influence R (W ) as shortcuts for K D(W ) , ∆ D(W ) , influence R (D(W )), respectively.

Regular flatness pairs. We call a flatness pair (W, R) of a graph G regular if none of its cells is W -external, W -marginal, or untidy.

Tilts of flatness pairs. Let (W, R) and ( W , R ) be two flatness pairs of a graph G and let W ∈ S R (W ). We assume that R = (X, Y, P, C, Γ, σ, π) and R = (X , Y , P , C , Γ , σ , π ). We say

• the set of W -internal cells of R is the same as the set of W -internal cells of R and their images via σ and σ are also the same,

The next observation follows from the third item above and the fact that the cells corresponding to flaps containing a central vertex of W are all internal (recall that the height of a wall is always at least three). Observation 14. Let (W, R) be a flatness pair of a graph G and W ∈ S R (W ). For every W -tilt ( W , R ) of (W, R), the central vertices of W belong to the vertex set of Compass R ( W ).

Also, given a regular flatness pair (W, R) of a graph G and a W ∈ S R (W ), for every W -tilt ( W , R ) of (W, R), by definition, none of its cells is W -external, W -marginal, or untidy -thus, ( W , R ) is regular. Therefore, regularity of a flatness pair is a property that its tilts "inherit".

Observation 15. If (W, R) is a regular flatness pair of a graph G, then for every W ∈ S R (W ), every W -tilt of (W, R) is also regular.

We next present one of the two main results of [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF] (see [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]Theorem 5]). Proposition 7. There exists an algorithm that given a graph G, a flatness pair (W, R) of G, and a wall W ∈ S R (W ), outputs a W -tilt of (W, R) in time O(n + m).

We conclude this subsection with the Flat Wall theorem and, in particular, the version proved by Chuzhoy [START_REF] Chuzhoy | Improved Bounds for the Flat Wall Theorem[END_REF], restated in our framework (see [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]Proposition 7]). Proposition 8. There exist two functions f 18 : N → N and f 19 : N → N, where the images of f 18 are odd numbers, such that if r ∈ N ≥3 is an odd integer, t ∈ N ≥1 , G is a graph that does not contain K t as a minor, and W is an f 18 (t) • r-wall of G, then there is a set A ⊆ V (G) with |A| ≤ f 19 (t) and a flatness pair ( W , R ) of G \ A of height r. Moreover, f 18 (t) = O(t 2 ) and f 19 (t) = t -5.

B.6 Flat walls with compasses of bounded treewidth

The following result was proved in [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]Theorem 8]. It is a version of the Flat Wall theorem, originally proved in [START_REF] Robertson | Graph minors . XIII. The disjoint paths problem[END_REF]. The proof in [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]Theorem 8] is strongly based on the proof of an improved version of the Flat Wall theorem given by of Kawarabayashi, Thomas, and Wollan [START_REF] Kawarabayashi | A new proof of the flat wall theorem[END_REF] (see also [START_REF] Chuzhoy | Improved Bounds for the Flat Wall Theorem[END_REF][START_REF] Archontia | Optimizing the graph minors weak structure theorem[END_REF]). Proposition 9. There is a function f 20 : N → N and an algorithm that receives as input a graph G, an odd integer r ≥ 3, and a t ∈ N ≥1 , and outputs, in time 2 Ot(r 2 ) • n, one of the following:

• a tree decomposition of G of width at most f 20 (t) • r, or Given graphs H and G, we say that a subgraph M of G is a minor-model of H in G if there is a partition of the vertex set of M to sets V 1 , . . . , V |V (H)| such that for every i ∈ [|V (H)|], G[V i ] is connected and the graph obtained from G after contracting the edges of each G[V i ] is isomorphic to H. Following the version of the Flat Wall theorem in [START_REF] Kawarabayashi | A new proof of the flat wall theorem[END_REF], Proposition 9 can be modified so as when it reports that K t is a minor of G, it also outputs a minor-model of K t in G.

B.7 Levelings and well-aligned flatness pairs

Let G be a graph and let (W, R) be either a flatness pair or a railed annulus flatness pair of G.

is a ∆-painting, for some closed annulus ∆. In both cases, we define the ground set of W in R to be the set ground R (W ) := π(N (Γ)) and we refer to the vertices of this set as the ground vertices of the R-compass of W in G. Notice that ground R (W ) may contain vertices of compass R (W ) that are not necessarily vertices in V (W ).

Levelings. We define the R-leveling of W in G, denoted by W R , as the bipartite graph where one part is the ground set of W in R, the other part is a set vflaps R (W ) = {v F | F ∈ flaps R (W )} containing one new vertex v F for each flap F of W in R, and, given a pair (x, F ) ∈ ground R (W ) × flaps R (W ), the set {x, v F } is an edge of W R if and only if x ∈ ∂F. We call the vertices of ground R (W ) (resp. vflaps R (W )) ground-vertices (resp. flap-vertices) of W R . Notice that the incidence graph of the plane hypergraph (N (Γ), {c | c ∈ C(Γ)}) is isomorphic to W R via an isomorphism that extends π and, moreover, bijectively corresponds cells to flap-vertices. If (W, R) is a flatness pair of G, this permits us to treat W R as a D-embedded graph, for some closed disk D, where bd(D) ∩ W R is the set X ∩ Y. If (W, R) is a railed annulus flatness pair of G, we can treat A R as a ∆-embedded graph, for some closed annulus ∆ with boundaries B 1 and B 2 , where

Representations in flatness pairs and railed annulus flatness pairs. We denote by W • the graph obtained from W if we subdivide once every edge of W that is short in compass R (W ). The graph W • is a "slightly richer variant" of W that is necessary for our definitions and proofs, namely to be able to associate every flap-vertex of an appropriate subgraph of W R (that we will denote by R W ) with a non-empty path of W • , as we proceed to formalize. We say that (W, R) is well-aligned if the following holds: W R contains as a subgraph an r-wall R W where D(R W ) = D(W R ) and W • is isomorphic to some subdivision of R W via an isomorphism that maps each ground vertex to itself. Suppose now that the flatness pair (W, R) is well-aligned. We call the wall R W in the above condition a representation of W in W R .

Proposition 10 ( [START_REF] Sau | A more accurate view of the Flat Wall Theorem[END_REF]). If a flatness pair (W, R) is regular, then it is also well-aligned. Moreover, there is an O(n)-time algorithm that, given G and such a (W, R), outputs a representation R W of W in W R .

Well-aligned railed annulus flatness pairs. We denote by A • the graph obtained from A if we subdivide once every edge in E(A) that is short in compass R (A). The graph A • is a "slightly richer variant" of A that is necessary for our definitions and proofs, namely to be able to associate every flap-vertex of an appropriate subgraph of A R (that we will denote by R A ) with a non-empty path of A • , as we proceed to formalize. We say that (A, R) is well-aligned if the following holds:

A R contains as a subgraph an (r, q)-railed annulus R A where the first (resp. last) cycle of A W is the same as the first (resp. last) cycle of A R and A • is isomorphic to some subdivision of R A via an isomorphism that maps each ground vertex to itself. Suppose now that the railed annulus flatness pair (A, R) is well-aligned. We call the wall R A in the above condition a representation of A in A R . Note that, as R A is a subgraph of A R , it is bipartite as well. The above property gives us a way to represent a flat wall by a wall of its leveling in a way that ground vertices are not altered.

Notice that both A R and its subgraph R A can be seen as ∆-embedded graphs where B 1 ∩ A R = B 1 ∩ R A and these are both subsets of the vertex set of the first cycle of A R (resp. of R A ) and B 2 ∩ A R = B 2 ∩ R A and these are both subsets of the vertex set of the last cycle of A R (resp. of R A ). This establishes a bijection δ from the set of cycles of A to the set of cycles of R A .

Let G be a graph, let (A, R) be a well-aligned railed annulus flatness pair of G. We set Leveling (A,R) (G) to be the graph obtained from G after replacing Compass R (A) with A R . We now show the next result.

Lemma 12. Let G, H be graphs and let (A, R) be a well-aligned railed annulus flatness pair of G. Also, let s

Proof. Let P 1 , . . . , P k be the paths of L in G. Since for every i ∈ [k], s i , t i / ∈ Compass R (A), no flap F ∈ flaps R (A) does contain any endpoint of P 1 , . . . , P k . Therefore, for every flap F ∈ flaps R (A) there is at most one i ∈ [k] such that P i contains some vertex of F \ ∂F . For every i ∈

For the reverse implication, notice that every collection P 1 , . . . , P k of disjoint paths in Leveling (A,R) (G) corresponds to a collection P 1 , . . . , P k of disjoint paths in G, where for every i ∈ [k], P i is obtained by replacing each vertex v F that is contained in P i by a path in F that connects the two neighbors of v F in P i (these neighbors belong to ∂F ).

C Missing complexity proofs

C.1 Hardness of Ordered Linkability

In this subsection we treat the parameterized complexity of Ordered Linkability which we restate below.

Ordered Linkability

Input: a graph G, R ⊆ V (G), and a graph H where k = |H|. Question: is R H-linked in G?

We consider the above problem in the case where the graph H is the 1-regular graph on 2k vertices. In this case, the task is, given a graph G, a subset of vertices R ⊆ V (G), and an integer k ≥ 1, decide whether for every sequence s 1 , . . . , s k , t 1 , . . . , t k of distinct vertices of R, the graph G has pairwise disjoint vertex-disjoint paths between s i and t i , for i ∈

Proof. Given a graph G, we use ω(G) to denote the maximum r such that G contains K r as a subgraph. Recall that the Clique problem asks, given a graph G and a positive integer k, whether ω(G) ≥ k. It is well-known that Clique is W[1]-hard [START_REF] Downey | Fundamentals of Parameterized Complexity[END_REF] when parameterized by k. Furthermore, the optimization version is hard from the parameterized approximation viewpoint. In particular, by the breakthrough result of Lin [START_REF] Lin | Constant approximating k-clique is w[1]-hard[END_REF], for any positive constant c ≥ 1, no algorithm running in time O k (n O (1) ) for a computable function f (k) can distinguish between the cases ω(G) ≥ k and ω(G) < k/c, unless FPT = W [START_REF] Adler | Computing excluded minors[END_REF]. We use this result for our reduction. Consider an instance (G, k) of Clique. Without loss of generality, we assume that k = 4r + 1 for an integer r ≥ 2. We construct the graph G as follows (see Figure 11).

• For every vertex x ∈ V (G), construct a set S x of (k -1)/2 vertices (note that k -1 is even) and then form a clique from S = x∈V (G) S x by making the vertices pairwise adjacent.

• For every vertex x ∈ V (G), construct a vertex w x and make it adjacent to the vertices of S x ; denote W = {w x : x ∈ V (G)}.

• For every edge {x, y} ∈ E(G), construct a vertex e xy and make it adjacent to the vertices of S x and S y ; denote L = {e xy : {x, y} ∈ E(G)}.

We set R = W ∪ L and k = 1 2 k 2 + 1; note that k is an integer because k is odd and k -1 is divisible by 4.

First, we show that if G contains a clique of size k as a subgraph, then there are disjoint k -tuples (s 1 , . . . , s k ) and (t 1 , . . . , t k ) of vertices of R such that G has no vertex-disjoint paths between s i and t i , for i ∈ [k ].

We use the following observation.

By Turan's theorem [START_REF] Turán | Eine Extremalaufgabe aus der Graphentheorie[END_REF], 2 . This inequality is equivalent to |Z| ≤ k(k-3) 2 2(k-5) and holds because k(k-3) 2 2(k-5) ≥ k 2 + 2 = 2k ≥ |Z|. We conclude that H has a matching M saturating every vertex of Y .

Note that for every w x ∈ X ∩ W , there is an adjacent vertex v ∈ S x \ S x . By adding {w x , v} to M for each w x ∈ X ∩ W , we obtain a matching M in G saturating every vertex of X. This concludes the proof of the claim.

Using Claim 5, we construct the paths between s i and t i in G as follows. Let i ∈ [k ]. The matching M contains the edges {s i , u} and {t i , v}, for some u, v ∈ S. Because S is a clique, (s i , u, v, t i ) is an (s i , t i )-path. Since M is a matching, all these paths are vertex-disjoint.

To conclude the proof, note that the existence of an algorithm solving Ordered Linkability in time O k (n O (1) ) would imply that there is an algorithm distinguishing the cases ω(G) ≥ k and ω(G) < k/5 in time f ( 1 2 k 2 + 1) • n O (1) , contradicting the result of Lin [START_REF] Lin | Constant approximating k-clique is w[1]-hard[END_REF].

C.2 Monochromatic Path Topological Minor is W[1]-hard on planar graphs

Topological minor models. Given a graph G and a graph H, we say that H is a topological minor of G if there is an injection ϕ : V (H) → V (G) and a function ψ mapping the edges of H to paths of G such that • For every distinct e 1 , e 2 , ψ(e 1 ) and ψ(e 2 ) are internally vertex disjoint paths of G and • For every e = {x, y} ∈ E(G), ψ(e) is a path joining ϕ(x) and ϕ(y).

Given the above, we say that H is a topological minor of G via the pair (ϕ, ψ).

We consider the following problem:

Monochromatic Path Topological Minor Input: multicolored graph (G, X 1 , . . . , X z ) a graph H and a coloring function λ : V (H) → [z]. Question: does G contain H as a topological minor via a pair (ϕ, ψ) where

• for every x ∈ V (H), ϕ(x) ∈ X λ(x) (i.e., the image of x carries the color of x) and • every e ∈ E(H), there is some i ∈ [z] such that V (ψ(e)) ⊆ V i (i.e., the path ψ(e) is monochromatic) Theorem 6. Monochromatic Path Topological Minor, when parameterized by k = |H|, is W[1]-hard on planar graphs, even when z = 4 and H is the (k × k)-grid.

Proof. We give a parameterized reduction from the following problem: