Fedor V Fomin
email: fedor.fomin@ii.uib.no

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

Giannos Stamoulis
email: giannos95@gmail.com

Dimitrios M Thilikos

An Algorithmic Meta-Theorem for Graph Modification to Planarity and FOL

Keywords: 2012 ACM Subject Classification Mathematics of computing → Graph algorithms; Theory of computation Graph modification Problems, Algorithmic meta-theorems, First Order Logic, Irrelevant vertex technique, Planar graphs, Surface embeddable graphs Digital Object Identifier 10.4230/LIPIcs.ESA.2020.51

In general, a graph modification problem is defined by a graph modification operation and a target graph property P. Typically, the modification operation may be vertex removal, edge removal, edge contraction, or edge addition and the question is, given a graph G and an integer k, whether it is possible to transform G to a graph in P after applying k times the operation on G. This problem has been extensively studied for particilar instantiations of and P. In this paper we consider the general property P φ of being planar and, moreover, being a model of some First-Order Logic sentence φ (an FOL-sentence). We call the corresponding meta-problem Graph -Modification to Planarity and φ and prove the following algorithmic meta-theorem: there exists a function f : N 2 → N such that, for every and every FOL sentence φ, the Graph -Modification to Planarity and φ is solvable in f (k, |φ|) • n 2 time. The proof constitutes a hybrid of two different classic techniques in graph algorithms. The first is the irrelevant vertex technique that is typically used in the context of Graph Minors and deals with properties such as planarity or surface-embeddability (that are not FOL-expressible) and the second is the use of Gaifman's Locality Theorem that is the theoretical base for the meta-algorithmic study of FOL-expressible problems.

Introduction

The term algorithmic meta-theorems was coined by Grohe in his seminal exposition in [START_REF] Grohe | Logic, graphs, and algorithms[END_REF] in order to describe results providing general conditions, typically of logical and/or combinatorial nature, that automatically guarantee the existence of certain types of algorithms for wide families of problems. Algorithmic meta-theorems reveal deep relations between logic and combinatorial structures, which is a fundamental issue of computational complexity. Such theorems not only yield a better understanding of the scope of general algorithmic techniques and the limits of tractability but often provide (or induce) a variety of new algorithmic results. The archetype of algorithmic meta-theorems is 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] stating that all graph properties expressible in Monadic Second-Order Logic (in short, MSOL-expressible properties) are fixed-parameter tractable when parameterized by the size of the sentence and the treewidth of the graph.

Our meta-theorem belongs to the intersection of two algorithmic research directions: Deciding First-Order Logic properties of sparse graphs and graph planarization algorithms.

FOL-expressible properties on sparse graphs. For graph properties expressible in firstorder logic (in short FOL-expressible properties), a rich family of algorithmic meta-theorems, were developed within the last decades. Each of these meta-theorems can be stated in the following form: for a graph class C, deciding FOL-expressible properties is fixed-parameter tractable on C, i.e. there is an algorithm running in f (|φ|) • n O (1) time where |φ| is the size of the the input FOL-sentence φ and n is the number of vertices of the input graph. The starting point in the chain of such meta-theorems is the work of Seese [START_REF] Seese | Linear time computable problems and first-order descriptions[END_REF] for C being the class of graphs of bounded degree [START_REF] Seese | Linear time computable problems and first-order descriptions[END_REF]. The first significant extension of Seese's theorem was obtained by Frick and Grohe [START_REF] Frick | Deciding first-order properties of locally tree-decomposable structures[END_REF] for the class C of graphs of bounded local treewidth [START_REF] Frick | Deciding first-order properties of locally tree-decomposable structures[END_REF]. The class of graphs of bounded local treewidth contains graphs of bounded degree, planar graphs, graphs of bounded genus, and apex-minor-free graphs. The next step was done by Flum and Grohe [START_REF] Flum | Fixed-parameter tractability, definability, and model-checking[END_REF], who extended these results up to graph classes excluding some minor. Dawar, Grohe, and Kreutzer [START_REF] Dawar | Locally excluding a minor[END_REF] pushed the tractability border up to graphs locally excluding a minor. Further extension was due to Dvořák, Král, and Thomas, who proved tractability for the class C of being locally bounded expansion [START_REF] Dvorák | Testing first-order properties for subclasses of sparse graphs[END_REF]. Finally, Grohe, Kreutzer, and Siebertz [START_REF] Grohe | Deciding first-order properties of nowhere dense graphs[END_REF] established fixed-parameter tractability for classes that are effectively nowhere dense. In some sense, the result of Grohe et al. is the culmination of this long line of meta-theorems, because for somewhere dense graph classes closed under taking subgraphs deciding first-order properties is unlikely to be fixed-parameter tractable [START_REF] Dvorák | Testing first-order properties for subclasses of sparse graphs[END_REF][START_REF] Kreutzer | Algorithmic meta-theorems[END_REF].

Notice that the above line of results also sheds some light on graph modification problems. In particular, since many modification operations are FOL-expressible, in some situations when the target property P is FOL-expressible, the above meta-algorithmic results can be extended to graph modification problems. As a concrete example, consider the problem of removing at most k vertices to obtain a graph of degree at most 3. All vertices of the input graph of degree at least 4 + k should be deleted, so we delete them and adapt the parameter k accordingly. In the remaining graph all vertices are of degree at most 3 + k and the property of removing at most k vertices from such a graph to obtain a graph of degree at most 3 is FOL-expressible. Hence the Seese's theorem implies that there is an algorithm of running time f (k) • n O (1) solving this problem. However these theories are not applicable with instantiations of P, like planarity, that are not FOL-expressible.

51:3

Another island of tractability for graph modification problems is provided by Courcelle's theorem and similar theorems on graphs of bounded widths. For example, graph modification problems are fixed-parameter tractable in cases where the target property P is MSOLexpressible under the additional assumption that the graphs in P have fixed treewidth (or bounded rankwidth, for MSOL 1 -properties, see e.g., [START_REF] Courcelle | Vertex-minors, monadic second-order logic, and a conjecture by seese[END_REF]).

