Édouard Bonnet

Eun Jung Kim

Amadeus Reinald

Stéphan Thomassé

Twin-width VI: the lens of contraction sequences

Keywords: 2012 ACM Subject Classification Theory of computation → Twin-width, contraction sequences, width parameters, FO and MSO model checking, matroids

A contraction sequence of a graph consists of iteratively merging two of its vertices until only one vertex remains. The recently introduced twin-width graph invariant is based on contraction sequences. More precisely, if one puts error edges, henceforth red edges, between two vertices representing non-homogeneous subsets, the twin-width is the minimum integer d such that a contraction sequence exists that keeps red degree at most d. By changing the condition imposed on the trigraphs (i.e., graphs with some edges being red) and possibly slightly tweaking the notion of contractions, we show how to characterize the well-established bounded rank-width, tree-width, linear rank-width, path-width -usually defined in the framework of branch-decompositions-, and proper minor-closed classes by means of contraction sequences.

Contraction sequences hold a crucial advantage over branch-decompositions: While one can scale down contraction sequences to capture classical width notions, the more general bounded twin-width goes beyond their scope, as it contains planar graphs in particular, a class with unbounded rank-width. As an application we give a transparent alternative proof of the celebrated Courcelle's theorem (actually of its generalization by Courcelle, Makowsky, and Rotics), that MSO2 (resp. MSO1) model checking on graphs with bounded tree-width (resp. bounded rank-width) is fixed-parameter tractable in the size of the input sentence. We are hopeful that our characterizations can help in other contexts.

We then explore new avenues along the general theme of contraction sequences both in order to refine the landscape between bounded tree-width and bounded twin-width (via spanning twin-width) and to capture more general classes than bounded twin-width. To this end, we define an oriented version of twin-width, where appearing red edges are oriented away from the newly contracted vertex, and the mere red out-degree should remain bounded. Surprisingly, classes of bounded oriented twin-width coincide with those of bounded twin-width. This greatly simplifies the task of showing that a class has bounded twin-width. As an example, using a lemma by Norine, Seymour, Thomas, and Wollan, we give a 5-line proof that Kt-minor free graphs have bounded twin-width. Without oriented twin-width, this fact was shown by a somewhat intricate 4-page proof in the first paper of the series. Finally we explore the concept of partial contraction sequences, instead of terminating on a single-vertex graph, the sequence ends when reaching a particular target class. We show that FO model checking (resp. ∃FO model checking) is fixed-parameter tractable on classes with partial contraction sequences to a class of bounded degree (resp. bounded expansion), provided such a sequence is given. Efficiently finding such partial sequences could turn out simpler than finding a (complete) sequence.

Introduction

A trigraph is a graph with some of its edges being distinguished, typically called red edges, while the rest of the edges are called black. The (vertex) contraction (or identification) of two non-necessarily adjacent vertices u and v in a trigraph consists of merging these two vertices into a new vertex w, keeping every edge wx black if both ux and vx were black edges, and turning all the other edges incident to w red. The rest of the trigraph does not change. A contraction sequence of an n-vertex (tri)graph G is a sequence of trigraphs G = G n , G n-1 , . . . , G 1 such that G i is an i-vertex trigraph, obtained by performing one contraction in G i+1 . A d-sequence is a contraction sequence such that every trigraph of the sequence has maximum red degree at most d. The twin-width of a graph is defined via contraction sequences: It is the minimum integer d such that G admits a d-sequence.

See Figure 1 for an example of a graph with a 2-sequence. Not to hinder the flow of this introduction, we will try to limit further definitions. The reader is deferred to Section 2 if encountering some unknown terminology. 1 Classes of bounded twin-width are surprisingly diverse. They include for instance classes of bounded tree-width, or even bounded rank-width, proper minor-closed classes, hereditary proper subclasses of permutation graphs, subgraphs of O(1)-dimensional grids [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], as well as Ω(log n)-subdivisions of n-vertex graphs, classes with bounded queue or stack number, and some families of expanders [START_REF] Bonnet | Twin-width II: small classes[END_REF]. Nevertheless classes of bounded twin-with have interesting properties: If a class C has bounded twin-width, then so has any class that is obtained from C by a fixed first-order transduction [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], they are χ-bounded [START_REF] Bonnet | Twin-width III: Max Independent Set, Min Dominating Set, and Coloring[END_REF], and allow a fixed-parameter tractable (FPT) algorithm for FO model checking [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], provided O(1)-sequences are given in input, and more practical FPT algorithms on specific problems like k-Independent Set or k-Dominating Set [START_REF] Bonnet | Twin-width III: Max Independent Set, Min Dominating Set, and Coloring[END_REF]. Twin-width naturally extends to matrices over finite alphabets and binary structures in general [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF][START_REF] Bonnet | Twin-width and permutations[END_REF]. Efficiently approximating twin-width (that is, returning an f (d)-sequence when the twin-width of the input is at most d) can be done for classes of totally ordered binary structures [START_REF] Bonnet | Twin-width IV: ordered graphs and matrices[END_REF], and for all the above-mentioned classes of bounded twin-width, but remains an open challenge for unordered graphs. This paper investigates variations on the theme of contraction sequences. We first show that bounded rank-width and bounded linear rank-width can be defined by means of contractions sequences. Instead of requiring the maximum red degree to be bounded, one shall strengthen the condition to bounded-size red components, and bounded total number of red edges, 2 respectively. In the sparse regime of biclique-free classes, this characterizes bounded tree-width and bounded path-width. See Figures 2c and2d for some illustration.

Let us elaborate on that with an alternative formalism. A useful equivalent viewpoint on contraction sequences is the notion of partition sequence, that is, a sequence P n , . . . , P 1 of partitions of the vertex set V (G), where P n is the partition into singletons, P 1 = {V (G)}, and each P i is obtained by merging two parts of P i+1 . Then a width w : P(V (G)) → N (i.e., a function from the partitions of V (G) to the naturals) can be naturally lifted to the graph G as the minimum integer t such that there exists a partition sequence P n , . . . , P 1 satisfying w(P i ) ⩽ t for every i. This defines the width of G associated to w.

What are partitions of "good quality" or small width? Probably partitions P i such that the quotient G/P i "captures" the edge set of G quite well, minimizing the extra amount of information one needs to fully recover G. In that respect, the ideal scenario is when a pair of parts X, Y ∈ P i is homogeneous, that is, X and Y are completely adjacent or completely non-adjacent in G. Consider the auxiliary graph with vertex set the parts of P i , and edge set all pairs of parts X, Y ∈ P i , which are not homogeneous. Note that this auxiliary graph is precisely the red graph of trigraph G i (as previously defined), that is, obtained from G i by keeping the red edges only. Three width measures come relatively naturally: the maximum degree, w d , the maximum component size, w c , and the total number of edges, w t , in the red graph of G i . We obtain the following invariants on graphs.

The twin-width of G as the width tww(G) associated to w d (see Figure 2a). The component twin-width of G as the width ltww(G) associated to w c (see Figure 2c). The total twin-width of G as the width ttww(G) associated to w t (see Figure 2d). As we will see in Section 3, the striking fact is that the latter two parameters already exist, up to functional equivalence.

▶ Theorem 1. The following parameters are functionally equivalent:

Component twin-width and rank-width; Total twin-width and linear rank-width.

rank-width) in the language of twin-width and contraction sequences. This unifying lens has two main benefits. The first benefit is simplicity and renewal. We propose some examples where our characterizations somewhat simplify matters or bring a new, slightly but resolutely different perspective. We give a short alternative proof of the celebrated theorem by Courcelle, Makowsky, and Rotics [START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF] that monadic second-order (MSO) model checking (with adjacency relation only) is fixed-parameter tractable on classes with bounded rank-width. More precisely, G |= φ is decidable in time f (|φ|, cw)|V (G)| on graphs G given with a clique-width expression with cw labels, and MSO sentences φ. This is known to generalize Courcelle's theorem that MSO model checking with incidence relation is fixed-parameter tractable on classes with bounded tree-width.

Let us sketch how our algorithm goes. Instead of parsing a clique-width expression (or a tree-decomposition), we scan the contraction sequence from G = G n to G 1 . We maintain types that are "local to the red graph", that is, the theory up to quantifier rank q of all the sentences of depth q that are true on a given red component. As the component twin-width is bounded, note that there is a bounded number of vertices per red component. Initially in G n = G, the red components are single vertices, hence the local theory is easy to determine. Eventually in G 1 , the whole graph has been merged into a single vertex, thus the local theory of the unique vertex of G 1 matches the "global" theory of G. As this is precisely what we are after, the crux lies in updating the local theories when moving from trigraph

G i+1 to trigraph G i . When contracting u, v ∈ V (G i+1 ), up to d + 1 red components of G i+1 are fused into one in G i ,
where d is the upper bound on the component twin-width. We show that the local theory on these red components, combined with the black edges sitting on them, is enough to determine unambiguously the local theory of the new red component. The relative simplicity of component twin-width brings our proof down to a minimum: one lemma in the vein of the Feferman-Vaught theorem [START_REF] Feferman | The first order properties of products of algebraic systems[END_REF]. For completeness, we prove this folklore lemma with Ehrenfeucht-Fraïssé games for MSO.

We also present an analogue to dynamic programming over clique-width expressions or tree-decompositions, with the approach of contraction sequences. We exemplify it with a practical algorithm for the particular MSO-expressible problem q-Coloring. As the MSO model checking algorithm, it can be described as dynamic programming over the contraction sequence. However this algorithm is obviously much more practical and simple than the generic MSO model checking. We then list some advantages that our approach holds over the classic dynamic-programming algorithms. In [START_REF] Bonnet | Twin-width III: Max Independent Set, Min Dominating Set, and Coloring[END_REF], this scheme was used to solve some particular FO-expressible problems on graphs of bounded twin-width given with an O(1)-sequence.

This brings us to the second benefit, which is an unexpected collapse of the metaalgorithmic techniques dedicated to handle first-order and monadic second-order logic. Dynamic programming over contraction sequences tackles in one sweep problems that were seemingly as different and required as disparate techniques as k-Subgraph Isomorphism on planar graphs3 and q-Coloring on graphs of bounded rank-width [START_REF] Cygan | Parameterized algorithms[END_REF]. Another realization of that collapse is a similar algorithm efficiently solving FO model checking on graphs of bounded twin-width given with O(1)-sequences [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], and MSO model checking on graphs of bounded rank-width/bounded component twin-width. This motivates searching for characterizations or generalizations of classes of bounded expansion or nowhere dense classes by means of contraction sequences, as a way to push further their unifying power.