To conclude, according to the current state of the art, all known algorithmic meta-theorems concerning fixed-parameter tractability of graph modification problems are attainable either when the target property P is FOL-expressible and the structure is sparse or when P is MSOL/MSO 1 -expressible and the structure has bounded tree/rank-width. Interestingly, planarity is the typical property that escapes the above pattern: it is not FOL-expressible and it has unbounded treewidth.

Graph planarization.

The Planar Vertex Deletion problem is a generalization of planarity testing. For a given graph G the goal is to find a vertex set of size at most k whose removal makes the resulting graph planar. Planarity is a nontrivial and hereditary graph property, hence by the result of Lewis and Yannakakis [START_REF] Lewis | The node-deletion problem for hereditary properties is np-complete[END_REF], the decision version of Planar Vertex Deletion is NP-complete. The parameterized complexity of this problem has been extensively studied.

The non-uniform fixed-parameter tractability of Planar Vertex Deletion (parameterized by k) follows from the deep result of Robertson and Seymour in Graph Minors theory [START_REF] Robertson | Graph minors. XX. wagner's conjecture[END_REF], that every minor-closed graph class can be recognized in polynomial time. Since the class of graphs that can be made planar by removing at most k vertices is minor-closed, the result of Robertson and Seymour implies that for Planar Vertex Deletion, for each k, there exists a (non-uniform) algorithm that in time O(n 3 ) solves Planar Vertex Deletion. Significant amount of work was involved to improve the enormous constants hidden in the big-Oh and the polynomial dependence in n. Marx and Schlotter [START_REF] Marx | Obtaining a planar graph by vertex deletion[END_REF] gave an algorithm that solves the problem in time f (k) • n 2 , where f is some function of k only. Kawarabayashi [START_REF] Kawarabayashi | Planarity allowing few error vertices in linear time[END_REF] obtained the first linear time algorithm of running time f (k) • n and Jansen, Lokshtanov, and Saurabh [START_REF] Bart | A near-optimal planarization algorithm[END_REF] obtained an algorithm of running time

O(2 O(k log k) • n).
For the related problem of contracting at most k edges to obtain a planar graph, Planar Edge Contraction, an f (k) • n O (1) time algorithm was obtained by Golovach, van 't Hof and Paulusma [START_REF] Golovach | Obtaining planarity by contracting few edges[END_REF]. Approximation algorithms for Planar Vertex Deletion and for Planar Edge Deletion were studied in [START_REF] Chekuri | Approximation algorithms for euler genus and related problems[END_REF][START_REF] Chuzhoy | An algorithm for the graph crossing number problem[END_REF][START_REF] Chuzhoy | On graph crossing number and edge planarization[END_REF].

Our results. Let be one of the following operations on graphs: Vertex removal, edge removal, edge contraction, or edge addition. We are interested whether, for a given graph G and an FOL-sentence φ, it is possible to transform G by applying at most k -operations, into a planar graph with the property defined by φ. We refer to this problem as the Graph -Modification to Planarity and φ problem. For example, when is the vertex removal operation and φ is a tautology, then the problem is Planar Vertex Deletion. Similarly, Graph -Modification to Planarity and φ generalizes Planar Edge Deletion and Planar Edge Contraction. On the other hand, for the special case of k = 0 this is the problem of deciding FOL-expressible properties on planar graphs.

Examples of first-order expressible properties are deciding whether the input graph G contains a fixed graph H as a subgraph (H-Subgraph Isomorphism), deciding whether there is a homomorphism from a fixed graph H to G to (H-Homomorphism), satisfying degree constraints (the degree of every vertex of the graph should be between a and b for some constants a and b), excluding a subgraph of constant size or having a dominating E S A 2 0 2 0 51:4 An Algorithmic Meta-Theorem for Graph Modification to Planarity and FOL set of constant size. Thus Graph -Modification to Planarity and φ encompasses the variety of graph modification problems to planar graphs with specific properties. For example, can we delete k vertices (or edges) such that the obtained graph is planar and each vertex belongs to a triangle? Reversely, can we delete at most k vertices (or edges) from a graph such that the resulting graph is a triangle-free planar graph? Can we add (or contract) at most k edges to such that the resulting graph is 4-regular and planar? Or can we delete at most k edges resulting in a square-free or claw-free planar graph? Informally, our main result can be stated as follows.

Theorem (Informal). Graph -Modification to Planarity and φ is solvable in time f (k, φ) • n 2 , for some function f depending on k and φ only. Thus the problem is fixed-parameter tractable, when parameterized by k + |φ|.

Our theorem not only implies that Planar Vertex Deletion is fixed-parameter tractable parameterized by k (proved in [START_REF] Bart | A near-optimal planarization algorithm[END_REF][START_REF] Marx | Obtaining a planar graph by vertex deletion[END_REF]) and that deciding whether a planar graph has a first-order logic property φ is fixed-parameter tractable parameterized by |φ| (that follows from [START_REF] Dawar | Locally excluding a minor[END_REF][START_REF] Dvorák | Testing first-order properties for subclasses of sparse graphs[END_REF][START_REF] Frick | Deciding first-order properties of locally tree-decomposable structures[END_REF][START_REF] Grohe | Deciding first-order properties of nowhere dense graphs[END_REF]). It also implies a variety of new algorithmic results about graph modification problems to planar graphs with some specific properties that cannot be obtained by applying the known results directly. Of course, for some formulas φ, Graph -Modification to Planarity and φ can be solved by more simple techniques. For example, if φ defines a hereditary property characterized by a finite family of forbidden induced subgraphs F, then deciding, whether it is possible to delete at most k vertices to obtain a planar F-free graph, can be done by combining the straightforward branching algorithm and, say, the algorithm of Jansen, Lokshtanov, and Saurabh [START_REF] Bart | A near-optimal planarization algorithm[END_REF] for Planar Vertex Deletion. For this, we iteratively find a copy of each F ∈ F and if such a copy exists we branch on all the possibilities to destroy this copy of F by deleting a vertex. By this procedure, we obtain a search tree of depth at most k, whose leaves are all F-free induced subgraphs of the input graph that could be obtained by at most k vertex deletions. Then for each leaf, we use the planarization algorithm limited by the remaining budget. However, this does not work for edge modifications, because deleting an edge in order to ensure planarity may result in creating a copy of a forbidden subgraph. For such type of problems, even for very "simple" ones, like deleting k edges to obtain a claw-free planar graph, or planar graph without induced cycles of length 4, our theorem establishes the first fixed-parameter algorithms. Also our theorem is applicable to the situation when φ defines a hereditary property that requires an infinite family of forbidden subgraphs for its characterization and for non-hereditary properties expressible in FOL.

In our paper, we show the result for Graph -Modification to Planarity and φ, but further we argue that it can be extended for modification problems to graphs embeddable to a surface of a given Euler genus.

The price we pay for such generality is the running time. While the polynomial factor in the running time of our algorithm is comparable with the running time of the algorithm of Marx and Schlotter [START_REF] Marx | Obtaining a planar graph by vertex deletion[END_REF] for Planar Vertex Deletion, it is worse than the more advanced algorithms of Kawarabayashi [START_REF] Kawarabayashi | Planarity allowing few error vertices in linear time[END_REF] and Jansen et al. [START_REF] Bart | A near-optimal planarization algorithm[END_REF]. Similarly, the algorithms for deciding first-order logic properties on graph classes [START_REF] Dvorák | Testing first-order properties for subclasses of sparse graphs[END_REF][START_REF] Frick | Deciding first-order properties of locally tree-decomposable structures[END_REF][START_REF] Grohe | Deciding first-order properties of nowhere dense graphs[END_REF] are faster than our algorithm.

The proof of the main theorem is based on a non-trivial combination of the irrelevant vertex technique of Robertson and Seymour [START_REF] Robertson | Graph minors. II. algorithmic aspects of tree-width[END_REF][START_REF] Robertson | Graph minors .xiii. the disjoint paths problem[END_REF] with the Gaifman's Locality Theorem [START_REF] Gaifman | On local and non-local properties[END_REF]. While both techniques were widely used, see [START_REF] Adler | Tight bounds for linkages in planar graphs[END_REF][START_REF] Cygan | The planar directed k-vertex-disjoint paths problem is fixed-parameter tractable[END_REF][START_REF] Golovach | Obtaining planarity by contracting few edges[END_REF][START_REF] Grohe | Finding topological subgraphs is fixed-parameter tractable[END_REF][START_REF] Bart | A near-optimal planarization algorithm[END_REF]28] and [START_REF] Dawar | Locally excluding a minor[END_REF][START_REF] Flum | Fixed-parameter tractability, definability, and model-checking[END_REF][START_REF] Frick | Deciding first-order properties of locally tree-decomposable structures[END_REF], the combination of the two techniques requires novel ideas. Following the popular trend in Theoretical Computer Science, an alternative title for our paper could be "Robertson and Seymour meet Gaifman". Organization of the paper. In Section 2 we give the formal definition of the general Graph -Modification to Planarity and φ problem, present the theoretical background around Gaifman's Locality Theorem, and give some preliminary definitions and results. In Section 3 we highlight the main ideas behind the proof explain how our arguments can be extended in cases where the target property is having bounded Euler genus and being a model of an FOL-sentence φ. Finally, in Section 4 we provide some directions for further research.

Problem definition and preliminaries

Before we explain our techniques, we give some necessary definitions. We denote by N the set of all non-negative integers. Given an n ∈ N, we denote by N ≥n the set containing all integers equal or greater than n. Given two integers x and y we define by [x, y] = {x, x+1, . . . , y-1, y}.

Given an n ∈ N ≥1 , we also define

[n] = [1, n].
All graphs in this paper are undirected, finite, and they do not have loops or multiple edges. Given a graph G, we denote by V (G) and E(G) the set of its vertices and edges, respectively. If S ⊆ V (G), then we denote by G \ S the graph obtained by G after removing from it all vertices in S, together with their incident edges. Also, we denote by G \ v the graph G \ {v}, for some v ∈ V (G). We also denote by

G[S] the graph G \ (V (G) \ S).

Modifications on graphs

We define OP := {vr, er, ec, ea}, that is the set of graph operations of removing a vertex, removing an edge, contracting an edge, and adding an edge, respectively. Given an operation ∈ OP, a graph G, and a vertex set R ⊆ V (G), we define the application domain of the operation as

G, R =        R, if = vr, E(G) ∩ R 2 , if = er, ec, and R 2 \ E(G), if = ea.
Notice that G, R is either a vertex set or a set of subsets of vertices each of size two. Given a set S ⊆ G, R , we define G S as the graph obtained after applying the operation on the elements of S. The vertices of G that are affected by the modification of G to G S, denoted by A(S), are the vertices in S, in case = vr or the endpoints of the edges of S, in case ∈ {er, ec, ea}.

Given an FOL-sentence φ and some ∈ OP , we define the following meta-problem:

Graph -Modification to Planarity and φ (In short: G MPφ) Input: A graph G and a non-negative integer k. Question: Is there a set S ⊆ G, V (G) of size k such that G S is a planar graph and G S |= φ?

Let (x 1 , . . . , x ) ∈ N and f, g : N → N. We use notation f (n) = O x1,...,x (g(n)) to denote that there exists a computable function h : N → N such that f (n) = h(x 1 , . . . , x ) • g(n).
We are ready to give the formal statement of the main theorem of this paper.

Theorem 1. There exists a function f : N 2 → N such that, for every FOL-sentence φ and for every ∈ OP, G MPφ is solvable in O k,|φ| (n 2 ) time.

Gaifman's theorem

For vertices u, v of graph G, we use d G (u, v) to denote the distance between u and v in G. We also use N (≤r) G (v) to denote the set of vertices of G at distance at most r from v.