We also define a notion of spanning twin-width, 4 intermediate between bounded tree-width and bounded twin-width, which exactly captures classes excluding a minor, among monotone classes.

▶ Theorem 2. A monotone graph class C has bounded spanning twin-width if and only if it is proper minor-closed.

So far we explored what happens when restricting the notion of bounded twin-width. Here is an attempt to generalize it. One may observe that homogeneity of two distinct parts X, Y of P i is in fact a directed relation. Let us say that Y is homogeneous to X if the pair X, {y} is homogeneous for all y ∈ Y . We can now form the directed red graph D i whose vertices are the parts of P i , and with arcs X → Y for all pairs X, Y ∈ P i with Y not homogeneous to X. The oriented width of P i is the maximum out-degree w o of D i . This defines the oriented twin-width of G denoted otww(G) (see Figure 2b). Note that otww(G) ⩽ tww(G) since contracting parts can only create red arcs, which are directed from the contracted vertex.

Oriented twin-width is in some sense "fairer" than twin-width, as far as the "error count" is concerned. When an error (red edge) occurs while contracting two parts, it is only accounted to the newly contracted part, and not to other adjacent parts (since only their red in-degree may increase). Surprisingly, we will see that: ▶ Theorem 3. Oriented twin-width and twin-width are functionally equivalent.

The proof simply revisits the equivalence between bounded twin-width and so-called O(1)mixed freeness (see Section 2), and can almost integrally be found in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF]. Our contribution here is mainly conceptual, in identifying the overlooked oriented twin-width. The indirect nature of the proof, which does not immediately provide an O(1)-sequence from a partition sequence with bounded oriented width, suggests that something non-trivial is at play. Indeed this greatly simplifies, as we then exemplify, the proof that K t -minor free graphs have bounded twin-width presented in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF]. We also observe that planar graphs have oriented twin-width at most 9. Together with Theorem 3, this gives a very direct proof that planar graphs have bounded twin-width.

Another direction to generalize bounded twin-width is to allow contraction sequences to end at "simple" (tri)graphs instead of the 1-vertex graph. Of course for this notion to be new, "simple" should not imply bounded twin-width. Bounded-degree and bounded-expansion are reasonably "tractable" classes with unbounded twin-width [START_REF] Bonnet | Twin-width II: small classes[END_REF]. We say that a class C is collapsible to a class D if graphs of C admit partial O(1)-sequences to (tri)graphs in D. We showcase the flexibility of the FO model-checking algorithm in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF]: Collapsible classes to bounded degree and collapsible classes to bounded expansion admit respectively a fixed-parameter tractable FO and ∃FO model-checking algorithm, provided a corresponding partial O(1)-sequence is given. This is a relatively elementary fusion of the algorithm in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] and classic techniques from the meta-algorithmic toolbox, namely Gaifman's locality theorem and low tree-depth covers. On the one hand, it can be seen as a first attempt to unify and extend tractable FO model-checking algorithms on "sparse" classes (bounded degree, bounded expansion) and on possibly "dense" classes (bounded twin-width). On the other hand, we explain why efficiently finding the corresponding partial O(1)-sequences, may turn out simpler than computing (complete) O(1)-sequences.

Organization of the paper.

In Section 2 we recall the relevant background. In Section 3 we show Theorem 1, present an alternative proof of Courcelle's theorems, and give a practical algorithm for q-Coloring on graphs of bounded component twin-width (i.e., bounded rank-width). In Section 4, we prove Theorem 3 and use it to bound the twin-width of K t -minor free graphs. In Section 5, we present some FO model-checking algorithms using partial contraction sequences to classes of bounded degree and bounded expansion. In Section 6, we show the equivalence between proper minor-closed and bounded spanning twin-width, for monotone classes.

Preliminaries

We denote by [i, j] the set of integers {i, i + 1, . . . , j -1, j}, and [k] is a short-hand for [1, k].

We use the standard graph-theoretic definitions and notations. Given a graph G, its vertex set is denoted by V (G) and its edge set by E(G). Given a subset S of V (G), G[S] denotes the subgraph of G induced by S.

Two parameters w and w ′ defined on graphs (or more generally on matrices) are functionally equivalent if there exists a function f such that for every graph (or matrix) G, we have w(G) ⩽ f (w ′ (G)) and w ′ (G) ⩽ f (w(G)). Among classical pairs of functionally equivalent parameters, let us mention branch-width and tree-width, or rank-width and clique-width. When speaking of a class C of graphs, we mean closed under isomorphism. When C is furthermore closed under taking subgraphs, we speak of a monotone class and when C is closed under induced subgraphs, we speak of a hereditary class. A class C of graphs is sparse if there is a t for which no graph in C contains the complete bipartite graph K t,t as a subgraph (i.e., not necessarily induced).

To avoid unnecessary notations, a connected component of a graph may either refer to a (maximal connected) vertex set or its induced subgraph. More often our connected components will be vertex sets, contrary to the standard definition.

Branch decompositions

A branch decomposition of a graph G is a ternary tree T in which the leaves are in one-toone correspondence with V (G). In particular every edge e of T corresponds to the vertex bipartition B e of G defined by the two sets of leaves of the connected components of T \ e. Given now any function m from graph bipartitions to the non-negative integers, we obtain a parameter b m (G), which is the minimum, over all branch-decompositions T of G of the maximum of m(B e ) over all edges e of T .

For instance, when m(B e ) is the rank (computed in F 2 ) of the adjacency matrix of the bipartite subgraph of G spanned by the vertex bipartition B e , the parameter b m is the rank-width of G. We obtain the linear rank-width of G by keeping the same rank function m but insisting that branch-decompositions T are ternary trees where the internal vertices form a path. A class has bounded tree-width (resp. bounded path-width) if and only if it is sparse (i.e., K t,t -free) and has bounded rank-width (resp. bounded linear rank-width) [START_REF] Gurski | The tree-width of clique-width bounded graphs without Kn[END_REF]. Hence tree-width and path-width can be seen as the sparse restrictions of rank-width and linear rank-width.

Let us now introduce a parameter, which is equivalent to rank-width. The boolean-width bool(X, Y ) of a bipartition (X, Y ) of V (G) is the logarithm in base 2 of the number of subsets of Y (equivalently, of X) that are the neighborhood of some subset of X (resp. of Y ). The boolean-width of a graph G is the parameter b bool (G). Boolean-width is functionally equivalent to rank-width. When we only consider branch decompositions in which internal vertices form a path, we speak of linear boolean-width, which is similarly equivalent to linear rank-width.

We will use the next observation implicitly, which is proved in [START_REF] Bui-Xuan | Boolean-width of graphs[END_REF].

▶ Observation 4. Let (X, Y ) be a vertex bipartition of G, and let q be the maximum number of vertices in X, which have distinct neighborhoods in the bipartite graph G(X, Y ) (i.e., ignoring edges within X and within Y ). Then, the boolean-width of (X, Y ) is at least log 2 q and at most q.

It is often convenient to root a branch-decomposition T of G at some arbitrary non leaf node. Given then an internal node v of T , the leaves of the subtree of T rooted at v is denoted by A v , and the bipartition (A v , V (G) \ A v ) of G is said to be associated with v. Note that there is a unique bipartition associated with an internal node of T .

Branch-decompositions are a very popular concept and can be adapted to partitions of the edge set instead of the vertex set (leading to the branch-width), or to the ground set of a matroid using as parameter its connectivity function (yielding matroid branch-width). One very appealing feature is that parameters defined by branch-decompositions admit dual parameters via tangles [START_REF] Oum | Certifying large branch-width[END_REF]. However, the main limitation is that planar graphs have unbounded value for parameters defined with branch-decompositions. Indeed every balanced bipartition of a planar graph is complex, and thus return a large value for the classical parameters m, which in turn gives an unbounded b m . The main way to overcome the "planar barrier" is to measure the complexity of vertex partitions instead of vertex bipartitions.

Partition sequences

A partition sequence of a graph G is a sequence S = P n , . . . , P 1 of partitions of V (G) where P n := {{v} : v ∈ V (G)} is the partition of V (G) into singletons, P 1 = {V (G)} is the whole set, and each P i is obtained by merging two parts of P i+1 . In particular each P i consists of i subsets of V (G). A vertex ordering compatible with S is any total order ⩽ on V (G) (often also seen as a permutation σ) such that for every P i and every part X in P i , the elements of X are consecutive along ⩽.

A function w from vertex-partitioned graphs into the non-negative integers is called a width. The partition-width associated to w of a graph G is the minimum integer t such that there exists a partition sequence P n , . . . , P 1 of G such that w(P i ) ⩽ t for every i ∈ [n]. We denote it by p w (G).

We say that two disjoint subsets of vertices X, Y of a graph G are homogeneous if there are all edges or no edge between them. More generally, if G is a binary structure, we insist that any two ordered pairs (x, y) and (x ′ , y ′ ) with x, x ′ ∈ X and y, y ′ ∈ Y induce the same structure. By extension, X is homogeneous with X when X is a singleton, but is not homogeneous with X when X has at least two elements. Indeed if x, x ′ ∈ X, the isomorphism type of x, x and the one of x, x ′ are not the same.

Given a graph G and a partition P i , we consider an auxiliary trigraph G i , called quotient trigraph and denoted by G/P i , with vertices the parts of P i , red edges all pairs of parts X, Y , which are not homogeneous, and black edges all pairs of parts X, Y for which X, Y is a complete bipartite graph in G. The red graph R(G i ) (resp. black graph) of G i has vertex set V (G i ), and edge set its red edge set R(G i ) (resp. black edge set E(G i )). A red component of a trigraph is a connected component in its red graph R(G i ), while its (maximum) red degree is the (maximum) degree of R(G i ).

By our convention, we add a loop (X, X) to every part X, which is not a singleton. Loops count as degree 1. Note that a vertex u of G i corresponds to a subset of vertices of G, which we denote by u(G). It will also be convenient to speak of the total degree of u in G i , which is the total number of red and black edges incident to u. The graph obtained from G i by forgetting the colors (i.e., the graph that is the union of the red and black edges) is called the total graph of G i .

A module in a graph G is a subset of vertices X such that for every x, x ′ ∈ X and y ∈ V (G) \ X, both xy and x ′ y induce an edge or both induce a non-edge. Here we do not impose that X is a maximal subset satisfying the latter property. More generally, if G is a binary structure, we insist that the ordered pairs xy and x ′ y induce the same structure. When X, Y are two disjoint subsets of vertices, we say that Y is homogeneous to