Formulas. In this paper we deal with logic formulas on graphs. In particular we deal with formulas of first-order logic (FOL) and monadic second-order logic (MSO 2 ). The syntax of FOL-formulas includes the logical connectives ∨, ∧, ¬, a set of variables for vertices, the quantifiers ∀, ∃ that are applied to these variables, the predicate u ∼ v, where u and v are vertex variables and whose interpretation is that u and v are adjacent, and the equality of variables representing vertices. An MSO 2 -formula, in addition to the variables for vertices of FOL-formulas, may also contain variables for subsets of vertices or subsets of edges. The syntax of MSO 2 -formulas is obtained after enhancing the syntax of FOL-formulas so to further allow quantification on subsets of vertices or subsets of edges and introduce the predicates v ∈ S (resp. e ∈ F ) whose interpretation is that the vertex v belongs in the vertex set S (resp. the edge e belongs in the edge set F ).

An FOL-formula φ is in prenex normal form if it is written as

φ = Q 1 x 1 . . . Q n x n ψ such that for every i ∈ [n], Q i ∈ {∀, ∃}
and ψ is a quantifier-free formula on the variables x 1 , . . . , x n . Then Q 1 x 1 . . . Q n x n is referred as the prefix of φ. For the rest of the paper, when we mention the term "FOL-formula", we mean an FOL-formula on graphs that is in prenex normal form. Given an FOL-formula φ, we say that a variable x is a free variable in φ if it does not occur in the prefix of φ. We write φ(x 1 , . . . , x r ) to denote that φ is a formula with free variables x 1 , . . . , x r . We call a formula without free variables a sentence. For a sentence φ and a graph G, we write G |= φ to denote that φ evaluates to true on G. Also, for a sentence φ we denote its length by |φ|.

Gaifman sentences. Given an FOL-formula ψ(x) with one free variable x, we say that ψ(x) is r-local if the validity of ψ(x) depends only on the r-neighborhood of x, that is for every graph G and v ∈ V (G) we have

G |= ψ(v) ⇐⇒ N (≤r) G (v) |= ψ(v).
Observe that there exists an FOL-formula δ r (x, y) such that for every graph G and v, u ∈ [START_REF] Flum | Parameterized Complexity Theory[END_REF]Lemma 12.26]).