X if Y is a module in G[X ∪ Y ].
We obtain a directed version of G i as follows: The directed trigraph D i is obtained from G i by orienting red edges XY as X → Y whenever X is not homogeneous to Y and keeping black edges unchanged. Note that some red edges of D i can be directed in both ways.

Given G and a partition P i , we define four possible widths: w o is the maximum red out-degree of D i , w d is the maximum red degree of G i , w c is the maximum number of vertices in a red connected component of G i , and w t is the total number of red edges in G i . Note that w o ⩽ w d ⩽ w c ⩽ w t . We now obtain the associated width-parameters:

The oriented twin-width of G as the partition-width otww(G) associated to w o .

The twin-width of G as the partition-width tww(G) associated to w d .

The component twin-width of G as the partition-width ltww(G) associated to w c . The total twin-width of G as the partition-width ttww(G) associated to w t .

Observe that otww(G) ⩽ tww(G) ⩽ ltww(G) ⩽ ttww(G). Note that there is a slight variation with our original definition of twin-width since loops add one to the degree. For the sake of consistency, we will actually drop the red loops for oriented twin-width and twin-width. We will see in Sections 3 and 4 that we did not create new parameters: ▶ Theorem. The following parameters are functionally equivalent:

Twin-width and oriented twin-width. Component twin-width and rank-width. Total twin-width and linear rank-width.

It is somewhat comforting to be on charted territory since the choices of the widths w o , w d , w c , w t are natural. The equivalence between oriented twin-width and twin-width is very handy, as we will see in Section 4.

The matrix viewpoint

Given an n × m matrix M , a row-partition (resp. column-partition) is a partition of the rows (resp. columns) of M . A (k, ℓ)-partition (or simply partition) of a matrix M is a pair (R = {R 1 , . . . , R k }, C = {C 1 , . . . , C ℓ })
where R is a row-partition and C is a column-partition. A contraction or merge of a partition P consists of replacing two parts in P by their union. A contraction of a partition (R, C) of a matrix M is obtained by performing one contraction in the row-partition R or in the column-partition C.

We distinguish two extreme partitions of an n × m matrix M : the finest partition where (R, C) have size n and m, respectively, and the coarsest partition where they both have size one. A contraction sequence of an n × m matrix M is a sequence of partitions

(R 1 , C 1 ), . . . , (R n+m-1 , C n+m-1 ) where (R 1 , C 1 ) is the finest partition, (R n+m-1 , C n+m-1
) is the coarsest partition, and for every i

∈ [n + m -2], (R i+1 , C i+1 ) is a contraction of (R i , C i ).
Given a subset R of rows and a subset C of columns in a matrix M , the zone R ∩ C denotes the submatrix of all entries of M at the intersection between a row of R and a column of C. A zone of a partition pair (R,

C) = ({R 1 , . . . , R k }, {C 1 , . . . , C ℓ }) is any R i ∩ C j for i ∈ [k] and j ∈ [ℓ].
A zone is constant if all its entries are identical. The error value of R i is the number of non-constant zones among all zones in {R i ∩ C 1 , . . . , R i ∩ C ℓ }. We adopt a similar definition for the error value of C j . The error value of (R, C) is the maximum error value taken over all R i and C j . The twin-width of a matrix M is the minimum t for which there exists a contraction sequence of M consisting of partitions with error value at most t. In particular, the twin-width of matrices over finite alphabets extends the scope of twin-width from graphs to arbitrary binary structures over finite signatures. One may define the twin-width of a binary structure as the twin-width of the matrix canonically encoding that structure (by placing at row x column y a letter encoding the isomorphism type of (x, y), i.e., the atomic formulas satisfied by (x, y)).

In a contraction sequence of a matrix M , one can always reorder the rows and the columns of M in such a way that all parts of all partitions in the contraction sequence consist of consecutive rows or consecutive columns. To mark this distinction, a row-division is a row-partition where every part consists of consecutive rows; with the analogous definition for column-division. A (k, ℓ)-division (or simply division) of a matrix M is a pair (R, C) of a row-division and a column-division with respectively k and ℓ parts. A division sequence is a contraction sequence in which all partitions are divisions.

A matrix

M = (m i,j ) is vertical (resp. horizontal) if m i,j = m i+1,j (resp. m i,j = m i,j+1
) for all i, j. Observe that a matrix that is both vertical and horizontal is constant. We say that M is mixed if it is neither vertical nor horizontal. A crucial remark is that a matrix is mixed if and only if it contains a corner, i.e., a contiguous 2-by-2 mixed submatrix. A t-mixed minor in M is a division (R, C) = ({R 1 , . . . , R t }, {C 1 , . . . , C t }) such that every zone R i ∩ C j is mixed (hence contains a corner). A matrix without t-mixed minor is t-mixed free. The minimum t for which one can reorder the column and the rows of M to form a t-mixed free matrix is called the mixed value of M .

▶ Theorem 5 ([7]). Twin-width and mixed value are functionally equivalent for matrices.

Given a graph G and a permutation σ of its vertex set, we denote by Adj σ (G) the adjacency matrix of G in which the columns and the rows are ordered according to σ. As usual, given two vertices u, v, the entry Adj σ (G) u,v is equal to 1 if uv is an edge and 0 otherwise. By extension, we say that the mixed value of a graph G is the minimum t for which Adj σ (G) is t-mixed free, taken over all permutations σ. The link between mixed value and twin-width for graphs was proved in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF]:

▶ Theorem 6 ([7]
). Twin-width and mixed value are functionally equivalent for graphs.

Bounded expansion and tree-depth covers

We recall some definitions from a paper by Plotkin, Rao, and Smith [START_REF] Plotkin | Shallow excluded minors and improved graph decompositions[END_REF] and from the sparsity program of Nešetřil and Ossona de Mendez [START_REF] Nešetřil | Sparsity -Graphs, Structures, and Algorithms[END_REF]. One possible way of defining a minor of a graph G is by a collection of disjoint sets

B 1 , B 2 , . . . , B h ⊆ V (G), called branch sets, such that G[B i ] is connected for all i ∈ [h].
A minor of G is then any graph H, say on vertex set [h], such that ij ∈ E(H) implies that there is an edge in G with one endpoint in B i and the other endpoint in B j . A depth-r minor (also called r-shallow minor) of a graph G is a minor H of G obtainable in such a way that each branch set induces in G a subgraph with radius at most r. Let us denote by ∇ r (G) the set of all the depth-r minors of G. In particular ∇ r (G) is subgraph-closed. Given a non-decreasing function f : N → N, we say that a graph G has expansion f if for every r ∈ N, every graph H ∈ ∇ r (G) has (maximum) average degree at most f (r). A graph class C has expansion f if all its graphs have expansion f , and C has bounded expansion if it has expansion f for some function f . Note that saying that a graph has bounded expansion is meaningless (they all do, individually) but the fact that, for a specific function f , a single graph has expansion f is meaningful.

The tree-depth of a graph G is the minimum integer k such that there is rooted forest F of height k on vertex set V (G) with every edge of G being in an ancestor-descendant relationship in F . Bounded tree-depth is more restrictive than bounded tree-width, so in particular, bounded tree-depth graphs have bounded twin-width. There is a very useful connection between bounded tree-depth and bounded expansion, in the form of low tree-depth covers, or the related low tree-depth decompositions [START_REF] Nešetřil | Tree-depth, subgraph coloring and homomorphism bounds[END_REF][START_REF] Nešetřil | On low tree-depth decompositions[END_REF]. A low tree-depth cover with parameters

k, f of a graph G is a family of h = f (k) subsets X 1 , . . . , X h ⊆ V (G) such that, for every i ∈ [h], G[X i ]
has tree-depth at most k, and every subset of V (G) of size at most k is fully included in at least one X i . A graph class C has low tree-depth covers if there is a function f depending only on C such that for every G ∈ C and integer k, G has a low tree-depth cover with parameters k, f . ▶ Theorem 7 ([24, 27]). Let C be a monotone graph class. Then C has low tree-depth covers if and only if C has bounded expansion. Furthermore if C has bounded expansion, then there is a function f and an algorithm that given a graph G ∈ C and an integer k, outputs a low tree-depth cover of

G with parameters k, f in linear time O k,f (k) (|V (G)|).

Finite model theory

We recall some relevant background from finite model theory. We denote by FO τ and MSO τ the set of first-order, respectively monadic second-order, formulas on signature τ . In firstorder, every variable is interpreted as an element of the universe. In monadic second-order, a first-order variable is interpreted as an element, while a second-order variable is interpreted as a subset of the universe. We will mainly consider signatures consisting of unary and binary relation symbols only. Typically the signature τ will be one of the following:

{E}, where E is binary: the language of graphs with possible edge orientations and loops; {E, ∼}, where ∼ is interpreted as an equivalence relation: the language of graphs with an unlabeled partition; {E, U 1 , . . . , U d }, where U 1 , . . . , U d are unary relations interpreted as a partition of the universe: the language of colored graphs, or graphs with a labeled partition; {inc}, where inc is interpreted as a vertex-edge incidence relation of a graph. MSO {E} is usually denoted by MSO 1 , and MSO {inc} by MSO 2 , when a theory interprets inc as above. A sentence is a formula without free variables. A relational τ -structure A on universe A gives an interpretation R A ⊆ A r to every r-ary relation symbol R ∈ τ . A structure A is a model of a sentence φ, denoted by A |= φ, if φ holds when interpreted on A. We will only consider finite models where the universe A is a finite set. The FO model checking (resp. MSO model checking) asks given a τ -structure A and a sentence φ ∈ FO τ (resp. φ ∈ MSO τ ) whether A |= φ holds. The fragment ∃FO (existential first-order logic) consists of the formulas with no universal quantifier and all the negations pushed down to atomic formulas.

The Gaifman graph of a τ -structure A has vertex set its universe A, and edges ab whenever a and b appear in the same relation R A for some R ∈ τ . The quantifier rank (or quantifier depth) of a formula φ is the largest number of quantifiers that are nested in φ. FO τ [q] (resp. MSO τ [q]) denotes the set of formulas in FO τ (resp. MSO τ ) with quantifier rank at most q. When the signature is irrelevant or clear from the context, we may omit it, and simply write FO, MSO, FO[q], MSO [q].

If two finite τ -structures are not isomorphic, then there is a sentence that holds in one but not in the other (for instance the sentence that fully describes the former structure). However it is very well possible that two non-isomorphic τ -structures satisfy the exact same sentences of FO[q] or MSO[q], for some (finite) integer q. Ehrenfeucht-Fraïssé games characterize exactly when that happens. Initially the game was defined for first-order logic. We call it the EF game and start with its description. We will then present its extension MSO-EF for monadic second-order.

In the EF game, two players Spoiler and Duplicator confront each other over two τstructures A and B. They play a succession of rounds, when Spoiler wants to show that A and B are not isomorphic, whereas Duplicator tries to argue the opposite. The i-th round goes like this. Spoiler chooses a structure A or B, and picks one element in it, say a i ∈ A (or b i ∈ B). Duplicator answers by picking an element in the other structure, say b i ∈ B (resp. a i ∈ A). If after q rounds, a i → b i (for i ∈ [q]) is still an isomorphism between the induced substructures (A, =)[a 1 , . . . , a q ] and (B, =)[b 1 , . . . , b q ], we say that Duplicator has survived q rounds of the EF game.

We write A ≡ FO q B if Duplicator has a strategy such that she can survive (at least) q rounds. The Ehrenfeucht-Fraïssé theorem states that this is equivalent to A and B agreeing on all the sentences of FO τ [q]. ▶ Lemma 8 (Ehrenfeucht-Fraïssé, see Theorem 3.9 in [START_REF] Libkin | Elements of Finite Model Theory[END_REF]). Let A and B be two τ -structures. Then, A and B satisfy the same sentences of FO τ [q] if and only if

A ≡ FO q B.
The MSO-EF game is similar to the EF-game, but Spoiler can (in each round) alternatively decide to play a subset of A (or a subset of B), to which Duplicator answers with a subset of B (resp. of A). Now after q rounds, a tuple of e elements have been played in both A and B, say (a 1 , . . . , a e ) and (b 1 , . . . , b e ) in this order, as well as a tuple of s sets, say (A 1 , . . . , A s ) in A and (B 1 , . . . , B s ) in B, with q = e + s. Duplicator has survived these q B if Duplicator has a strategy allowing her to survive (at least) q rounds of the MSO-EF game. The same characterization holds for MSO and the MSO-EF game.

rounds if a i → b i (for i ∈ [e]) is an isomorphism between (A, =, A 1 , . . . , A s )[a 1 , . . . ,
▶ Lemma 9 (Ehrenfeucht-Fraïssé for MSO, see Corollary 7.8 in [23]). Let A and B be two τstructures. Then, A and B satisfy the same sentences of MSO τ [q] if and only if

A ≡ MSO q B.

From branch-decompositions to contraction sequences

We start this section by showing Theorem 1, that is, the functional equivalence between boolean-width (equivalently rank-width) and component twin-width, and between linear boolean-width and total twin-width.

Classical width parameters as contraction sequences

▶ Theorem 10. Boolean-width and component twin-width are functionally equivalent.

Proof. Let G be a graph. We first show that the component twin-width of G is bounded in terms of the boolean-width of G. This was essentially done in the first paper of the series [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], but only sketched and without the explicit notion of component twin-width.

Let T be a rooted branch-decomposition of G whose leaves are bijectively mapped to V (G), and assume that T has boolean-width at most d. We make a sequence of contractions G n , . . . , G ℓ such that the size of any red component in the trigraph sequence is at most 2 d+1 and G ℓ has at most 2 d+1 vertices. We may assume G n has at least 2 d+1 + 1 vertices, as otherwise we are done. Henceforth, a rooted branch-decomposition T j for each trigraph G j on at least 2 d+1 + 1 vertices is constructed along with the contraction sequence while the following invariant, which clarifies what we actually mean by branch-decomposition of a trigraph, is maintained:

(♣) For each node v of T j with |A v | ⩾ 2 d + 1, all edges of G j crossing (A v , V (G j ) \ A v ) are
black, and the boolean-width of the bipartition

(A v , V (G j ) \ A v ) is at most d.
The invariant (♣) clearly holds for G n = G and T n = T . Let G i+1 be a trigraph on i + 1 ⩾ 2 d+1 + 1 vertices and T i+1 be a rooted branch-decomposition for which (♣) holds. We construct G i and T i satisfying the invariant.

Observe that there exists a node v of T i+1 such that

2 d + 1 ⩽ |A v | ⩽ 2 d+1
; a node v such that A v has size at least 2 d + 1 and which is furthest from the root meets the condition. By Observation 4 and the second part of (♣) applied to v, there are two distinct vertices x, y of G i+1 , which belong to A v such that x, y have the same (black) neighborhood in V (G i+1 ) \ A v . Now contract x, y to yield G i . Let T i be a branch-decomposition of G i obtained by deleting y and identifying the node x to the new vertex of G i resulting from the contraction of x and y. Due to the choice of x, y and the first part of (♣) on i + 1, the edges between A v (of the new tree T i ) and V (G i ) \ A v are all black. This means that any bipartition of V (G i ) that can potentially contain a newly created red edge of G i must be associated with a strict descendant of v. By the definition of v, any strict descendant of v has at most 2 d leaves (both in T i+1 and T i ) and is thus out of the scope of the invariant (♣). Therefore, the first part of (♣) is maintained.

This also means that for any node u of T i , which is not a strict descendant of v, the bipartition (A u , V (G i ) \ A u ) associated with u is the same as the bipartition associated with u in T i+1 after deleting one vertex of G i+1 , namely y. Since the boolean-width of a bipartition does not increase after vertex deletion, we conclude that the second part of (♣) is maintained as well. Finally, we observe that the invariant (♣) indicates that G has component twin-width at most 2 d+1 since any red component of G i is included inside some A v with size at most 2 d+1 .

To see the other direction, let P n , . . . , P 1 be a partition sequence of G such that every connected component of the red graph G i has at most d vertices. Let P ′ i be the coarsening of P i such that each part of P ′ i corresponds to a red component of G i , i.e., is the union of parts of P i , which form a red component in G i . Slightly abusing the notation, we call a part of P ′ i a red component of P i . Let T n be a star tree rooted at its center r, whose n leaves are bijectively mapped to V (G). We will iteratively transform a rooted tree T i+1 to T i in a way that mirrors the merging of parts in P ′ i . The root r will be unchanged throughout the transformations. During iterative transformations we maintain the following invariants: i is a coarsening of P ′ i+1 (possibly P ′ i+1 = P ′ i ), that there is a unique red component C ∈ P ′ i , obtained as the union of some (possibly one) red components C 1 , . . . , C s of P ′ i+1 , and that P ′ i \ {C} = P ′ i+1 \ {C 1 , . . . , C s }. By the invariant (a), there are subtrees of T i+1 -r whose leaves are mapped to parts C 1 , . . . , C s of P ′ i+1 . Let t(C j ) be the root of the subtree of T i+1 -r corresponding to C j for j ∈ [s]. Now, we construct T i from T i+1 as follows: replace the edges connecting the root r and t(C j ) for j ∈ [s] by a subcubic tree rooted at t(C) with s leaves, whose root t(C) becomes the child of r and whose s leaves are identified (arbitrarily) with t(C j ) for j ∈ [s].

By the induction hypothesis and the construction of T i , the invariants (a)-(b) are maintained. Furthermore, since C = s i=1 C i , the red component C ∈ P ′ i consists of at most d parts of P i , thus at most d + 1 parts of P i+1 , and we have s ⩽ d + 1. To see that the boolean-width of T i is at most 2 d , it suffices to check that for all I ⊆ [s], the boolean-width of the bipartition ( j∈I C j , V (G) \ j∈I C j ) is at most 2 d . For a proper subset I of [s], we know that j∈I C j consists of at most d parts of P i+1 and each of these parts of P i+1 has the same neighborhood across the bipartition ( j∈I C j , V (G) \ j∈I C j ) since each C j is a red component. Hence, the vertex set j∈I C j has at most d vertices with distinct neighborhood across the bipartition and thus the boolean-width is at most 2 d . For I = [s], the same argument applies once it is noted that j∈I C j = C consists of at most d parts of P i .

As P ′ 1 = P 1 = {V (G)}, the invariants (a) and (b) at i = 1 imply that T 1 is a subcubic tree whose leaves are bijectively mapped to V (G). With the invariant (c), we conclude that T 1 and the bijection form a boolean decomposition of width at most 2 d . ◀ ▶ Theorem 11. Linear boolean-width and total twin-width are functionally equivalent.

Proof. Let G be a graph. We first bound total twin-width in terms of linear boolean-width.

Let T be a linear branch-decomposition of G (i.e., in which the internal nodes form a path P ) with boolean-width at most d. We root T at an internal node that is an endpoint of the path P . We follow the same proof as for Theorem 10 and observe that every tree T i is now a linear branch-decomposition. Indeed, the linearity of T i implies that there is a unique choice of a minimal rooted subtree of T i with at least 2 d + 1 leaves. Moreover, the invariant (♣) of Theorem 10 means that the endpoints of any red edge are restricted to the leaves of this subtree. Note that there are at most 2 d + 1 + 2 d +1 2 red edges in any G i . Let P n , . . . , P 1 be a partition sequence of G achieving total twin-width at most d. Let V i ⊆ V (G) be the union of all non-singleton parts of P i . As every red edge which is not a loop has at least one endpoint with a loop, at most d parts of P i are incident to red edges. Note that V i \ V i+1 has at most two vertices, and it has two vertices only when we contract two singleton parts. Consider now any total order

≺ on V (G) such that u ≺ v if there exists i ∈ [n] with u ∈ V i and v / ∈ V i . Indeed, we have V n-1 ≺ V n-2 \ V n-1 ≺ • • • ≺ V 2 \ V 3 ≺ V 1 \ V 2
. Now consider the linear branch decomposition T corresponding to ≺ and we argue that the boolean-width of T is bounded by d. Every bipartition corresponds either to a cut

(V i , V (G) \ V i ) or to (V i ∪ {v}, V (G) \ (V i ∪ {v})) for some v ∈ V i \ V i+1 .
Observe that each non-singleton part of P i is entirely contained in V i . Moreover, each red edge crossing the cut incident with a non-singleton part P ∈ P i multiplies the number of equivalence classes in V i by a factor of 2, where each class has the same neighborhood across the cut. This implies that the number of equivalence classes in V i is at most 2 d-1 + 1 ⩽ 2 d . Therefore, with Observation 4 we deduce that the boolean-width of T is at most 2 d . ◀

Here again, we can find equivalent parameters in the sparse regime:

▶ Theorem 12. In the class of K t,t -free graphs: tree-width and component twin-width are functionally equivalent. path-width and total twin-width are functionally equivalent.

Note that if we do not add red loops to contracted vertices, linear rank-width and total twin-width are not equivalent because of cographs. Indeed, still without red loops, there is always a contraction sequence that produces no red edge at all: iteratively contract two twins. However cographs have unbounded linear rank-width (this folklore fact can be derived from the unboundedness of linear rank-width for trees [START_REF] Adler | Linear rank-width and linear clique-width of trees[END_REF]). Thus the addition of loops may seem a bit artificial and even made to force the equivalence. There is however a good reason for loops: From the adjacency-matrix viewpoint (which is both used for rank-width and twin-width), the main diagonal represents equality, a different predicate than the edge (or non-edge) predicate.

Alternative proof of Courcelle's theorems

We will give an alternative proof to the celebrated result by Courcelle, Makowsky, Rotics [START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF] that MSO 1 model checking can be solved in linear time on bounded clique-width graphs, given with an O(1)-expression. This generalizes the original Courcelle's theorem [START_REF] Courcelle | The monadic second-order logic of graphs. I. Recognizable sets of finite graphs[END_REF] that MSO 2 model checking can be solved in linear time on bounded tree-width graphs. Indeed MSO 2 is not more expressible than MSO 1 on graphs of bounded tree-width [11, Theorem 9.37], and there is a linear-time FPT algorithm returning a tree-decomposition of optimal width [START_REF] Hans | A linear-time algorithm for finding tree-decompositions of small treewidth[END_REF]. We observe that there are other alternative proofs to the central result of Courcelle, Makowsky, Rotics; for instance, one based on automata [START_REF] Ganian | On parse trees and myhill-nerode-type tools for handling graphs of bounded rank-width[END_REF], and one game-theoretic [START_REF] Langer | Linear-time algorithms for graphs of bounded rankwidth: A fresh look using game theory[END_REF]. Let us also mention that the incoming presentation does not follow the exposition of the first-order model checking algorithm in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], but rather its streamlined revisitation by Gajarský, Pilipczuk, Reidl, and Toruńczyk [START_REF] Gajarský | personal communication[END_REF].

We call MSO rank-q type (or type for short) any set of sentences mso-tp q (G) :

= {φ ∈ MSO {E} [q] : G |= φ}
where G is a graph, and we recall, MSO {E} [q] denotes the set of MSO sentences on a signature with a single binary relation E, and quantifier rank at most q. Then mso-tp q (G) is called the MSO rank-q type of G, or type of G for short. We fix a positive integer d, upperbounding the component twin-width on the class we want to tackle. We call local MSO rank-q partitioned type (or local partitioned type for short) any set of sentences loc-mso-tp q,d (G,

P o , C) := {φ ∈ MSO {E,U1,...,U d } [q] : (G[C], P o [C]) |= φ}
where G is a graph with a labeled vertex partition P o , and C ⊆ V (G) is the set of initial vertices of G landing in a same red component D with at most d parts. The unary relations U 1 , . . . , U d are interpreted as the labeled partition

P o [C] of G[C]. Thus some U d ′ +1 , U d ′ +2 , . . . , U d may possibly be empty if P o [C] has d ′ < d parts.
We use the superscript o (for ordered) for the labeled partition P o since we will usually fix the labeling by giving an ordering of the parts. The (unlabeled) vertex partition P stands for P o ignoring the labels. We may sometimes identify C with the red component D.

It is not difficult to show that there are only finitely many MSO sentences of quantifier rank q on finitary signatures, up to logical equivalence (see for instance [START_REF] Libkin | Elements of Finite Model Theory[END_REF]Proposition 7.5]). Furthermore there is an algorithm (running in time function of q and signature τ only) that lists all the sentences of depth q, up to logical equivalence. Therefore the number of (local) MSO rank-q (partitioned) types is bounded by a function of q and d only. A superset of the (local) MSO rank-q (partitioned) types can be listed in time function of q and d only, by listing all the subsets of sentences of depth q. Instead of deciding G |= φ for a particular sentence φ with quantifier rank q, we will compute mso-tp q (G). By the previous observation, this allows to decide G |= φ for every sentence φ with quantifier rank q (by simply checking if φ ∈ mso-tp q (G)) in constant time, if q and d are treated as a constant.