V (G), we have d G (u, v) ≤ r ⇐⇒ G |= δ r (v, u) (see
We say that an FOL-sentence φ is a Gaifman sentence when it is a Boolean combination of sentences φ 1 , . . . , φ m such that, for every h ∈ [m],

φ h = ∃x 1 . . . ∃x h 1≤i<j≤ h d(x i , x j ) > 2r h ∧ i∈[ h ] ψ h (x i ) , ( 1
)
where h , r h ≥ 1 and ψ h is an r h -local formula with one free variable. We refer to the variables x 1 , . . . , x h for each h ∈ [m] as the basic variables of φ. Moreover, for every h ∈ [m] we call φ h a basic local sentence of φ and the formula ψ h a local formula of φ.

Proposition 2 (Gaifman's Theorem [START_REF] Gaifman | On local and non-local properties[END_REF]). Every FOL-sentence φ is equivalent to a Gaifman sentence φ . Furthermore, φ can be computed effectively.

Equivalent formulations

Given a Gaifman sentence φ combined from sentences φ 1 , . . . , φ m and a unary relation symbol R, we define φ R as the sentence that is the same Boolean combination of sentences φ 1 R , . . . , φ m R such that, for every h ∈ [m],

φ h R = ∃x 1 . . . ∃x h i∈[ h ] x i ∈ R ∧ 1≤i<j≤ h d(x i , x j ) > 2r h ∧ i∈[ h ] ψ h (x i ) , ( 2
)
where h , r h ≥ 1 and ψ h is an r h -local formula with one free variable. Let (G, k) be an instance of the G MPφ problem. We may assume, because of Proposition 2, that φ is a Gaifman sentence. We consider an enhanced version of the G MPφ problem as follows. Let (G, R, k) be a triple, where G is a graph, R ⊆ V (G), and k ∈ N. We say that (G, R, k) is a (φ, )-triple if there exists a set S ⊆ G, R such that |S| ≤ k, G S is a planar graph, and G S |= φ R . Also, we say that a set

S ⊆ G, V (G) is a -planarizer of G if G S is planar.
It is easy to observe that the property that (G, R, k) is a (φ, )-triple can be expressed in MSO 2 . This is easy in case ∈ {vr, er, ec}. In the case where = ea, we observe the following: Observation 3. Let = ea, G be a graph, and S ⊆ G, V (G) where S = {{v 1 , u 1 }, . . . , {v r , u r }}. Then there exists an MSO 2 -formula φ P,S on structures of the type

(G, v 1 , u 1 , . . . , v r , u r ) such that G S is a planar graph ⇐⇒ (G, v 1 , u 1 , . . . , v r , u r ) |= φ P,S .
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 1. t∈V (T ) χ(t) = V (G); 2.
for every edge e of G there is a t ∈ V (T ) such that χ(t) contains both endpoints of e and 3. for every v ∈ V (G), the subgraph of T induced by {t ∈ V (T ) | v ∈ χ(t)} is connected. The width of (T, χ) is defined as w(T, χ) := max |χ(t)| -1 t ∈ V (T ) . The treewidth of G is defined as tw(G) := min w(T, χ) (T, χ) is a tree decomposition of G .

Theorem 1 is a consequence of the following lemma. Lemma 4. Given a Gaifman sentence φ and a ∈ OP, there exists a function f 1 : N 2 → N, and an algorithm with the following specifications:

Reduce_Instance(k, G, S, R) Input: an integer k ∈ N, a graph G, a set R ⊆ V (G)
, and a set S ⊆ R that is a vr-planarizer of G of size at most k.

Output: One of the following: Proof of Theorem 1. Let φ be an FOL-formula. By Proposition 2, φ is equivalent to a Gaifman sentence φ . Using the planarization algorithm from [START_REF] Bart | A near-optimal planarization algorithm[END_REF], we compute, in O k (n) steps, a vr-planarizer S of G of size at most k. If = ea, then S := ∅, while if ∈ {vr, er, ec}, then if such a set does not exist the we safely return a negative answer (for the case of = er, ec, this is due to the fact that if there exists a ecor an er-planarizer of G of size at most k then also a vr-planarizer of G of size at most k exists (see [START_REF] Golovach | Obtaining planarity by contracting few edges[END_REF]Lemma 1])). We are now in position to apply recursively the algorithm Reduce_Instance(k, G, S, R) of Lemma 4 until either an answer or the third case appears. In the first case, we either return a negative answer, if ∈ {er, ec, ea}, or set (k, G, S, R)

1. if ∈ {er, ec, ea}: a report that (G, k) is a no-instance of G MPφ. if = vr: a vertex u ∈ S such that S \ {u} is a vr-planarizer of G \ u of size at most k -1 and (G, k) and (G \ u, k -1) are equivalent instances of G MPφ. 2. a vertex set X ⊆ V (G) and a vertex v ∈ X such that S ⊆ R \ X and (G, R, k) is a (φ, )-triple iff (G \ v, R \ X, k) is a (φ,
:= (k -1, G \ v, S \ R) if = vr, while in the second case we set (k, G, S, R) := (k, G \ v, S, R \ X).
In the third case we have that tw(G) ≤ f 1 (k, |φ |). Recall that the property that (G, R, k) is a (φ, )-triple can be expressed in MSO 2 , thus the status of the final equivalent instance (G, R, k) can be evaluated in O k,|φ| (n) steps by applying Courcelle's theorem. As the recursion takes at most n steps, we obtain the claimed running time.

3

The algorithm

Two main lemmata

We now give two lemmata, whose combination gives the proof of Lemma 4. Before we state them, we give a series of definitions.

Let ∈ OP, G be a graph, k ∈ N, and let S be a -planarizer of G. We say that S is an inclusion-minimal -planarizer of G if none of its proper subsets is a -planarizer of G. Notice that, in the special case where = ea, the unique inclusion-minimal -planarizer of G is the empty set of edges. We say that a set Q ⊆ V (G) is -planarization irrelevant if for every inclusion-minimal -planarizer S of G that has size at most k, it holds that A(S) ∩ Q = ∅.

Partially disk-embedded graphs. We define a closed disk ∆ to be a subset of the plane homeomorphic to the set {(x, y) | x 2 + y 2 ≤ 1} and we use bor(∆) to denote its boundary. We say that a graph G is partially disk-embedded in some closed disk ∆, if there is some subgraph K of G that is embedded in ∆ such that bor(∆) is a cycle of K and no vertex in ∆ \ bor(∆) is adjacent to a vertex not in ∆. We use the term partially ∆-embedded graph G to denote that a graph G is partially disk-embedded in some closed disk ∆. 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 ∩ ∆.

Grids and walls.

Let k, r ∈ N. The (k × r)-grid is the Cartesian product of two paths on k and r vertices respectively. An elementary r-wall, for some odd r ≥ 3, is the graph obtained from a (2r × r)-grid with vertices (x, y), x ∈ [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. Given an elementary wall W , a vertical path of W is one whose vertices, in ordering 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), for 51:9 some i ∈ {1, 3, . . . , 2r -1}. Also an horizontal path of W is the one whose vertices, in ordering of appearance, are (1, j), (2, j), . . . , (2r, j), for some j ∈ [2, r -1], or (1, 1), (2, 1), . . . , (2r -1, 1) or (2, r), (2, r), . . . , (2r, r). An r-wall is any graph W obtained from an elementary r-wall W after subdividing edges (see Figure 1). We call the vertices that where added after the subdivision operations subdivision vertices, while we call the rest of the vertices (i.e., those of W ) branch vertices. The perimeter of W , denoted by perim(W ), is the cycle of W whose non-subdivision vertices are the vertices of the perimeter of W . Also, a vertical (resp. horizontal) path of W is a subdivided vertical (resp. horizontal) path of W .

A subgraph W of a graph G is called a wall of G if W is an r-wall for some odd r ≥ 3 and we refer to r as the height of the wall W .

Let W be a wall of a graph G and K be the connected component of G \ perim(W ) that contains W \ perim(W ). The compass of W , denoted by comp(W ), is the graph G[V (K ) ∪ V (perim(W ))]. Observe that W is a subgraph of comp(W ) and comp(W ) is connected.

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 all occurring vertices of degree one. Notice that each (2r + 1)-wall has r layers (see Figure 1). The central vertices of W , denoted by center(W ), are the two branch vertices of W that do not belong to any of its layers.

We are now in position to state the following two lemmata. Lemma 5. Given a ∈ OP, there exist two functions f 1 , f 2 : N 2 → N, and an algorithm with the following specifications:

Find_Area(k, q, G, S)
Input: a k ∈ N, an odd q ∈ N ≥1 , a graph G, and a set S ⊆ V (G) that is a vr-planarizer of G of size at most k.

Output: One of the following:

1. if ∈ {er, ec, ea}: a report that (G, k) is a no-instance of G MPφ. if = vr: a vertex u ∈ S such that S \ u is a vr-planarizer of G \ u of
N G (S) ∩ V (comp(W )) = ∅, or
3. a tree decomposition of G of width at most f 1 (k, q). Moreover, this algorithm runs in O k,q (n) steps.

By N G (S) we denote the vertices not in S adjacent in G with vertices in S. In the first possible output of the algorithm of Lemma 5 we have either a negative answer to the G MPφ problem or an equivalent instance of G MPφ with reduced value of k.

The main steps of the proof of Lemma 5 are the following. In case, = ea we first check whether G is planar. If not, we report a negative answer, otherwise we find a wall W in G whose size is a "big-enough" function of k and whose compass has "small-enough" treewidth using [START_REF] Golovach | The parameterized complexity of graph cyclability[END_REF]Lemma 4.2]. This wall contains an (also "big-enough") subwall of W whose compass is not affected by S. In case ∈ {vr, er, ec}, we consider the neighbors of S in the planar graph G , that is the set N := N G (S). Moreover, we consider a big enough triangulated grid Γ as a contraction of G (using [START_REF] Fedor | Contraction obstructions for treewidth[END_REF]Theorem 3]) and the set N Γ of the "contraction-heirs" of the vertices of N in Γ. If |N Γ | is "big-enough", then we prove, using the main technical result of [START_REF] Demaine | Bidimensional parameters and local treewidth[END_REF], that some of the vertices of S should be affected by every possible solution, in case = vr, or that we have a no-instance, in case ∈ {er, ec}. If |N Γ | is "small-enough", then we can find a "big-enough" wall W in G whose compass is not affected by S (again using the previously mentioned result of [START_REF] Golovach | The parameterized complexity of graph cyclability[END_REF]). The proof is completed by proving that this wall contains some "big-enough" subwall that is not affected by any inclusion-minimal -planarizer.