The algorithm will only compute local partitioned types. Note that for an n-vertex graph G with a partition sequence P n , . . . , P 1 , loc-mso-tp q,d (G, P o n = {{v} : v ∈ V (G)}, C) is easy to determine, with any labeling P o n of P n , since G/P n is isomorphic to the graph G and each possible C is a singleton {w} (for some w ∈ V (G)). Thus these local partitioned types all coincide to the one of the 1-vertex graph with its unique labeled partition. Furthermore loc-mso-tp q,d (G, P 1 = {V (G)}, V (G)) matches5 mso-tp q (G), which is the set we are after.

Thus we only need to compute all the local partitioned types loc-mso-tp q,d (G, P o i , C) C from the knowledge of loc-mso-tp q,d (G, P o i+1 , C ′ ) C ′ . We will prove that this is possible since the local partitioned types, the contracted pair of parts (X, X ′ ), and the black edges of the quotient trigraph are enough to reconstitute the local partitioned type of the new red component containing X ∪ X ′ . We show that fact with the characterization via the Ehrenfeucht-Fraïssé game for MSO (see Lemma 9). Recall that given two input structures A, B, Duplicator has a strategy to survive q rounds of the MSO-EF game if and only if A and B satisfy the same sentences of MSO[q], hence have the same rank-q type. The subsequent Lemma 13 has a technical and lengthy pre-condition that we chose to state outside the lemma environment for the sake of legibility. It starts here.

Let (G 1 , (X 1 1 , . . . , X 1 ℓ1 )), . . . , (G k , (X k 1 , . . . , X k ℓ k )) be k graphs G j given with a labeled partition of size ℓ j . Let (H 1 , (Y 1 1 , . . . , Y 1 ℓ1 )), . . . , (H k , (Y k 1 , . . . , Y k ℓ k )) be such that (G j , (X j 1 , . . . , X j ℓj )) ≡ MSO q (H j , (Y j 1 , . . . , Y j ℓj )), for every j ∈ [k].
Let (G, P o ) be a graph with a labeled vertex partition made from the disjoint union

j∈[k] (G j , (X j 1 , . . . , X j ℓj ))
with parts labeled by the order σ, say,

(X 1 1 , . . . , X 1 ℓ1 , X 2 1 , . . . , X 2 ℓ2 , . . . , X k 1 , . . . , X k ℓ k ),
and adding the biclique between some pairs of parts X j h , X j ′ h ′ prescribed by a meta-graph B on vertex set P o .

The natural bijection ι :

X j h → Y j h (for j ∈ [k] and h ∈ [ℓ j ]
) allows to transpose σ and B to the union of the H j . Let (H, Q o ) be the graph with a labeled partition made from the disjoint union j∈ [k] (H j ,(Y j 1 , . . . , Y j ℓj )) with the parts labeled along ι(σ), and adding the bicliques prescribed by ι(B). Finally we distinguish two parts (the parts to be contracted) X, X ′ in P o , and we distinguish the homologous parts Y

:= ι(X), Y ′ := ι(X ′ ) in Q o . ▶ Lemma 13. (G, P o , X, X ′ ) ≡ MSO q (H, Q o , Y, Y ′ ).
Proof. The global strategy of Duplicator simply follows the corresponding local strategy if a vertex is played, and if a set S is played, the union of the local answers to each projection of S on the red components is replied.

More precisely, if Spoiler plays x s ∈ X j h (or y s ∈ Y j h ), then Duplicator answers y s ∈ Y j h (resp. x s ∈ X j h ) accordingly to her local strategy on (G j , (X j 1 , . . . , X j ℓj )), (H j , (Y j 1 , . . . , Y j ℓj )). Importantly we know that Duplicator replies a vertex of Y j h to a vertex of X j h played by Spoiler, since otherwise the local unary relation U h over G j contradicts the partial isomorphism ensured by (G j , (X j 1 , . . . , X j ℓj )) ≡ MSO q (H j , (Y j 1 , . . . , Y j ℓj )). (Duplicator also remembers that moves (x s , y s ) have been added to the local j-th game, in case more moves are played there.) If Spoiler plays a set S p ⊆ V (G), Duplicator considers all the non-empty sets S p ∩ V (G j ) (for j ∈ [k]) and replies T p := j A j where A j is the local answer to S p ∩ V (G j ). Duplicator builds similarly an answer T p ⊆ V (H) to a move S p ⊆ V (G) by Spoiler.

Since (G j , (X j 1 , . . . , X j ℓj )) ≡ MSO q (H j , (Y j 1 , . . . , Y j ℓj )), the projection of the mapping x s → y s (for s indexing the vertex moves) onto G j , H j is a partial isomorphism between the two corresponding local structures. Since there is the same (black) graph B on the parts of P, as ι(B) on the parts of Q, there is an edge in G between x s ∈ X j h and x s ′ ∈ X j ′ h ′ if and only if there is an edge in H between y s ∈ X j h and x s ′ ∈ X j ′ h ′ . For every s and p, x s ∈ S p if and only if y s ∈ T p otherwise the moves (x s , y s ) and (S p ∩ V (G j ), T p ∩ V (H j )), played in some order, where x s ∈ V (G j ) would make Duplicator lose the local j-th game. Finally since the parts X, X ′ and Y, Y ′ are homologous (under the bijection ι), x s ∈ X (resp. x s ∈ X ′ ) if and only if y s ∈ Y (resp. y s ∈ Y ′ ). Otherwise we already observed that (x s , y s ) would have been a losing pair of moves for Duplicator in the corresponding local game. Thus the mapping x s → y s (for s indexing the vertex moves) is a partial isomorphism between (G, P o , X, X ′ ) and (H,

Q o , Y, Y ′ ).
◀ By Lemma 9, we have just established that the local partitioned type of a new red component C ′ obtained by the merge of two parts X, X ′ is function of the local partitioned type of every component C 1 , . . . , C ℓ ending up in C ′ after the contraction, the contracted pair (X, X ′ ), and the transversal black edges (bicliques) linking some pairs of parts in two distinct C i 's.

The crucial place where the upper bound d on the component twin-width comes into play is in the time that the update from loc-mso-tp q,d (G, P o i+1 , C ′ ) C ′ to loc-mso-tp q,d (G, P o i , C) C takes. Let Z ∈ P i be the result of the merge of the two parts X, X ′ ∈ P i+1 . Since all the red components have size at most d, the set Z is in a red component with a set Q of at most d -1 other parts of P i . The black edges in G/P i+1 on the vertex subset Q ′ := {X, X ′ } ∪ Q, the pair of parts (X, X ′ ), and the local partitioned type of each red component within Q ′ , account for less than 2 ( d+12 ) d+1 2 (d + 1)f (q) outcomes, for some function f . Thus the transition table giving the new local partitioned type can be precomputed in time depending only on d and q. (The red components of G/P i not containing Z do not need an update.) Treating d and q as constant, the update takes constant time, and the overall algorithm, O(n) time.

If the partition sequence is not given with the input graph, we rely on an algorithm approximating rank-width [START_REF] Oum | Approximating rank-width and clique-width quickly[END_REF] to find the sequence. Our proof looks like the original one by Courcelle, Makowsky, Rotics [START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF], except it does not need to use transductions to deal with the label-joins and relabelings of the clique-width expression. Instead everything is concentrated in Lemma 13, a statement similar to the Feferman-Vaught theorem [START_REF] Feferman | The first order properties of products of algebraic systems[END_REF], which is invoked in [START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF] to handle the disjoint union of two labeled graphs.

It is known that every MSO transduction of a class of bounded clique-width has itself bounded clique-width [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics and its applications[END_REF]. This fact alternatively follows from the above algorithm combined with the same arguments as used to show that any FO transduction of a class of bounded twin-width has bounded twin-width [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF].

Extensions. This approach can also be used to the solve optimization versions of MSO. Say, we want to maximize the size of a set S ⊆ V (G) such that G |= ψ(S) for some formula ψ(X) with one free set variable and quantifier rank q. We now consider the local MSO rank-q partitioned (0,1)-type (same as before but for formulas with one free set variable), or local partitioned 1-type, for short:

loc-mso-tp q,d (G, P o , C, S) := {φ(X) ∈ MSO {E,U1,...,U d } [q] : S ⊆ C, (G[C], P o [C]) |= φ(S)}.
The number of distinct such types is again upperbounded by a function of d and q only, although S may be any subset on up to |V (G)| vertices. Thus, any fixed triple (G, P o , C) defines an equivalence relation S ∼ S ′ ⇔ loc-mso-tp q,d (G, P o , C, S) = loc-mso-tp q,d (G, P o , C, S ′ ) with g(d, q) classes for some computable function g. The initialization is still straightforward. The updates merge maximum-cardinality vertex subsets each realizing some prescribed type, indeed producing a largest vertex subset for the resulting type. The proof follows again from Lemma 13, where one now adds a unary relation which may arbitrarily overlap with the partition P o .

Finally, any finitary logic for which Lemma 13 still holds, like CMSO (i.e., MSO with additional modular counting predicates, interpreted as "the size of a set is p modulo q" for some fixed integers p, q), also admits a tractable model checking algorithm following the same arguments.

Simpler algorithm for a particular MSO 1 problem: q-Coloring

Like for tree-width and clique-width, one can design more practical algorithms for particular MSO-expressible problems, when the component twin-width is bounded, still utilizing the viewpoint of contraction sequences. This gives rise to a different dynamic-programming scheme than the one on tree-decompositions or on clique-width expressions. It comes naturally positively-instance driven [START_REF] Tamaki | Positive-instance driven dynamic programming for treewidth[END_REF], that is, generating only positive subproblems. This is known to have significantly sped up some exact algorithms, as the computation of tree-width and tree-decompositions (see again the work of Tamaki [START_REF] Tamaki | Positive-instance driven dynamic programming for treewidth[END_REF]). The approach by contraction sequences has other advantages that we will list after we give a particular example. ▶ Theorem 14. Given an n-vertex graph G and a contraction sequence G = G n , . . . , G 1 witnessing that its component twin-width is at most d, the q-Coloring problem can be solved in time O((2 q -1)

d d 2 n). Proof. If C ⊆ V (G i ) is a red component, that is, a connected component in the red graph of G i , we denote by C(G) the set u∈C u(G). A q-coloring profile (or profile for short) of C is a function γ : V (C) → 2 [q] \ {∅} such that there is a proper q-coloring c of G[C(G)] satisfying, for every u ∈ C, that c(u(G)) = γ(u).
Thus γ gives the exact set of colors used by a (contracted) vertex of the red component. We will maintain for each red component C the complete set of profiles of C. Description of the algorithm. Initially in G n , there are n red components isomorphic to the 1-vertex graph. Thus for each u ∈ V (G), we store the set of profiles {u → {1}, u → {2}, . . . , u → {q}}. This corresponds to the q ways a vertex can be colored. Eventually in G 1 , if there is a profile for the unique red component (again a 1-vertex graph), it means that G is q-colorable.

We shall just update the profiles as the red components evolve. Let u, v be the vertices contracted into a vertex z when going from G i+1 to G i . Let C be the red component of G i containing z, and

C 1 , . . . C d ′ be the red components in G i+1 such that C = j∈[d ′ ] C j \ {u, v} ∪{z}. Since |C| ⩽ d, it holds that | j∈[d ′ ] C j | ⩽ d + 1, and in particular d ′ ⩽ d + 1. Say that u ∈ C a and v ∈ C b .
The update only consists of computing a set of profiles for C (and destroying the set of profiles of C 1 , . . . , C d ′ ). For every γ 1 , . . . , γ d ′ in the profile set of C 1 , . . . , C d ′ , respectively, we check in time O(d 2 ) is there is a black edge between a pair x ∈ C j , y ∈ C j ′ with γ j (x) ∩ γ j ′ (y) ̸ = ∅. If there is no such edge, we add the corresponding union profile γ to the profile set of C, i.e., γ(z) = γ a (u) ∪ γ b (v), and γ(x) = γ j (x) if x ̸ = z and x ∈ C j . This finishes the description of the algorithm.

Correctness and running time. The correctness comes from the invariant that every red component is associated to its set of profiles. Indeed a black edge between xy ∈ E(G i ) means that there is a biclique between x(G) and y(G), thus these sets cannot use a shared color. The running time is as indicated since

j∈[d ′ ] #profile(C j ) ⩽ j∈[d ′ ] (2 q -1) |Cj | = (2 q -1) j∈[d ′ ] |Cj | = (2 q -1) d+1 ,
where #profile(C j ) is the number of profiles of red component C j . To actually compute a coloring, one can simply augment profiles with one representative coloring. ◀

Advantages. Assuming the SETH, 6 this new approach will for instance not improve the theoretically best algorithm for q-Coloring parameterized by clique-width, since Lampis showed that running time O * ((2 q -2) cw ) is achievable and essentially optimal [START_REF] Lampis | Finer tight bounds for coloring on clique-width[END_REF]. However our algorithm presents some practical advantages.

The first remarkable feature is its simplicity. Contrary to dynamic programming on clique-width expressions, which has to deal with unions, joins, and relabelings (or treedecompositions with their forget, introduce, and join internal nodes), we have only one operation to handle: the contraction of two vertices, where all optimization efforts can be invested. We have only n -1 operations in total, while tree-decompositions and clique-width parse trees typically have O(n) nodes, incurring a multiplicative overhead.

We do not maintain partial solutions that turn out to be locally infeasible. When a red component C has at least one profile, we know that G[C(G)] is q-colorable. On the contrary, in the usual algorithm parameterized by clique-width, a join between two labels sharing at least one color can happen long after the corresponding vertices were introduced. This causes to maintain a lot of unnecessary partial solutions.

Oriented twin-width

Oriented twin-width is "fairer" than twin-width in the following sense: In the partition sequence, when merging two parts X, Y of P i+1 to form P i , the only red arcs of D i that are created are directed from X ∪ Y . Indeed, if Z is homogeneous to X and to Y , it is also homogeneous to X ∪ Y . Thus any error due to a contraction is only attributed to the contracted vertices and does not wildly spread to their neighbors. This locality of error makes one's life much easier when designing partition sequences. Let us illustrate why. Given a graph G and two non necessarily adjacent vertices x, y, we denote by G/{x, y} the graph obtained by contracting x, y into one vertex {x, y} and joining it to all neighbors of x and y in G. We say that a class C of graphs is d-contractible if for every graph G of C there are two vertices x, y such that G/{x, y} is also in C and is such that the degree of {x, y} in the resulting graph is at most d. For instance the following lemma due to Norine et al. [START_REF] Norine | Proper minor-closed families are small[END_REF] implies that K t -minor free graphs are 2 Õ(t) -contractible, where Õ(t) = O(t) log k (t) for some fixed k.

▶ Lemma 15 (Lemma 2.2. in [START_REF] Norine | Proper minor-closed families are small[END_REF]). Let G be a K t -minor free graph, for some integer t ⩾ 3. Then there are two vertices u, v ∈ V (G), both of degree 2 Õ(t) , that are either false twins or adjacent.

Moreover, by a direct application of the discharging Kotzig [START_REF] Kotzig | Contribution to the theory of eulerian polyhedra[END_REF] could show that planar graphs are 9-contractible (and the bound is attained by the so-called stellated icosahedron).

▶ Lemma 16. For every integer d, every d-contractible class of graphs C has oriented twin-width at most d.

Proof. Let G be a graph on n vertices in C and x, y two vertices such that G/{x, y} is in C and {x, y} has degree at most d. To start the partition sequence, consider P n-1 consisting of singletons and part {x, y}. Note that the only red arcs created by the contraction stem from {x, y}, yielding out-degree at most d in D n-1 (recall Section 2.2). We inductively iterate the argument on G/{x, y} to form a partition sequence in which every vertex in D i has out-degree at most d. ◀

In particular, K t -minor free graphs have oriented twin-width 2 Õ(t) , and planar graphs have oriented twin-width at most 9.

Is bounded oriented twin-width a new notion? Surprisingly, the answer turns out to be negative. This is quite fortunate since it allows for more flexibility when looking for contraction sequences: One may just worry about the red out-degree. In contrast with the easy arguments above, the original proof that proper minor-closed classes have bounded twin-width [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] is quite tedious, involving a carefully chosen depth-first-search tree. Up to our knowledge, no classic result on minor-closed classes directly implies bounded twin-width.

▶ Theorem 17. Oriented twin-width and twin-width are functionally equivalent.

Proof. We already observed that a class with twin-width d has a fortiori oriented twin-width as most d. Moreover mixed value and twin-width are functionally equivalent for graphs by Theorem 6. Thus to show that 1. twin-width, 2. oriented twin-width, 3. mixed value are all functionally equivalent, we just need to argue that bounded oriented twin-width implies bounded mixed value. Actually this is similar to the proof that bounded twin-width implies bounded mixed value, which is done in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF]. We reproduce the arguments here for completeness.