The next lemma deals with the second possible output of the algorithm of Lemma 5 and contains the "core arguments" of this paper. Lemma 6. Given a Gaifman sentence φ and a ∈ OP, there exists a function f 3 : N 2 → N and an algorithm with the following specifications:

Find_Vertex(k, ∆, G, R, W )
Input: a k ∈ N, a partially ∆-embedded graph G, a set of annotated vertices R ⊆ V (G), and a q-wall W of G such that

q = f 3 (k, |φ|). the compass of W has treewidth at most f 2 (k, q), G ∩ ∆ = comp( W ), bor(∆) = perim( W ), V (comp( W )) is -planarization irrelevant, and Output: a vertex set X V (comp( W )) and a vertex v ∈ X such that (G, R, k) is a (φ, )- triple iff (G \ v, R \ X, k) is a (φ, )-triple.

Moreover, this algorithm runs in

O k,|φ| (n) steps.
Notice that the above algorithm produces a (φ, )-triple where both R and G are reduced. To see why Lemma 4 follows from Lemma 5 and Lemma 6, observe that in the second possible output of the algorithm Find_Area(k, q, G, S) we can call the algorithm Find_Vertex(k, ∆, G, R, W ), where W := W , which outputs a vertex set X V (comp( W )) and a vertex v

∈ X such that (G, R, k) is a (φ, )-triple iff (G \ v, R \ X, k) is a (φ, )-triple. Observe that since N G (S) ∩ V (comp( W )) = ∅, then S ⊆ R \ X.
We insist that the algorithm Find_Vertex(k, ∆, G, R, W ) does not use the fact that N G (S) ∩ V (comp( W )) = ∅ but we use the latter to guarantee that S ⊆ R \ X. For the running time of Lemma 4, recall that the two algorithms of Lemma 5 and Lemma 6 run in O k,|φ| (n) steps.

Sketch of the proof of Lemma 6

In order to prove Lemma 6, we first find a collection W of "sufficiently many" subwalls of W each with ρ layers (where ρ is "big-enough"), whose compasses are pairwise vertex-disjoint.

The key idea is to define a "characteristic" of each wall W ∈ W that encodes all possible ways that a -planarizer S of G affects comp(W ) along with the ways that the fact that G S |= φ is certified by a vertex assignment to the basic variables of the Gaifman formula φ in comp(W ). Recall that φ R is a Boolean combination of sentences φ 1 R , . . . , φ m R so that for every h ∈ [m],

φ h R = ∃x 1 . . . ∃x h i∈[ h ] x i ∈ R ∧ 1≤i<j≤ h d(x i , x j ) > 2r h ∧ i∈[ h ] ψ h (x i ) ,
where h , r h ≥ 1 and ψ h is an r h -local formula with one free variable. Notice that φ R is evaluated on annotated graphs of the form (G, R). Clearly, φ R is a sentence in Monadic Second Order Logic, in short, a MSO 2 -sentence.

As a first step, for every h

∈ [m], W ∈ W, S ⊆ G, R of size at most k, I h ⊆ [ h ]
, and t ∈ [ρ], we define:

sig (S,I h ,t) φ h , (W ) :=        1, if ∃ X = {x i | i ∈ I h } ⊆ V (comp(W (t) ) S) ∩ R such that X is (|I h |, r h )-scattered in comp(W (t) ) S and G S |= x∈ X ψ h (x), 0, otherwise.
In the above definition, W (t) is the subwall of W that has t layers (which are the last t layers of W ) and the same center as W . Also, a set X of vertices is (α, β)-scattered, if |X| = α and there are no two vertices in X within distance ≤ 2β. Intuitively, sig

(S,I h ,t) φ h ,
(W ) = 1 if the application of the operation on G as defined by S gives rise to the existence of a scattered set X in the compass of W (t) so that when the vertices of X are assigned to the basic variables of φ h corresponding to I h , the local formula ψ h is satisfied for each x i ∈ X in the modified graph.

Next, for every W ∈ W and every S ⊆ G, R of size at most k we define:

msig (S)
φ, (W ) = (sig

(S,I 1 ,t) φ 1 , (W ), . . . , sig (S,Im,t) φm, (W )) | (I1, . . . , Im, t) ∈ 2 [ 1 ] × • • • × 2 [ m ] × [ρ] .
Clearly, msig

φ, (W ) can be seen as a (2 • ρ)-tuple of binary m-tuples, given that := h∈[m] h . Let SIG be the set of all such tuples and notice that |SIG| is bounded by some function of k and |φ| and msig

(S) φ, (W ) W ∈ W, S ⊆ G, R of size at most k ⊆ SIG.
It is now time to define the characteristic of a wall W ∈ W. We set r := max h∈[m] {r h } and d := 2(r + ( + 1)r + r). We define the (φ, )-characteristic of W as follows:

(φ, )-char(W ) = {(s, σ, t) ∈ [0, k] × SIG × [d + 1, ρ] | ∃S ⊆ G, R , |S| = s, A(S) ⊆ V (comp(W (t-d) )) ∩ R, comp(W ) S is planar, and msig (S) φ, (W ) = σ}.
Notice that all queries in the definition of (φ, )-char(W ) can be expressed in MSO 2 . Indeed, this is easy to see when ∈ {vr, er, ec}, as in this case the query "comp(W ) S is planar" is trivially true, since V (comp( W )) is -planarization irrelevant. In the case where = ea, the MSO 2 expressibility follows from Theorem 3. As each W ∈ W has treewidth bounded by a function of k and |φ|, it follows by the theorem of Courcelle that (φ, )-char(W ) can be computed in O k,|φ| (n) time.

E S A 2 0 2 0 51:12 An Algorithmic Meta-Theorem for Graph Modification to Planarity and FOL