We show the contrapositive. Let G be a graph with mixed value greater than 2d + 2, hence such that every adjacency matrix of G has a 2d + 2-mixed minor. Fix a partition sequence S = P n , . . . , P 1 of G. Let σ be a vertex ordering compatible with S. Let D = (R = {R 1 , . . . , R 2d+2 }, C = {C 1 , . . . , C 2d+2 }) be a 2d + 2-mixed minor of M := Adj σ (G). By design, the partition sequence S defines a symmetric division sequence over M since when merging two subsets of vertices, one can contract (simultaneously) the corresponding columns and the corresponding rows.

Recall that the vertices of the red directed graphs D i are subsets of vertices of G. Let ℓ be the maximum index such that a vertex of D ℓ fully contains a part P of D. Without loss of generality, we may assume that P is a column part, thus P = C j for some j ∈ [2d + 2]. As there is a corner in every cell M [R i , C j ] with i ∈ [2d + 2], there is in particular at least one row r i in each R i such that M [r i , C j ] contains two distinct values. In D ℓ , the d + 1 vertices v 1 , v 3 , . . . , v 2d+1 respectively corresponding to rows r 1 , r 3 , . . . , r 2d+1 are all in different parts, except possibly one pair v 2h-1 , v 2h+1 . Indeed as we performed a symmetric division sequence on M , and stopped the first time a part of the 2d + 2-mixed minor D was contained in a part of the sequence, there is at most one part R h that is contained in a part of P ℓ . (One may observe that D need not be symmetric, so h is not necessarily equal to j.) Thus the vertex of D ℓ corresponding to C j is the source of at least d red arcs. Therefore G has oriented twin-width at least d. ◀

Note that our proof of Theorem 17 shows that otww(C) ⩽ tww(C) ⩽ exp(exp(O(otww(C)))). It would be interesting to improve the bound given by the second inequality and/or to complement it by a lower bound. As a consequence, d-contractible classes have twin-width 2 2 O(d) , and K t -minor free graphs have twin-width 2 2 2 Õ(t) .

Partial contraction sequences to a target class

In this section, we present a couple of FO model-checking algorithms based on partial contraction sequences. It consists of pipelining the algorithm of [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] with other elements of the meta-algorithmic toolbox.

Partial sequences. For two non-negative integers d, ∆, let D d,∆ be the class of graphs admitting a partial d-sequence to a trigraph of total degree at most ∆. A class C is said to be collapsible to bounded degree if there are two integers d, ∆ such that C is included in D d,∆ . For a non-negative integer d and a non-decreasing function f : N → N, let E d,f be the class of graphs admitting a partial d-sequence to a trigraph whose total graph has expansion bounded by f . We refer the reader to Section 2.4 for the definition of expansion. A class C is said collapsible to bounded expansion if there is an integer d and a function f : N → N such that C is included in E d,f . Similarly we may say that a class C is collapsible to class C ′ if there is an integer d such that every graph G ∈ C has a partial d-sequence to a trigraph whose total graph is in C ′ .

The FO model checking algorithm in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF]. We will not need a full description of the algorithm. It is enough to recall the following. Let G n , . . . , G 1 be a contraction sequence of G, and P n , . . . , P 1 the corresponding partition sequence. Like the algorithm presented in this paper for MSO model checking in Section 3.2, we maintain the local theory of sentences of quantifier rank q rooted at each vertex u of each trigraph G i of the sequence. In the case of bounded component twin-width, the local theory was naturally limited to the red component of u. Now that the red graphs can have arbitrary large components, the local theory is limited to vertices at distance less than 3 q from u in the red graph of G i . Since the red degree is assumed to be bounded by d, this represents a set, say, S q,d (u) of less than d 3 q vertices. In [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] the local theory is not materialized by types but by a tree (called reduced morphismtree), denoted here by T q,d (u), of depth q and total size function of q only, containing all the possible games in the partitioned graph (G, P i )[ v∈S q,d (u) v(G)] up to equivalent moves. More precisely, the root of T q,d (u) is labeled by the empty sequence, and every child adds a new vertex of v∈S q,d (u) v(G) (new move) to the current sequence (branch from the root to the current node). At this stage, it is not determined yet if a move is played by ∃ or ∀ player. One can define by induction what two equivalent moves are. At the level of leaves (depth q) two equivalent moves are siblings defining the same induced substructures in (G, P i )[ v∈Sq(u) v(G)] (with equality). Then two sibling internal nodes are equivalent if there is a bijection between their children such that the paired children would be equivalent if they had the same parent.

Initially, the tree T q,d (v) for each vertex v ∈ V (G n ) = V (G) is easy to compute: it is a path of length q where the only possible move is v. The tree T q,d (u) when u is the unique vertex of G 1 is enough to decide G |= φ for every sentence φ with quantifier rank k. Indeed such sentence can be effectively rewritten as a prenex7 sentence of depth q := Tower(k + log * k + 3) [31, Theorem 2.2 and inequalities [START_REF] Plotkin | Shallow excluded minors and improved graph decompositions[END_REF]]. As usual the crux of the algorithm is how to update the trees T q,d (u) after one contraction is performed. Per tree, this takes time function of q and d only, while at most d 3 q trees may require an update after one contraction; hence the overall running time of f (d, q)n for some computable function f . We will however not need to detail how the update is done.

Algorithms based on partial sequences. We first observe that we can pipeline the FO model checking algorithm on graphs given with a (complete) O( 1)-sequence, developed in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], with Gaifman's locality theorem. Thus, given a corresponding partial sequence, FO model checking is FPT on collapsible classes to bounded degree. We recall Gaifman's locality theorem. An r-local formula with one free variable is a formula ϕ(x) such that ∀A, a:

A |= ϕ(a) if and only if A[N r A [a]] |= ϕ(a), where N r
A [a] is the r-neighborhood of a, that is, the set of elements at distance at most r from a in the Gaifman graph of A.

▶ Theorem 18 (Gaifman's Locality Theorem [START_REF] Gaifman | On local and non-local properties[END_REF]). For every positive integer q, there are computable integers k and r such that every FO sentence φ with quantifier rank q is equivalent to a Boolean combination of sentences of the form

∃x 1 . . . ∃x k 1⩽i<j⩽k d(x i , x j ) > 2r ∧ 1⩽i⩽k ϕ(x i )
where ϕ(x) is an r-local formula.

In the previous statement, d(x i , x j ) > 2r is a short-hand for the fact that there is no path of length at most 2r between x i and x j .

▶ Theorem 19. Given G ∈ D d,∆ with a partial sequence G = G n , . . . , G s such that G s has total degree ∆, and a sentence φ ∈ FO E [k], one can decide whether G |= φ in time f (d, ∆, k)n for some computable function f .
Proof. We run the algorithm of [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] on the partial sequence G n , . . . , G s with a small nuance. When the total degree of a vertex u ∈ V (G i ) becomes at most ∆, we turn all its black incident edges into red. We denote this new trigraph G ′ i and proceed to the next contraction on G ′ i (not G i ). By that process, the red degree may exceed d but remains bounded by d + ∆ (in the extreme case when ∆ black edges were turned red). We thus maintain trees T q,d+∆ (u), with q function of k as given in Theorem 18. When we reach the trigraph G ′ s , by design all its edges are red, since its total degree is at most ∆. We may therefore interpret G ′ s as a mere graph. Up to this point the algorithm takes time g(d, ∆, q)(n -s) for some computable function g.

To apply Gaifman's locality theorem directly, we adopt the partition viewpoint on the contraction sequence. Recall that there is a partial partition sequence P n , . . . , P s corresponding to the partial trigraph sequence G n , . . . , G s . We consider the structure

A := (G, P s , D := {ab : a ∈ u(G), b ∈ v(G), uv ∈ R(G ′ s )})
. We add the "dummy" graph D so that the Gaifman graph of A is simply a blow-up of the Gaifman graph of G ′ s . We apply Theorem 18 with r = 3 q on FO E,∼,D sentences that are not using the relation D. The tree T q,d+∆ (u) for every u ∈ V (G ′ s ) allows us to determine every such r-local sentence ϕ(x) of quantifier rank at most q. We can therefore mark the vertices u ∈ V (G ′ s ) such that ϕ(a) holds for at least one vertex a ∈ u(G). This takes time linear in s. We conclude as in the FO model-checking algorithm for bounded-degree structures of Seese [START_REF] Seese | Linear time computable problems and first-order descriptions[END_REF], by observing that finding a 2r-scattered set of size k (i.e., k vertices pairwise at distance more than 2r) among the marked vertices in the graph G ′ s can be done in time h(k, r)s for some computable function h (with a bounded search tree). Hence the overall running time. ◀ Typical graphs collapsible to bounded degree -but of unbounded twin-width and unbounded degree-are blow-ups (replace every vertex by a clique module of arbitrary size) of bounded-degree graphs; and more generally any modular decomposition where all the modules have bounded twin-width, while the core has bounded degree. We believe that Theorem 19 should hold more generally for collapsible classes to bounded expansion. We will only show the result for existential first-order sentences.

▶ Theorem 20. Given G ∈ E d,g with a partial sequence G = G n , . . . , G s such that the total graph of G s has expansion g, and a sentence φ = ∃x 1 ∃x 2 . . . ∃x q ψ ∈ ∃FO E [q] with ψ a quantifier-free formula, one can decide whether G |= φ in time f (d, g, q)n for some computable function f . Proof. We run the algorithm of [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] on the partial sequence G n , . . . , G s . When we reach G s , we compute a low tree-depth cover X 1 , . . . , X h of the total graph G ′ s of G s with parameters h, f = f (E d,g ) such that, we recall, G ′ s [X j ] has tree-depth at most q for every j ∈ [h], every subset of V (G ′ s ) of size at most q is fully contained in at least one X j , and h = f (k) Theorem 7. As G ′ s [X j ] has tree-depth at most q for every j ∈ [h], it has twin-width bounded by a function of q, and a (complete) f ′ (q)-sequence can be found in polynomial time for some function f ′ . For every j ∈ [h], we perform the following run. We trim all the trees T q,d (u) with u ∈ V (G s ) by deleting every move that is not in X j (and its subtree). We resume the algorithm of [START_REF] Bonnet | Twin-width II: small classes[END_REF] with the trigraph G s [X j ] and the twin-width bound set to f ′ (q).

If G |= φ indeed holds, let X j be such that G ′ s [X j ] contains q vertices (v 1 , . . . , v q ) such that G |= ψ(v 1 , . . . , v q ) (recall that φ is existential). The corresponding runs detects a solution. If G |= φ does not hold, every run is negative. The claimed overall running time is easy to derive. ◀ Theorem 19 tackles more general graph classes than the FO model-checking algorithm of [START_REF] Bonnet | Twin-width II: small classes[END_REF], combining the features of graphs with bounded twin-width and of sparse graphs. The interest of such algorithms might also be to ease the computation of the (partial) sequence. It is still unknown if there is an approximation algorithm outputting f (d)-sequences for graphs of twin-width at most d, in say, fixed-parameter time. A reason why this may be a delicate issue is that Ω(log n)-subdivisions of n-vertex graphs have bounded twin-width, while o(log n)-subdivisions do not [START_REF] Bonnet | Twin-width II: small classes[END_REF]. Furthermore the O(1)-sequences for Θ(log n)-subdivisions require arguments related to optimal sorting networks, which are difficult to conciliate with typical obstructions (like brambles, tangles, or grid minors) usually enabling to approximate width parameters. Now we observe that Ω(log n)-subdivisions are not an issue to compute partial O(1)-sequences to bounded degree or bounded expansion. Indeed there is a relatively easy argument for the former case (not involving sorting networks), whereas the latter case is immediate, the expansion being already bounded.

Spanning twin-width

Let ≼ be a partial order on a set X. When x ≼ y, we say that x is an ancestor of y, that y is a descendant of x, and that x, y are comparable. A forest order ≺ on X is a partial order such that whenever x, y ≼ z, then x, y are comparable. A tree order is a forest order with a minimum element. We write x ≺ c y when x ≺ y and there is no z such that x ≺ z ≺ y. The binary relation (X, ≺ c ) is the Hasse diagram of ≼. Notice that the Hasse diagram of a tree order is a directed tree.

Let G be a connected graph. A tree order ≼ on V (G) is compatible with G if uv is an edge of G whenever u ≺ c v. Put in another way, a tree order compatible with G can be seen as the transitive closure of some oriented rooted spanning tree of G.

Adding a tree order to a graph can help to design partition sequences. For instance, the key ingredient in the proof of [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] that minor-closed classes have bounded twin-width lies in the fact that if G is K t -minor free, then it has a tree order ≼ (a kind of Lex-DFS) such that (G, ≼) seen as a binary structure has bounded twin-width. This is one appealing feature of twin-width: One often has to guess which additional information will guide the sequence. Here the tree order can be seen as an intermediate step between the mere graph G and the full partition sequence.

In order to refine the landscape between bounded tree-width and bounded twin-width, a natural candidate is the spanning twin-width of a connected graph G, defined as the minimum twin-width of (G, ≼) taken over all tree orders ≼ compatible with G. We extend the notion to disconnected graphs by taking the maximum over all connected components. Observe that this parameter is not monotone. Indeed the spanning twin-width of a subgraph (even induced) can be larger than the one of the host graph. Nevertheless for monotone classes, it exactly captures classes excluding a minor. ▶ Theorem 21. A monotone graph class C has bounded spanning twin-width if and only if there exists some t such that no graph in C admits K t as a minor.

Proof. As already mentioned, the backward implication is proved in [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF] using a Lex-DFS. To show the forward direction, we exhibit graphs in C with arbitrarily high spanning twin-width. Here an induced subdivision of a graph H is any graph obtained from arbitrarily subdividing the edges of H (including the possibility of not subdividing the edge and just keeping it). Proof of the Claim: To see this, observe that if H is a cubic graph on t vertices and G contains a K t minor, then G contains a minor that contains H as a subgraph. Consider then an edge-minimal subgraph G ′ of G that contains a minor, itself containing H as a subgraph and observe now that G ′ is exactly an induced subdivision of H. ♢

We will now rely on the notion of first-order (FO) transductions. In general, a transduction transforms a class of structures into a class of structures, applying some rules definable in first-order logic. Here we only need a special case of transductions so we give a simplified definition. A (non-copying) FO transduction T of a graph G in a relational structure A consists of augmenting A with a constant number of unary relations, and then defining the vertex set and edge set of G by means of two first-order formulas with one and two free variables, respectively, in the vocabulary of A augmented with the unary relations. Since the interpretation of the added unary relations can be arbitrary, T(A) is not a single graph G but a set of them. A graph class C is a transduction in a class S of relational structures if C ⊆ A∈S T(A). Importantly bounded twin-width is preserved by applying FO transductions [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF]: If C is a transduction in a class of binary structures with bounded twin-width, then C itself has bounded twin-width.

Our strategy is to show that if an induced subdivision S of a (connected) cubic graph H is given together with a tree order ≼, then one can retrieve H from (S, ≼) using a fixed FO transduction. Since FO transductions keep twin-width bounded [START_REF] Bonnet | Twin-width I: tractable FO model checking[END_REF], the assumption that C has bounded spanning twin-width would directly imply that the class of cubic graphs has also bounded twin-width, which is false [START_REF] Bonnet | Twin-width II: small classes[END_REF].

We only have to show how to recover H from (S, ≼). FO transductions allow to introduce a bounded number of unary relations, so we can first identify the set V of vertices of S that have degree 3 (which are the original vertices of H). The technical task is now to decide if two such vertices x, y ∈ V are joined or not in H. This is the case if and only if there is an induced path x = u 0 , . . . , u ℓ = y of S such that all internal vertices are not in V . We denote this path by P . Note that when ℓ = 1 querying the existence of such a path can be directly done by asking if xy is an edge of S. Let us focus on the case when we want to retrieve an edge xy, which has been subdivided at least once, i.e., let us see how the tree order can help to retrieve the edge xy when ℓ > 1.

As ≼ is a tree order compatible with S, xy is an edge of H that is subdivided if and only if one of the following holds for P :

1. u 0 ≺ c • • • ≺ c u ℓ , 2. u 0 ≻ c • • • ≻ c u ℓ , or 3. there exists i ∈ [ℓ -1] such that u 0 ≺ c • • • ≺ c u i and u i+1 ≻ c • • • ≻ c u ℓ . 4. there exists i ∈ [ℓ -1] such that u i ≺ c • • • ≺ c u 0 and u i ≺ c • • • ≺ c u ℓ
(exceptional case when u i is the root of the tree-order).

there exists

i ∈ [ℓ -1] such that u i ≺ c • • • ≺ c u 0 and u ℓ ≺ c • • • ≺ c u i+1
(exceptional case when u i is the root of the tree-order).

there exists

i ∈ [ℓ -1] such that u i ≺ c • • • ≺ c u ℓ and u 0 ≺ c • • • ≺ c u i-1
(exceptional case when u i is the root of the tree-order).

Since all these conditions can be tested with a (long but bounded) first-order formula, H is a first-order transduction of (S, ≺). ◀

An interesting direction would be to investigate which hereditary classes have bounded spanning twin-width, as it could indicate some possible generalization of minor-closed classes to the dense setting. But even sparse hereditary classes C with bounded spanning twin-width are somewhat mysterious. For instance, the induced subgraphs of the grid with added diagonals (a non-planar graph), where two edges are added in each facial C 4 to form a K 4 , have bounded spanning twin-width (and arbitrarily large clique minors).

We believe that subdivisions of arbitrary cubic graphs could be the key in this study and that, for instance, any hereditary class of graphs with girth at least five avoiding any subdivision of a fixed cubic graph could have bounded twin-width (and maybe bounded spanning twin-width). In that direction, we suggest the following problem as a first step, where a segment graph is the intersection graph of segments in the plane.

▶ Conjecture 23. The class of segment graphs with girth at least five has bounded spanning twin-width.

We do not even know if this class has bounded twin-width.

Figure 1

 1 Figure 1 A 2-sequence witnessing that the initial graph has twin-width at most 2.

( a )

 a Twin-width: red degree. (b) Oriented twin-width: red out-degree. (c) Component twin-width: size of red components. (d) Total twin-width: number of red edges.

Figure 2

 2 Figure 2 Examples of graphs with low value of the four corresponding twin-width variants.

  a e ] and (B, =, B 1 , . . . , B s )[b 1 , . . . , b e ]. Similarly we write A ≡ MSO q

  (a) The leaves of each connected component of T j -r are mapped to each part of P ′ j . (b) The root r has as many children as |P ′ j | and all other internal nodes have two children. (c) For every edge of T j , the associated bipartition has boolean-width at most 2 d . The invariants (a)-(c) clearly hold for j = n. Suppose T n , . . . , T i+1 satisfy the invariants (a)-(c), with i ∈ [1, n -1]. Notice that P ′

  For every partitioned graph (G[C], P o [C]) induced by a red component, we keep only one representative S τ max ⊆ C per type τ = loc-mso-tp q,d (G, P o , C, S τ max ) such that for every S ⊆ C, S ∼ S τ max implies |S| ⩽ |S τ max |. That is, for each local partitioned 1-type associated to (G, P o , C), we keep a largest subset of C realizing that type.

▷ Claim 22 .

 22 If a monotone class C contains arbitrarily large clique minors, then C contains an induced subdivision of every cubic graph.

This phrases the classic width measures (tree-width, rank-width, path-width, linear

See the work of Eppstein[START_REF] Eppstein | Subgraph isomorphism in planar graphs and related problems[END_REF] building up on Baker's technique[START_REF] Baker | Approximation algorithms for NP-complete problems on planar graphs[END_REF] and leading to low tree-width decompositions, and[START_REF] Bonnet | Twin-width III: Max Independent Set, Min Dominating Set, and Coloring[END_REF] for the approach with contraction sequences.

The exact definition of spanning twin-width is somewhat technical and deferred to Section 6.

Strictly speaking loc-mso-tp q,d (G, P1 = {V (G)}, V (G)) is a superset of mso-tp q (G), but its projection to sentences ignoring the (trivial) labeled partition is exactly mso-tp q (G).

For Strong Exponential Time Hypothesis, the assumption that for every ε > 0, there is an integer k such that n-variable k-SAT cannot be solved in time (2 -ε) n by a classical algorithm.

A prenex formula or sentence has all its quantifiers as a prefix, followed by a quantifier-free formula.

Funding Eun Jung Kim: ANR-18-CE40-0025-01 (ASSK) by French National Research Agency.