We say that two walls are (φ, )-equivalent if they have the same (φ, )-characteristic. Since the collection W contains "sufficiently many" walls, then we can find a collection W ⊆ W of also "sufficiently many" walls that are pairwise equivalent. We fix a wall W 1 ∈ W and we set X := comp(W In what follows, we highlight the ideas of the proof of the fact that if (G, R, k) is a (φ, )triple, then (G \ v, R \ X, k) is a (φ, )-triple. We first consider a set S ⊆ G, R of size at most k that certifies that (G, R, k) is a (φ, )-triple. Then, we pick a wall W 2 ∈ W \ {W 1 } whose compass is not affected by S. We are allowed to pick this wall since there are "sufficiently many" walls equivalent to W 1 in W . Our strategy is to use the fact that W 1 and W 2 are (φ, )-equivalent in order to state a "replacement argument": we can find a t ∈ [ρ], such that the subset S in of S that affects comp(W (t) 1 ) and the set X of vertices of comp(W (t) 1 ) that are assigned to the basic variables of φ in order to certify that G S |= φ, can be replaced by their "equivalent" sets S and X in comp(W (t)

2 ). As a consequence of this, for every possible solution S and vertex assignment to the basic variables of φ, we can find both a new solution and a new vertex assignment that "avoid" the "inner part" of W 1 . This implies that the validity of any local formula of φ does not depend on the central vertices of W 1 . Thus, we can declare one of them "irrelevant" and safely remove it from G, while storing (by reducing R to R \ X) the fact that every possible solution S and vertex assignment to the basic variables of φ can "avoid" the "inner part" of W 1 .

To further inspect how this "replacement" is achieved, we need to dive deeper into the technicalities of the proof (through an intuitive perspective). Given a wall W , we refer to a wall-annulus of W as the subgraph of W that is obtained from W after removing from W all its layers, except a fixed number of consecutive layers. We think of every wall W ∈ W as divided in consecutive wall-annuli of fixed size. Since ρ is "big-enough", then we can find also "many enough" such wall-annuli. We denote each one of them by A i (W ). Given a W ∈ W, every wall-annulus A i (W ) is divided in some regions as depicted in Figure 2. The regions depicted in purple and green are consisting of r layers of the wall W (recall that r = max h∈[m] {r h }). The regions depicted in yellow and orange are "big-enough" so as to be able to find an also "big-enough" wall-annulus that "avoids" a given vertex assignment to the basic variables of φ.

Since ρ is "big-enough", then we can find a wall-annulus A i (W 1 ) that is not affected by S. This allows us to partition S in two sets, S in and S out in the obvious way. The fact that W 1 and W 2 are (φ, )-equivalent implies the existence of a set S in W 2 certifying that (φ, )-char(W 2 ) = (φ, )-char(W 1 ). Thus, by setting S := S ∪ S out , we have that S ⊆ G, R , |S | = |S|, and G S is planar. The latter is guaranteed by the fact that V (comp( W )) is -planarization irrelevant, in the case ∈ {vr , er, ec}, while in the case that = ea, the existence of the outer purple buffer of A i (W 1 ) (resp. A i (W 2 )) allows us to treat S in (resp. S) and S out separately, while not spoiling planarity. The last part of the proof requires to prove that G S |= φ R ⇐⇒ G S |= φ R .

For simplicity, here we only argue why G S |= φ h R =⇒ G S |= φ h R holds, as the arguments in the proof of the inverse direction are completely symmetrical. Therefore, given an ( h , r h )-scattered set X such that φ h is satisfied if the vertices of X are assigned to the basic variables of φ h , we aim to find a t ∈ [ρ] in order to "replace" the vertices in X ∩ V (comp(W (t) 1 )) with a set X of vertices in comp(W (t)

2 ) such that the resulting vertex set X is ( h , r h )-scattered and φ h is satisfied if the vertices of X are assigned to the basic variables of φ h . Notice that for every h ∈ [m] such that G S |= φ h R , these "replacement arguments" are pairwise independent.

We first deal with the possibility that the given scattered set X intersects some "inner part" of comp(W 2 ). Thus, in order to "clean" the "inner part" of comp(W 2 ), we find a wall W 3 ∈ W \ {W 1 , W 2 } that "avoids" both S and X (for different h ∈ [m], the choice of W 3 may coincide). Also, we consider a t ∈ [ρ] corresponding to a layer in the yellow region of the wall-annulus A i (W 2 ) such that the annulus of the wall-annulus of A i (W 2 ) bounded by the (t -r + 1)-th and t-th layer of W 2 is not intersected by X. Then, we "replace" the vertices of X in comp(W ( t)

2 ), call it X in with an "equivalent" vertex set X in comp(W

( t)
3 ) (notice that this is achieved by arguing for S := ∅ in the notion of (φ, )-characteristic). This results to an ( h , r h )-scattered set Y such that Y does not intersect comp(W ( t)

2 ) and G S |= x∈Y ψ h (x) (see Figure 3).

W 2 W 3 → W 2 W 3 Figure 3
The "cleaning" of the "inner part" of comp(W2). Left: The set A(S) is depicted in cross vertices, the set X \ Xin is depicted in blue, and the set Xin is depicted in red. Right: The set A(S) is depicted in cross vertices, the set Y \ Xin is depicted in blue, and the set X is depicted in red. Now, we are allowed to pick a t ∈ [ρ] corresponding to an "orange" layer of A i (W 1 ) such that the annulus of the wall-annulus of A i (W 1 ) bounded by the (t -r)-th and t -th layer of W 1 is not intersected by X. If we set Y in to be the set of vertices of Y in comp(W

(t ) 1 ), then since msig (Sin) φ, (W 1 ) = msig ( S) φ, (W 2 ), then there exists a set Ỹ in comp(W (t )
2 ) that is "equivalent" to Y in (see Figure 4). 2 ), then we can derive that Y and Ỹ are "separated" by a green and a purple region of A i (W 2 ). Thus, X := (Y \ Y in ) ∪ Ỹ is an ( h , r h )-scattered set of G S that "avoids" comp(W (r) 1 ). Moreover, φ h is satisfied given that the vertices of X of G S are assigned to the basic variables of φ h . The proof is concluded.

Extension on graphs of bounded genus

The immediate question is whether our results can be extended to target properties that are more general than planarity (and still not FOL-expressible). The first candidate is the -Modification to g-Euler Genus and φ, where we ask for a set S ⊆ G, V (G) of size k such that G S has Euler genus at most g. Notice that the property of having Euler genus at most g is not FOL-expressible. On the positive side, this property is MSO 2expressible as there is a set B g of graphs such that G has Euler genus at most g iff none of the graphs in B g is a minor of G and minor containment is MSO 2 -expressible. We next argue about how to adapt the techniques of this paper in order to prove that this problem can be solved in O k,|φ|,g (n 2 ) when ∈ {vr, er, ec}. For this we first straightforwardly extend the notions of -planarization irrelevant vertex set and -planarizer to the respective notions of -g-Euler Genus irrelevant vertex set -g-euler genus enforcer. Our aim is to prove a more general version of Lemma 4 where -planarizer is replaced by -g-euler genus enforcer. The O k,|φ|,g (n 2 ) time algorithm for -Modification to g-Euler Genus and φ follows directly from this extended version of Lemma 4 with the same arguments as its planarization counterpart. The extended version of Lemma 4 in turn is a consequence of the generalized versions of Lemma 5 and Lemma 6 where -planarizer is replaced by -g-euler genus enforcer and -planarization irrelevant is replaced by -g-Euler Genus irrelevant. The generalized version of Lemma 5 follows as the same arguments also hold on bounded-genus graphs: the result we use from [START_REF] Golovach | The parameterized complexity of graph cyclability[END_REF] has a bounded-genus analogue, the results from [START_REF] Fedor | Contraction obstructions for treewidth[END_REF] and [START_REF] Demaine | Bidimensional parameters and local treewidth[END_REF] hold for the more general graph class of apex-minor-free graphs. Also the fact that the "big-enough" q-wall that we find is -g-Euler Genus irrelevant can be proven using arguments from [25].

Having the extended version of Lemma 5, the proof of the extended version of Lemma 6 is almost identical as we still work inside a disk ∆ where G is partially embedded, so that local modifications should locally respect planarity. To be precise, the main difference is that in the definition of d, we now demand that d is also lower bounded by some big-enough function of the genus which guarantees that local modifications in the disk ∆ do not alter the genus of the whole graph.

Further research directions

In this paper we provide an algorithmic-meta theorem for the graph modifiction problem where the modification operation is in {vr, er, ec, ea} and the target property is planarity plus being a model of some FOL-sentence φ. We also argued how to extend this result for modification operations in {vr, er, ec} for the case where instead of planarity we consider the class of graphs embeddable in a surface of Euler genus g, for fixed g. The two general challenges that we distinguish are the following.

Pick a (non-empty) subset O of {vr, er, ec, ea} and define Graph O-Modification to Planarity and φ in the obvious way, by permitting any modification operation from O. It is possible (however more technical) to adapt our results for this problem in the case where ea ∈ O. However, in the case where ea ∈ O (while |O| > 1) the problem becomes considerably more complicated as parts of the graph may be relocated during the modification operation (in fact, from a more general perspective, the same issue appears for the ea-Modification to g-Euler Genus and φ problem that we avoided to consider in Subsection 3.3). We believe that this issue can be tackled using the techniques of [START_REF] Fedor | Modification to planarity is fixed parameter tractable[END_REF]. However, the technical details of such an enterprise seem to be quite involved. Consider other target properties, alternative to planarity, that are not FOL-expressible. A natural challenge in this direction is to consider some finite set of graphs H and define the -Modification to Excluding H-minors and φ problem where the target property, apart from being a model of φ, is to exclude every graph in H as a minor. Notice that if H contains some planar graph, then the yes-instance of the problem has bounded treewidth, therefore the problem is fixed-parameter tractable due to Courcelle's Theorem. The result of this paper can be seen as -Modification to Excluding {K 5 , K 3,3 }-minors and φ that is the simplest, however essential, version of the general problem. We conjecture that the same results can be achieved for every H and we believe that the techniques introduced in this paper can be the starting point of such a project.

F

  . V. Fomin, P. A. Golovach, G. Stamoulis, and D. M. Thilikos

F

F

  . V. Fomin, P. A. Golovach, G. Stamoulis, and D. M. Thilikos 51:7

  )-triple. 3. a tree decomposition of G of width at most f 1 (k, |φ|). Moreover, this algorithm runs in O k,|φ| (n) steps. -Theorem for Graph Modification to Planarity and FOL Given Lemma 4, Theorem 1 can be proved as follows.

Figure 1

 1 Figure 1 An 15-wall and its 7 layers.

size at most k - 1

 1 and (G, k) and (G \ u, k -1) are equivalent instances of G MPφ. 2. a q-wall W of G and a closed disk ∆ such that the compass of W has treewidth at most f 2 (k, q), G is partially ∆-embedded, where G ∩ ∆ = comp(W ), bor(∆) = perim(W ), Algorithmic Meta-Theorem for Graph Modification to Planarity and FOL V (comp(W )) is -planarization irrelevant, and

F

  where r = max h∈[m] {r h }, and v ∈ center(W 1 ).

Figure 2

 2 Figure 2 An example of a wall-annulus Ai(W ) of a wall W ∈ W, together with its regions refered in the proof of Lemma 6.

1 Figure 4

 14 Figure 4The last part of the proof. Left: The set A(Sout) is depicted in red cross vertices, the set A(Sin) is depicted in green cross vertices, the set Y \ Yin is depicted in blue, and the set Yin is depicted in red. Right: The set A(Sout) is depicted in red cross vertices, the set A( S) is depicted in green cross vertices, the set Y \ Yin is depicted in blue, and the set Ỹ is depicted in red.

been supported by the Research Council of Norway and the French Ministry of Europe and Foreign Affairs via the Franco-Norwegian project PHC AURORA 2019. Fedor V. Fomin: Research Council of Norway via the project "MULTIVAL". Petr A. Golovach: Research Council of Norway via the project "MULTIVAL". -CE40-0028) and ESIGMA (ANR-17-CE23-0010).