B Courcelle
email: courcell@labri.fr

I Durand
email: irene.durand@u-bordeaux.fr

On using SAT solvers for graph computations

Determining the clique-width or the linear clique-width of an undirected graph reduces to a Boolean satisfiability problem, a SAT problem in short, that can be solved for graphs of moderate size, depending on the available solver. This method is due to Heule and Szeider. We extend it to directed graphs, to vertex-labelled graphs and to the computation of relative clique-width. We have checked that certain proved upper-bounds to clique-width are actually reachable. We also propose open questions about upper-bounds to clique-width that this approach may help to solve.

Every existential second-order graph property (it has an NP-algorithm) can be checked via a SAT problem. However, this problem may be much too large to be solved in practice. We consider particular existential second-order sentences from which SAT problems of polynomial size can be easily constructed and, furthermore, that define hereditary graph properties (preserved by induced graph inclusion) and Motivated by the search of minimal excluded graphs for hereditary graph properties (induced subgraph inclusion is here the relevant partial order), we examine cases where a SAT problem for an induced subgraph of a graph G can be obtained easily from the corresponding SAT problem for G.

Introduction: Checking whether a graph has clique-width at most k is an NP-complete problem [START_REF] Fellows | Clique-width is NP-Complete[END_REF] if k is part of the input. For fixed k ≤ 3, this problem is solvable in polynomial time. There exist polynomial time approximation algorithms [START_REF] Oum | Approximating rank-width and clique-width quickly[END_REF] but they output terms of too large width, hence that are not appropriate as inputs to model-checking algorithms based on automata [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

Heule and Szeider have designed a method for reducing the computation of the clique-width of an undirected graph to a Boolean satisfaction problem 1(a SAT problem in short) [START_REF] Heule | A SAT approach to clique-width[END_REF]. This reduction is available on-line through the software TRAG [START_REF] Courcelle | Online software TRAG[END_REF], which uses the SAT solver Glucose [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF]. By using it, we can compute the exact clique-width of graphs of, say, at most 25 vertices.

We extend this reduction to computing the clique-widths of directed graphs and of partially vertex-labelled graphs. We can also compute in this way the linear clique-width [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] and the relative clique-width [START_REF] Lozin | Rautenbach The relative clique-width of a graph[END_REF] of a directed or undirected graph.

The (exact) clique-width of undirected graphs is known from graph-theoretical proofs in relatively few cases: cographs (hence for cliques), cycles, trees and square grids [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]. It is known for particular graphs such as Petersen's graph and a few others by the computations reported in [START_REF] Heule | A SAT approach to clique-width[END_REF].

There are few results about the clique-width of directed graphs [START_REF] Bang-Jensen | Classes of directed graphs[END_REF]. In particular, tournaments have unbounded clique-width, but one does not know the maximal clique-width of a tournament with n vertices. We hope that our extension to directed graphs of the method of [START_REF] Heule | A SAT approach to clique-width[END_REF] will help.

We also present a few related open problems, about upper-bounds to the clique-width of directed and undirected graphs.

Every existential second-order graph property (it has an NP-algorithm) can be checked by reduction to a SAT problem. However, this problem may be much too large to be solved in practice. We define a class of existential second-order sentences that yield SAT problems of polynomial size2 and furthermore, define hereditary graph properties, i.e. properties preserved by taking induced subgraphs. These sentences have existential quantifications over relations applied to universally quantified first-order formulas. Motivated by the determination of minimal excluded graphs for hereditary graph properties, we show cases where a SAT problem that checks such a property for an induced subgraph of a graph G can be obtained easily from the corresponding problem for G.

Summary : Section 1 reviews terminology on graphs, Section 2 reviews clique-width, cographs and related notions, Section 3 defines Boolean satisfiability problems and gives examples, in particular to tree-width. Section 4 presents SAT problems for checking clique-width and linear clique-width of directed and undirected graphs. We introduce a generalization of relative clique-width and we show how its computation reduces to solving a SAT problem. The purpose is to obtain upper-bounds of clique-width based on guessed decompositions. In Section 5, we review open problems about the behaviour of clique-width under graph transformations. Section 6 develops a logical view intended to identify graph properties reducing to SAT problems of polynomial size in that of the given graph. Section 7 is a conclusion and Section 8 is an appendix containing a technical construction.

Graphs 1.Notation and a few definitions

We consider finite, simple, undirected or directed graphs G = (V, E) with vertex set V and set E of edges or arcs, i.e., of directed edges. Graphs have neither loops nor parallel edges or arcs. If G is directed, we write uv ∈ E if and only if there is an arc u → v. An undirected graph is defined as a symmetric graph, i.e., as a directed graph such that each arc u → v has an opposite arc v → u. Hence, uv ∈ E if and only if vu ∈ E. We denote by uv the existence of an edge between u and v.

If G = (V, E) is defined as directed, the associated undirected graph is Und(G) := (V, E ∪ E -1 ), where E -1 := {vu | uv ∈ E}. A directed graph H is an orientation of an undirected graph G if G = U nd(H) and H has no two opposite arcs u → v and v → u. We say then that H is an oriented graph. An orientation of a clique is a tournament.

The number of vertices is n. Vertex sets are frequently taken of the form [n] := {1, ..., n} with n ≥ 1.

A subgraph H of G is induced, denoted by H ⊆ i G, if every edge or arc of G whose ends are in H is in H. We denote by G[X] the induced subgraph of G with vertex set X.

A set of graphs closed under isomorphism is called a class. A set of graphs is finite up to isomorphism (finite u.t.i.) if the set of isomorphism classes of its graphs is finite.

G n×m denotes the rectangular undirected grid with n rows and m columns.

Hereditary properties and bounds

Definitions 1.1 : Hereditary properties and their bounds A graph property P is hereditary if P (G) =⇒ P (H) whenever H is an induced subgraph of G. In this case, the bounds of P are the graphs G that do not satisfy P whereas their induced subgraphs Gu := G[V -{u}] satisfy P . They are the ⊆ i -minimal excluded graphs of P or of the class of graphs that satisfy P . This terminology 3 comes from [START_REF] Daligault | Well-quasi-order of relabel functions[END_REF][START_REF] Fraïssé | Theory of relations[END_REF][START_REF] Pouzet | Un bel ordre d'abritement et ses rapports avec les bornes d'une multirelation[END_REF]. We denote by M inEx(P ) the class of bounds of P to recall its definition.

If M inEx(P ) is finite u.t.i, then Property P is first-order expressible and can be checked in polynomial time. The corresponding defining FO sentence and algorithm need the knowledge of one graph from each isomorphism class of MinEx(P ) to be effectively constructible. Knowing that M inEx(P ) is finite u.t.i, for example by means of a well-quasi-ordering argument, does not imply that one can compute it, see [START_REF] Courcelle | On betweenness in order-theoretic trees[END_REF]. However, a SAT solver that can check Property P may help to determine some bounds of P , by the following algorithm : Algorithm 1.2 : Some bounds of Property P .

Choose a graph G, expected not to satisfy P .

Clique-width and related notions

We review the notion of clique-width [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] based on constructing labelled graphs by means of graph operations.

Definitions 2.1 : Clique-width (a) A vertex-labelled (directed or undirected) graph is a triple G = (V, E, π)
where π is a mapping from V to a set of labels. Then π(G) := π(V ) is the set of labels of the vertices of G. An a-labelled vertex x has label a = π(x).

(b) Labelled graphs are defined from the following symbols and operations.

The nullary symbol a(x) denotes a vertex x labelled by a.

The union of disjoint graphs G and H is denoted by G ⊕ H. As this binary operation is associative, we use it as an operation of variable arity. As it is also commutative, the set of arguments is not ordered. The corresponding notation is ⊕(t 1 , t 2 , ..., t p ) where the order of the subterms t 1 , t 2 , ..., t p is irrelevant. For uniformity in formal constructions, we will also use terms where ⊕ has a single argument, and thus is identity. In small terms where each occurrence of ⊕ has two arguments, and also in inductive constructions, we will use the infix notation t 1 ⊕ t 2 , for the purpose of readability.

We denote by --→ add a,b the unary arc-addition operation that adds to a directed graph the missing arcs from a-labelled vertices to b-labelled ones. We denote by add a,b the similar edge-addition operation that adds to an undirected graph the missing edges between a-labelled vertices and b-labelled ones. Hence, add a,b is equivalent to --→ add a,b • --→ add b,a for undirected graphs handled as symmetric graphs.

Clearly --→ add a,b ( --→ add a,b (G)) = --→ add a,b (
G). This redundancy and less obvious ones (see Example 2.6) can be eliminated [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

We will use parallel relabellings relab h where h is a mapping, for example:

a -→ b, b -→ c, c -→ a, d -→ e, e -→ d.
Replacing parallel relabellings by compositions of elementary relabellings relab a→b (such that label a is replaced by b and the other labels are not changed) can be done without introducing new labels, by a top-down algorithm that reorganizes labellings, so as to eliminate permutations of labels. See [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], Proposition 2.118.

The labelled graph denoted by a term t is val(t) = (V, E, π). Its vertices are defined in the nullary symbols. We also say that t defines the unlabelled graph (V, E). Two terms t and t ′ are equivalent, denoted by t ≡ t ′ , if they define identical graphs, with the same vertices (not just isomorphic graphs).

(c) The width of a term built with the operations of (b) is the number of labels occurring there. The clique-width of a graph G, denoted by cwd(G), is the smallest width of a term defining G u.t.i. If G is undirected, its clique-width is the same if it is defined with the operations add a,b or, for the associated symmetric directed graph, with the operations --→ add a,b .

The graph property cwd(G) ≤ k is hereditary for each k (Proposition 2.105 of [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]).

Examples 2.2 : (1) Some bounds for the property "cwd(G) ≤ 3". It is known from [START_REF] Golumbic | On the clique-width of some perfect graph classes[END_REF] that the square grid G 3×3 has clique-width 4. By removing vertices, we get, u.t.i., three graphs4 of clique-width 4. Their proper induced subgraphs have all clique-width 3, hence these three graphs are bounds for the property "cwd(G) ≤ 3". They are G 3×3 minus the central vertex that is isomorphic to C 8 , G 3×3 minus a corner, and G 3×3 minus the middle vertex of a side.

(2) A bound for the property "cwd(G) ≤ 4".

The rectangular grid G 3×4 has clique-width 5. By removing any vertex (there are, u.t.i., four possibilities), we get graphs of clique-width 4. Hence, this grid is thus a bound for the property "cwd(G) ≤ 4". It is not known whether the sets of bounds for these two properties are finite. Definition 2.3 : Cographs and probe cographs (a) Cographs are the undirected graphs generated from isolated vertices, the operation ⊕ and the following operation ⊗ that is also associative and commutative:

G ⊗ H is G ⊕ H augmented with edges between each vertex of G and each vertex of H.

They are the undirected graphs of clique-width at most 2, see [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]. In particular, if G and H are a-labelled undirected graphs, then

G ⊗ H = relab b→a (add a,b [G ⊕ relab a→b (H)]).
Its vertices are all labelled by a. Cographs are also the undirected graphs without any induced path P 4 (a path with 4 vertices), that is their unique bound u.t.i.. (b) A probe cograph G is obtained from a cograph H by choosing a set of vertices L of H and deleting the edges between any two vertices of L. Probe cographs have clique-width at most 4 and this upper-bound can be reached. They form an hereditary classes. This class has finitely many bounds, but the complete list is not yet known [START_REF] Courcelle | On betweenness in order-theoretic trees[END_REF]. (a) A skeleton over a set V is a term s built with the operation ⊕ and the elements of V used as nullary symbols, in such a way that each u ∈ V has a unique occurrence in s. It is convenient to describe it as a rooted tree in the usual way. In particular, it is uniform of height λ if all paths from the root of this tree to its leaves have length λ. A skeleton is binary if each occurrence of ⊕ has arity 1 or 2.

(b) The skeleton of a term is the term (equivalently the tree) obtained by deleting the unary operations add a,b , --→ add a,b , relab a→b and relab h , and by replacing each a(x) by x. Two skeletons are equal if they only differ by a permutation of the arguments of some operations ⊕, as this operation is commutative.

(c) Let G = (V, E) be a graph and s be a skeleton over V . The clique-width of G relative to s, denoted by cwd(G, s), is the minimal clique-width of a term t that defines G and has skeleton s. Clearly, cwd(G, s) is always defined and is at most n = |V | because one can use one label for each vertex and define the edges at the top level. We have cwd(G) ≤ cwd(G, s).

If we simplify a skeleton s by eliminating the occurrences of ⊕ of arity 1, we obtain a skeleton s ′ such that cwd(G, s ′ ) = cwd(G, s). Relative clique-width is defined in [START_REF] Lozin | Rautenbach The relative clique-width of a graph[END_REF] for undirected graphs and binary skeletons. We extend this definition to directed graphs and arbitrary skeletons.

Its skeleton is

Sk(t) = ⊕[1, 2, ⊕{3, ⊕[4, 5]}]
. Its root has degree 3. The graph it defines is the union of the two paths 1 -2 -4 -5 and 3 -2 -5. This term is redundant in the following sense: the edge between 2 and 5 is defined by the operation add b,c and also by the operation add a,b . As we construct graphs without parallel edges, the operation add b,c can be removed. The equivalent term

t ′ = add a,b (relab c→a (add b,c (⊕[a(1), ⊕{b(2), ⊕[a(3), add a,c (⊕(a(4), c(5)))]}])))
has the different skeleton Sk(t ′ ) = ⊕[1, ⊕{2, ⊕ [3, ⊕(4, 5)]}] that is a binary tree, whereas Sk(t) has a root of degree 3. The skeleton of the equivalent term:

t ′′ = add a,b (relab c→a (add b,c (⊕[a(1), add a,c {⊕(a(4), c(5))}, a(3)}, b(2)])))
is the same as that of t, by a permutation of arguments of ⊕.

(b) Consider the clique K 4 with vertices 1, 2, 3, 4. Consider the skeleton s = ⊕(1, 2, 3, 4). The relative clique-width cwd(K 4 , s) is 4, whereas cwd(

K 4 ) = 2. If s ′ is the binary skeleton ⊕[⊕(1, 2), ⊕(3, 4)] of height 1, then cwd(K 4 , s ′ ) = 2. A corresponding term is: add a,b (⊕[relab b→a (add a,b (⊕(a(1), b(2)))), relab a→b (add a,b (⊕(a(3), b(4))))]).
We have Sk(s ′ ) = Sk(s). For every binary skeleton s ′′ over 1, 2, 3, 4, we have cwd(K 4 , s ′′ ) = 2.

Boolean satisfiability problems

By a SAT problem we mean the satisfiability of a Boolean formula in conjunctive form.

Definitions 3.1 : SAT problems (1) A Boolean satisfiability problem, a SAT problem in short, is a tuple Φ = (B, C, F, σ F ) such that : B is a finite set of Boolean variables; a variable x in B or its negation x is called a litteral, C is a finite set of clauses, that are disjunctions of litterals, F is a subset of B defining the set of fixed litterals, σ F : F → {true, false} associates a fixed truth value to each x in F , hence to each fixed litteral, either x or x.

(2) A mapping σ : B → {true, false} that coincides with σ F on F is called a truth value assignment (an assignment in short) for Φ. It satisfies Φ, which we denote by σ |= Φ, if it makes true each clause. We let Sat(Φ) be the set of solutions of Φ, defined as the assignments that satisfy it.

The task of a SAT solver is to decide whether a SAT problem Φ is satisfiable, i.e. whether Sat(Φ) is not empty. A related problem consists in computing Sat(Φ).

(3) A unit clause c consists of a single litteral, x or x. We write c = x or c = x in this case.

(4) The size of a SAT problem is the sum of the lengths of its clauses, where the length of a clause is the number of its litterals.

An empty clause is not satisfiable, and so is any SAT problem containing an empty clause. A SAT problem with an empty set of clauses is considered as (trivially) satisfiable. These cases may occur after transformations of SAT problems by resolution which replaces two clauses x ∨C and x∨ C ′ by the single one C ∨C ′ . However, the set of solutions is not preserved by this transformation, as the new clause does not tell whether x or x can be true.

Some graph properties reducing to Boolean satisfiability

We give four examples of encodings of graph properties into SAT problems. In Section 4, we will study the problem of checking whether cwd(G) ≤ k.

Example 3.2 : p-coloring.

A p-coloring of a (loop-free, cf. Section 1.1) graph G associates a color in [p] := {1, ..., p} with each vertex u in such a way that adjacent vertices have different colors. To define the p-colorings of G, we use the Boolean variables c u,i intended to express that the vertex u has color i. The negation of c u,i is denoted by c u,i .The clauses are, for all u ∈ V and i, j in [p] such that i < j :

(i) c u,1 ∨ c u,2 ... ∨ c u,p and c u,i ∨ c u,j
expressing that every vertex u has a unique color in [p]. That no two adjacent vertices have the same color is expressed by

(ii) c u,i ∨ c v,i
for every two adjacent vertices u, v such that u < v and i ∈ [p]. (Vertices are integers, hence are ordered).

This SAT problem involves pn variables and at most n+p(p-1)n/2+p |E| = O(pn 2 ) clauses 5 (n = |V | and we can assume that p < n). It has a solution if and only if G is p-colorable. The valid assignments are in bijection with the p-colorings.

As a second example, we present a new SAT encoding of the property that a graph G has tree-width at most k, denoted by twd(G) ≤ k. Samer and Veith have defined in [START_REF] Samer | Encoding treewidth into SAT. Theory and Applications of Satisfiability Testing[END_REF] a reduction of this verification to a SAT problem. We give an easier construction based on results from [START_REF] Courcelle | From tree-decompositions to clique-width terms[END_REF]. Definitions 3.3 : Normal forests and tree-width.

(1) Trees are rooted and defined as pairs (N, ≤) where N is the set of nodes and ≤ is the ancestor relation, hence is a partial order. The root is the maximal element. If v and w are two ancestors of a node, they are comparable, i.e., v ≤ w or w ≤ v.

(2) A forest is a union of disjoint (rooted) trees. It can be defined as a pair (N, ≤) such that ≤ is a partial order, and, as for trees, two ancestors of any node are comparable. However, two nodes have no common ancestor if they belong to distinct trees.

(3) A forest T = (N, ≤) is normal for a graph G = (V, E) if N = V and every two adjacent vertices are comparable. A depth-first spanning tree of a connected graph is normal for it.

(4) Let T be normal for G. For each u ∈ V , we define f * T (u) as the set of vertices v > u such that v is adjacent to some w ≤ u. The width of T is the maximal cardinality k of a set f * T (u). (5) Assume T as above is a rooted tree. Then (T, g) is a tree decomposition of G of width k where the box g(u) associated with a node u of T is the set of vertices f * T (u) ∪ {u}. A normal forest can be made into a tree by adding a common root to all composing trees, that yields a tree-decomposition of same width.

Proposition 3.4 : A graph G has tree-width at most k if and only if it has a normal forest of width at most k.

Proof : By Lemma 3 of [START_REF] Courcelle | From tree-decompositions to clique-width terms[END_REF].

Construction 3.5 : A SAT problem for tree-width.

Let a graph G be defined as (V, E). Its vertices are denoted by u, v, w. In order to check that twd(G) ≤ k, we define a SAT problem TWD k (G) as follows.

The Boolean variables are : a u,v for u = v, to express that u < v in the order ≤ of the normal forest T to be defined, and s u,v,i for u = v and i = 1, ..., k. They will help to express that the set f * T (u) has at most k elements.

The clauses are, for all pairwise distinct vertices u, v, w :

a u,v ∨ a v,u
to express the antisymmetry of the intended strict order < on V ,

a u,v ∨ a v,w ∨ a v,w to express its transitivity, a u,v ∨ a u,w ∨ a v,w ∨ a w,v to express that < defines a forest T with set of nodes V , a u,v ∨ a v,u
for any two adjacent vertices u, v, in order to express the normality of T .

The variables s u,v,i are intended to assign, for each u, a unique number

i ∈ [k] := {1, ..., k} to each v ∈ f * T (u).
The corresponding clauses are as follows, for all pairwise distinct vertices u, v, w and i ∈ [k] : s u,v,i ∨ a u,v to express that numbers are only assigned to ancestors of u, a u,v ∨ s u,v,1 ∨ ... ∨ s u,v,k if u and v are adjacent, and

a w,u ∨ a u,v ∨ s u,v,1 ∨ ... ∨ s u,v,k if v and w are adjacent.
These clauses express that each vertex v ∈ f * T (u) is assigned some number. The clauses

s u,v,i ∨ s u,w,i express that i is assigned to at most one vertex in f * T (u).
A variable s u,v,i may be true for vertices v > u not in f * T (u). This SAT problem involves (k + 2)n(n -1) variables and O(kn 3 ) clauses, which is less than for clique-width: the reduction to a SAT problem presented in Section 4 uses O((nk)n 4 ) clauses for checking cwd(G) ≤ k.

From a solution to TWD k (G), we obtain a tree decomposition (T, g) of G of width at most k cf. Definition 3.6 [START_REF] Courcelle | The monadic second-order logic of graphs VIII: Orientations[END_REF]. The normal tree6 is T = (V, ≤) where ≤ is described by the truth values of the variables a u,v and the box g(u) := f * T (u) ∪ {u} associated with a node u of T is contained7 in the set of vertices v such that s u,v,i is true.

Proposition 3.6 : A graph G has tree-width at most k if and only if the SAT problem TWD k (G) is satisfiable.
Proof : Immediate consequence of Proposition 3.4 and Construction 3.5.

Example 3.7 : Automorphisms

An automorphism h : G → G can be described by variables h u,v , for any two vertices u, v, whose truth expresses that v = h(u). That h is bijective is expressed by the following clauses, for all u, v, w such that v = w :

h u,v ∨ h u,w and h v,u ∨ h w,u ,
and, for totality :

h u,1 ∨ h u,2 ∨... ∨ h u,n .
That h preserves arcs is expressed by the generic clauses:

e u,v ∨ h u,w ∨ h v,x ∨ e w,x and e u,v ∨ h w,u ∨ h x,v ∨ e w,x for all u, v, w, x.
We get O(n 4 ) generic clauses forming the set AUTO(n) involving n 2 variables in addition to those that specify arcs. We can use these clauses as follows.

Case 1 : To check whether there exists an automorphism of G that maps a to b, we add to

E(G) ∪ AU T O(n), the unit clause h a,b .
Case 2 : To check whether Ga and Gb are isomorphic, we do as in Case 1 and we remove the clauses concerning arcs with at least one end in {a, b}. Equivalently, it suffices to replace in the description of G by E(G) each unit clause e u,v by e u,v if any of u or v is {a, b}.

Example 3.8 : Probe cographs According to Definition 2.3, we consider undirected graphs. To express by a SAT problem that G = (V, E) is a probe cograph, we use variables ℓ u and f u,v for u < v, such that ℓ u is true if and only if u ∈ L (the set of vertices of H such that we delete the edges whose both ends are in L to obtain G) and f u,v is true if and only if uv is an edge of the intended cograph H. The clauses are as follows,

(i) f u,v and ℓ u ∨ ℓ v for all u < v such that uv ∈ E, (ii) f u,v ∨ ℓ u and f u,v ∨ ℓ v for all u < v such that uv / ∈ E, because edges are deleted from H on the basis of L, (iii) f {u,v} ∨ f {v,w} ∨ f {w,x} ∨ f {u,w} ∨ f {u,x} ∨ f {v,x}
for all pairwise distinct vertices u, v, w, x, to expressed that the graph with edges defined by the variables f u,v is a cograph. Here, f {u,v} is a short notation for f min(u,v),max(u,v) and similarly for f {u,w} , f {u,x} etc.

This SAT problem involves n(n + 1)/2 variables and O(n 4 ) clauses. The variables f u,v are used to guess a cograph H including the given graph G.

The class of probe cographs has finitely many bounds u.t.i. [START_REF] Courcelle | On betweenness in order-theoretic trees[END_REF]. They have diameter at most 4 (except P 6 of diameter 5) and clique-width at most 8. An intractable algorithm can list them. Presently, we only know bounds having clique-with 3. Some others might be found by using these characterizations and Algorithm 1.2 .

4 Clique-width checking as a Boolean satisfiability problem.

We extend to directed graphs the construction for undirected graphs of [START_REF] Heule | A SAT approach to clique-width[END_REF]. We use the same terminology and notation. We will omit the correctness proofs for the case of directed graphs because they extend in a straightforward manner those of [START_REF] Heule | A SAT approach to clique-width[END_REF]. However, we will give complete definitions and constructions that can be used for implementation. They have been tested and implemented in TRAG. (a) A template T on a set V consists of a partition of V into components and a partition into groups which refines the previous one, that is, each component is a union of groups. The set V will be a set of vertices.

Clique-width checking

(b) A derivation relative to a set V is a sequence D = (T 0 , ..., T λ ) of templates T i on V where each i is called a level, the partition in components of T i-1 refines that of T i and the partition in groups of T i-1 refines that of T i . Hence, a component (resp. a group) at level i is a union of components (resp. of groups) at level i -1. We say that D has height λ and thus, λ + 1 levels8 .

(c) The template T λ at the top level has a unique component, and the components and groups at level 0 are singletons.

(d) We say that D is a k-derivation if each component contains at most k groups.

(e) Let G = (V, E) be an undirected graph. A derivation D = (T 0 , ..., T λ ) on V is a derivation for G or, simply, is correct for G if the following conditions (written as in [START_REF] Heule | A SAT approach to clique-width[END_REF]) hold for all relevant integers i.

Edge Property : For u, v ∈ V such that uv ∈ E, if u, v are in a same group in T i , they are in a same component of T i-1 . Neighborhood Property : For distinct u, v, w ∈ V such that uv ∈ E and uw / ∈ E, if v, w are in a same group in T i , then u, v are in a same component of T i-1 .
Path Property : For distinct u, v, w, x ∈ V such that uv, uw, xv ∈ E and xw / ∈ E, if u, x are in a same group of T i , and v, w are in a same group of T i , then u, v are in a same component of T i-1 .

(f) Let G be directed with arc set E, the corresponding conditions are : (f.1) the arc property and the path property that read exactly as the edge and path property in (e) (although E need not be symmetric);

(f.2) the neighborhood property that is now:

Neighborhood Property : For distinct u, v, w ∈ V such
= n -k + 1.
Proof : If G is undirected, the result is Proposition 3.9 of [START_REF] Heule | A SAT approach to clique-width[END_REF]. If G is directed, a straightforward inspection of the proofs of [START_REF] Heule | A SAT approach to clique-width[END_REF] shows that they adapt immediately to the directed case.

In Section 8, we will give an algorithm extending that of [START_REF] Heule | A SAT approach to clique-width[END_REF] to construct a term of width at most k that defines G from a k-derivation of it.

Remarks 4.3 : 1) A derivation D = (T 0 , ..., T λ ) for a graph G corresponds to a term t that defines this graph, such that all vertices are at distance λ of the root in the skeleton Sk(t) (considered as a rooted tree). We will say that t and its skeleton are uniform of height λ.

2) The components of D specify a skeleton that may have occurrences of ⊕ of arity 1 in order to achieve uniformity. The skeleton of the term t of Example 2.6 is ⊕(1, 2, ⊕[3, ⊕(4, 5)]). The corresponding derivation with λ = 3 is (T 0 , ..., T 3 ) (we only show the components) :

T 3 : {1, 2, 3, 4, 5} T 2 : {1}, {2}, {3, 4, 5} T 1 : {1}, {2}, {3}, {4, 5} T 0 : {1}, {2}, {3}, {4}, {5}.
We now consider the description of derivations by clauses that translate Definition 4.1. We first consider the description of k-derivations of height λ for an edge-less graph with n vertices, that is, they do not depend on edges. Definitions 4.4 : Clauses for derivations. The set V of n > 2 vertices is linearly ordered by ≤ . Any other linear order gives the same final result, although some clauses are not the same. The variables u, u ′ , u ′′ , v, w, x will always denote vertices in V . We will use Boolean variables c u,v,0 , c u,v,i and g u,v,i , for u < v,

1 ≤ i ≤ λ.
The validity of c u,v,i (resp. g u,v,i ) means that u and v are in a same component (resp. a same group) in T i . We need no variable g u,v,0 . Level 0 will be treated directly, by means of the variables c u,v,0 defined as false. Every vertex is a component and a group at level 0.

The conditions of Definition 4.1(c) are expressed by the unit clauses:

c u,v,0 and c u,v,λ
for all u < v. In order that the variables c u,v,i and g u,v,i express membership in sets forming partitions (Definition 4.1(a)) we define the following clauses.

Component transitivity clauses:

For all u, v, w such that u < v < w and 1 ≤ i ≤ λ -1:

c u,v,i ∨ c v,w,i ∨ c u,w,i , c u,v,i ∨ c u,w,i ∨ c v,w,i and c u,w,i ∨ c v,w,i ∨ c u,v,i .

Group transitivity clauses

For all u, v, w such that u < v < w, and

1 ≤ i ≤ λ: g u,v,i ∨ g v,w,i ∨ g u,w,i , g u,v,i ∨ g u,w,i ∨ g v,w,i and g u,w,i ∨ g v,w,i ∨ g u,v,i .
That the partitions in groups refine the partitions in components (Definition 4.1(b)) is expressed by :

g u,v,i ∨ c u,v,i for all u, v such that u < v and 1 ≤ i ≤ λ.
The refinements of partitions between consecutive levels (Definition 2.1(b)) is expressed as follows.

Component and group refinement clauses :

c u,v,i-1 ∨ c u,v,i , g u,v,i-1 ∨ g u,v,i for all u, v such that u < v and 2 ≤ i ≤ λ.
In this way, we have defined the set D(n, λ) of Derivation clauses using approximately λn 2 variables. We have λ(n -2)

3 /3 < |D(n, λ)| < λn 3 /2.
We now express that the width of a derivation represented by the positively assigned variables c u,v,i , g u,v,i is at most k. (a) Let D = (T 0 , ..., T λ ) be a derivation on a set V . As in [START_REF] Heule | A SAT approach to clique-width[END_REF], we say that v ∈ V is representative (of its group) of level i if it is the smallest one in its group. Variables r v,i are used to mean that v is representative at level i > 0. Every vertex is representative at level 0.

The corresponding clauses form the following set R(n, λ). As V = [n], ordered in the standard way, the vertices u before v are 1, 2, ..., (v -1). Hence, we set the following clauses, for all 1 ≤ i ≤ λ and all vertices u, v such that u < v :

r v,i ∨ g u,v,i , r v,i ∨ g 1,v,i ∨ g 2,v,i ∨ ... ∨ g (v-1),v,i . The clauses r v,i ∨ g u,v,i express that if v is representative, it is minimal in its group. The clauses r v,i ∨ g 1,v,i ∨ g 2,v,i ∨ ... ∨ g (v-1),v,i express that if v is not representative at level i, it is not minimal in its group. If v = 1, they reduce to r 1,i for 1 ≤ i ≤ λ.
(b) Let k be an intended bound on clique-width so that [k] can be used as the set of labels for the construction of a term (cf. Definition 2.). We introduce variables s v,a,i to express that every representative vertex v at level i > 0 has a group number a ∈ [k], attached in a unique way to its group at level i (intended to become a label in the term to be constructed 9 ). Different groups at level i in a same component at that level must have different group numbers. We do not require that the group numbers for the groups in a same component form an interval of integers. At level 0, every vertex is representative with group number 1. The corresponding conditions are expressed by the following clauses. C1 : For each vertex v and each 1 ≤ i ≤ λ the clause :

r v,i ∨ s v,1,i ∨ ... ∨ s v,k,i expresses that a representative vertex v has a group number in [k]. C2 : For each vertex v, 1 ≤ i ≤ λ and each pair a, b such that 1 ≤ a < b ≤ k, we define the clause r v,i ∨ s v,a,i ∨ s v,b,i
They express, assuming C1, that each representative vertex has a unique group number.

C3 : For all vertices u, v such that u < v, 1 ≤ i ≤ λ and 1 ≤ a ≤ k : we define the clauses r u,i ∨ r v,i ∨ c u,v,i ∨ s u,a,i ∨ s v,a,i to express that no two groups in a same component have the same group number.

C4 : For each vertex v, 1 ≤ i ≤ λ and each 1 ≤ a ≤ k, we define the clause s v,a,i ∨ r v,i to express that s v,a,i holds only if v is representative at level i.

We obtain a set W (n, λ, k) of width clauses involving λn(k + 1) additional variables. We have

|W (n, λ, k)| = λn[(n +1)/2+1 +k(k -1)/2+ (n -1)k/2 +k],
hence this number is between λnk(n+k)/2 and λn(k+1)(n+k)/2. These clauses express that the considered derivation has width at most k.

Remark 4.6 : In [START_REF] Heule | A SAT approach to clique-width[END_REF], variables o > v,a,i are used instead of s v,a,i . If o > v,a,i is true, a representative vertex v has a group number strictly larger than a, and the group numbers associated with the representative vertices are increasing with respect to the order on vertices. This method uses only λkn(n -1)/2 clauses. However, the validity of o > v,a,i when v is representative does not specify a particular group number. Such information is useful for building a term from a valid assignment as we will see (in Section 8). Lemma 4.7 : Let D be a derivation of height λ for n vertices, described by the truth values of the variables c u,v,i and g u,v,i for an assignment σ satisfying D(n, λ). Then D has width at most k if and only if σ satisfies the clauses of the set W (n, λ, k) for appropriate Boolean values assigned to the variables r v,i and s v,a,i .

Proof : Clear from the definitions.

Next we define clauses depending on the arcs of the considered graph G, in order to express the arc, neighborhood and path properties of Definition 4.1(e,f). Conditions are formulated for directed graphs, hence also for undirected graphs handled as symmetric graphs; we obtain correct clique-width computations as recalled in Definition 4.1(c). Definition 4.8 : Clauses expressing the correctness of a derivation for a graph G.

To implement the conditions of Definition 4.1(e,f), we define as follows the set of clauses Dir(n, λ, G). The notation recalls that the graph G is directed. The translation is immediate from the given definitions.

Arc property clauses 10 . For all 1 ≤ i ≤ λ and adjacent vertices u, v ∈ V such that u < v, we set in Dir(n, λ, G) the clauses :

g u,v,i ∨ c u,v,i-1 .
Neighborhood property clauses. For all 1 ≤ i ≤ λ, all uv ∈ E and w / ∈ {u, v},

if uw / ∈ E, we set g {v,w},i ∨ c {u,v},i-1 , if wv / ∈ E, we set g {u,w},i ∨ c {u,v},i-1 .
The variables c u,v,i and g u,v,i are defined only if u < v; we write c {u,v},i-1 instead of c min(u,v),max(u,v),i-1 and similarly for g {v,w},i . Let P be the directed path

Path property clauses.

1 -→ 2 -→ 3 -→ 4.
There is no clause for the path property because no vertex has outdegree more than 1. For the undirected path P 4 = 1 -2 -3 -4, we have the clauses g 2,4,i ∨ g 1,3,i ∨ c 2,3,i-1 for the path property.

Consider now

C := 1 ←-2 -→ 3 ←-4 ←-1.
For the path property, we have the clauses : g 2,4,i ∨ g 1,3,i ∨ c 2,3,i-1 (because there is no arc 4 -→ 1). For the cycle C 4 := 1 -2 -3 -4 -1, we have no clause for the path property.

Relative clique-width.

We refer to Definition 2.5. A uniform skeleton s of height λ is equivalent to a sequence (P 0 , ..., P λ ) of partitions of V (in components) such that P i-1 refines P i , P λ has a unique class and P 0 consists of singletons.

We will specify a skeleton by unit clauses. They will have to be added to the others, so that any satisfying assignment defines groups relative to the fixed skeleton.

The unit clauses c u,v,0 and c u,v,λ define the partitions P 0 and P λ (cf. Definition 4.4). We specify the other partitions P i by the following unit clauses for 1 ≤ i ≤ λ and u < v : c u,v,i if u is minimal in its component at level i and v belongs to this component, c u,v,i if u and v are in different components at level i and are minimal in each of them.

We let SK(s) be the set of these clauses. Their number is bounded by c(n + c) where c is the total number of components at levels i := 1, ..., λ.

The component transitivity clauses (Definition 4.4) define the truth values of all other variables c u,v,i in such a way they define the partition P i . The following is clear from definitions and Theorem 4.9.

Proposition 4.11 : Let s be a uniform skeleton of height λ over

V = [n]. A graph G = (V, E) has relative clique-width cwd(G, s) = k if and only if the SAT problem CWD k,λ (G) ∪ SK(s) is satisfiable.
Here, we do not impose λ = nk + 1. The parameter λ is defined from s.

Example 4.12 : We take the skeleton s = ⊕[⊕(1, 2), 3, ⊕(4, ⊕ [START_REF] Courcelle | The monadic second-order logic of graphs VIII: Orientations[END_REF]6])]. Padded with operations ⊕ of arity 1 to obtain uniformity (cf Definition 2.5), which gives the skeleton:

⊕[⊕(⊕(1), ⊕(2)), ⊕(⊕(3)), ⊕(⊕(4), ⊕[5, 6])],
the corresponding sequence (P 0 , P 1 , P 2 , P 3 ) is P 3 : {1, 2, 3, 4, 5, 6} P 2 : {1, 2}, {3}, {4, 5, 6} P 1 : {1}, {2}, {3}, {4}, {5, 6} P 0 : {1}, {2}, {3}, {4}, {5}, {6}.

Then P 1 and P 2 are described by the following unit clauses :

c 5,6,1 , c u,v,1 for 1 ≤ u < v ≤

Linear clique-width Definition 4.13 : Linear clique-width

The linear clique-width of a graph G, denoted by lcwd(G), is relative to linear terms, i.e., those such that at most one argument of an operation ⊕ (of any arity) defines a graph with more than one vertex. It can be equivalently defined with respect to linear binary terms, that is, those that have a binary skeleton, because a subterm ⊕(t 1 , t 2 , ..., t n ) can be replaced by ⊕(t 1 , ⊕(t 2 , ...⊕(t n-1 , t n )..)) without changing the unary operations --→ add a,b and relab h , where, without loss of generality (because ⊕ is commutative and associative) the terms t 1 , t 2 , ..., t n-1 denote graphs with a single vertex.

For examples, trees have clique-width at most 3 and unbounded linear cliquewidth [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]. If m ≥ n ≥ 3, the rectangular grid G n,m has linear clique-width at most n + 2. Furthermore, cwd(G n,n ) = n + 1 by [START_REF] Golumbic | On the clique-width of some perfect graph classes[END_REF]. From tests 11 made with TRAG, we conjecture that lcwd

(G n,n ) = lcwd(G n,m ) = cwd(G n,m ) = n + 2.
The article [START_REF] Heule | A SAT approach to clique-width[END_REF] defines a set of clauses intended to constraint derivations so that they define linear terms. This method can be combined with the extension to directed graphs of Section 3. We detail it for completeness sake. (b) We introduce variables sc u,i for u ∈ V and 1 ≤ i ≤ λ -1 whose truth implies that {u} is a component at level i. The corresponding clauses are as follows :

L1 : For all u, v such that u < v and 1 ≤ i ≤ λ -1 :

c u,v,i ∨ sc u,i and c u,v,i ∨ sc v,i
to express that if u and v are distinct vertices in a component, then none of them is a singleton component.

L2 : For all u, v such that u < v and

1 ≤ i ≤ λ -1 sc u,i ∨ sc v,i ∨ c u,v,i ,
to express that if {u} and {v} are not components at level i, then u and v are in a same component, hence that there are no two components with at least two vertices at that level.

Here, we get a set L(n, λ) of 3(λ -1)n(n -1)/2 clauses. In a k-derivation satisfying L(n, λ) in addition to D(n, λ) ∪ W (n, λ, k), a variable sc u,i is false if the component of u at level i is not singleton (by L1). However, sc u,i may be false if all components at level i are singleton (see the next example). This cannot occur if the derivation is strict in the sense of [START_REF] Heule | A SAT approach to clique-width[END_REF] which means that, at any level i, at least two components get merged into one at level i + 1.

Example 4.15 : Consider the following derivation of height 3, so that the variables sc u,i are defined only for i = 1 and 2.

T 3 : {1, 2, 3, 4} T 2 : {1, 2}, {3}, {4} T 1 : {1}, {2}, {3}, {4} T 0 : {1}, {2}, {3}, {4}.
Then sc 1,2 and sc 2,2 must be false (because T 2 has a component {1, 2}) and sc 3,2 and sc 4,2 must be true. The four variables sc 1,1 , sc 2,1 , sc 3,1 , sc 4,1 can all be true. Alternatively, any of them can be false, and then, the other three variables must be true. No two of these variables can be false by L2. Proof : Clear from definitions and Proposition 6.3 of [START_REF] Heule | A SAT approach to clique-width[END_REF].

The choice of λ = nk + 1 yields terms that are not binary (the height of a derivation corresponding to binary linear term that defines a graph with n vertices is at least n -1). They can be transformed into binary ones.

Partial labellings

Definitions 4.17 : Labelled vertices.

(a) We recall that a term written with labels in [k] defines a labelled graph G = (V, E, π) so that π(V ) ⊆ [k] is the set of labels of the vertices of G. When defining clique-width, we omit this "final" labelling.

(b) A partial labelling of G = (V, E) is a partial mapping Lab : V → L where L is a set of labels. We define the clique-width of the partially labelled graph (V, E, Lab) as the least width of a term with labels in [k] that defines a labelled graph G = (V, E, π) such that, for some mapping α : π(V ) → L, we have Lab(v) = α(π(v)) if Lab(v) is defined. In other words, if Lab(v) is defined, this label depends only on π(v).

Knowing the clique-width of a partially labelled graph is useful in (usually difficult) proofs that a graph has clique-width at least some value. We define a set P (n, λ, Lab) of unit clauses to be added to all those considered before for expressing the existence of a k-derivation of height λ, possibly a linear one. It consists of the clauses g u,v,λ for all vertices u, v such that u < v and, Lab(u) and Lab(v) are defined and are different.

They imply that if u and v are in a same group at the top level T λ of a derivation, and Lab(u) and Lab(v) are defined, then these labels are equal, so that a mapping α as in Definition 4.17(b) can exist. The vertices u and v may not be in a same group at the top level whereas Lab(u) = Lab(v): then, an appropriate relabelling applied to the term t(V, λ) (cf. Section 8) yields a term as desired.

The number of clauses in P (n, λ, Lab) is at most n ′ (n ′ -1)/2 where n ′ is the number of vertices having a specified label.

A generalization of relative clique-width

Here is the idea. Given a graph G = (V, E), we split

V into three parts V 1 , V 2 , V 3 , and decide to decompose each of G[V 1 ], G[V 2 ] and G[V 3
] and then to combine the obtained terms t 1 , t 2 , t 3 by ⊕(t 1 , t 2 , t 3 ) together with arc addition operations. Each set V i can itself be partitioned. This amounts to choosing a tree of subsets of V that provides a hint and actually a constraint for finding a decomposition, that may not be optimal. This tree approximates the skeleton of the term to be defined. The hope is that the result will come quicker as the search space is, seemingly, smaller due to the proposed constraints that approximate an intended skeleton.

Definition 4.21 : Let G = (V, E) be a graph. (a) Let B be a family of subsets of V that are pairwise nonoverlapping, which means that two elements are either disjoint or one is included in the other. We call them blocks. Each vertex is a singleton block and V is also a block. Inclusion of blocks is the ancestor relation of s considered as a rooted tree T (B). The skeleton of a term without nodes of arity 1 is such a tree.

(b) A derivation D for G is compatible with B if no component overlaps a block. Let C be the set of components of D. Then B ∪ C is nonoverlapping. Hence the tree of components and the tree T (B) both embeds into a single tree. See Example 4.25.

(c) The clique-width of G relative to B, denoted by cwd(G, B), is the least width of a derivation for G compatible with B. Lemma 4.22 : If a derivation D for G is compatible with B, then every block is a union of pairwise disjoint components, and every component is a union of pairwise disjoint blocks. Some blocks may be components. The height of the tree T (B) may be larger than that of the derivation. For an example, if the components are {1,2,3,4} and the singletons, whereas the blocks are {1,2,3,4}, {1,2,3}, {1,2} and the singletons.

If B is defined from a binary skeleton s, then the derivations associated with B and s are the same. Construction 4.23. A SAT problem for cwd(G, B) ≤ k Encoding blocks. We let B 1 , ..., B q be the blocks that have at least 2 vertices and are not V . For each vertex u and integer j = 1, ..., q, we define a Boolean variable b u,j to mean that u ∈ B j . As we assume that B is nonoverlapping, we need not define clauses to check this condition.

We define the unit clause b u,j if u ∈ B j and b u,j otherwise. The clauses expressing that a derivation D of height λ is compatible with B are as follows (we use the notation of Section 4.1) :

For distinct vertices u, v, w and 1 ≤ i < λ, and

1 ≤ j < q, c u,v,i ∨ b v,j ∨ b w,j ∨ c u,w,i ∨ b u,j .
They forbid the overlap of a component C i containing u, v but not w with a block B j containing v, w but not u.

We let Blk(B, n, λ) be the set of these O(λqn 3 ) clauses and the qn unit clauses that describe B. They do not concern the edges of the considered graph. They are more numerous than those for relative clique-width (Section 4.2). Proof : Easy.

Example 4.25 : The Petersen graph

To define the Petersen graph shown in Figure 1, TRAG produces a term 12 t 0 witnessing that its clique-width is at most 5 that we rewrite as follows:

t 0 = add d,e (⊕(t 1 , e[4])).

Graph transformations, clique-width and open questions

We present open questions relative to the following general questions : how does the clique-width of a graph increase if we equip it with an orientation, if we add a vertex and incident edges or arcs, or if we contract an edge. Some clique-width computations by means of SAT problems may help to solve them.

Graph orientations

Proposition 5.1 : The linear clique-width of a directed graph

G is at most n -k where k is maximal such that 4 k < n -k. If G is oriented, its linear clique-width is at most n -k where k is maximal such that 3 k < n -k. If G is a tournament or is undirected, its linear clique-width is at most n -k where k is maximal such that 2 k < n -k.
Proof : The bound for undirected graphs is stated in [START_REF] Johansson | Logn-approximative NLC k -decomposition in O(n 2k+1 ) time[END_REF]. We give for all cases a proof based on derivations, whereas constructions using labels are cumbersome.

Let G be undirected and linearly ordered in an arbitrary way. We assume that V G = [n] and n ≥ 2. We define a derivation D = (T 0 , ..., T n-1 ) as follows.

The components of T i are {1, ..., i + 1}, {i + 2}, ..., {n}. In particular, those of T 0 are {1}, {2}, ..., {n} and the only one of T n-1 is {1, ..., n}.

For describing the groups of D, we define on {1, ..., i} the equivalence relation;

u ∼ i v :⇐⇒ for every w ∈ {i + 1, ..., n} we have uw ⇐⇒ vw, that has at most 2 i classes. The groups of T i are the equivalence classes of ∼ i and the singleton sets {i + 1}, ..., {n}.

We let

G i := G[{1, ..., i + 1}] hence, G n-1 = G.
By using the construction in Section 8 (that proves Theorem 4.2), we define G 1 , ..., G n-1 by linear terms.

We obtain G i from G i-1 by adding to it the vertex i + 1 and edges between it and its adjacent vertices that belong to {1, ..., i}. Any two such vertices in a same group, are equivalent with respect to ∼ i , hence linked to i + 1 in the same way. It follows that edges are added on the basis of groups.

Each edge of G between j and i + 1 > j is correctly added at the step constructing G i .

Each component of T i has at most 2 n-i + 1 groups, and also, trivially, at most i + 1 groups, as the largest component of T i has cardinality i+ 1. It follows that the linear clique-width of G is bounded by

c := max{min{i + 1, 2 n-i + 1} | i = 0, ..., n -1}. Let k > 0 be such that n > k and 2 k < n -k. If i < n -k, then i + 1 ≤ n -k. If i ≥ n -k, then 2 n-i + 1 ≤ 2 k + 1 ≤ n -k. Hence, c ≤ n -k.
For the three cases concerning directed graphs, the proof is the same with equivalence ∼ i defined by: u ∼ i v :⇐⇒ for every w ∈ {i + 1, ..., n} we have u → w ⇐⇒ v → w and w → u ⇐⇒ w → v.

It has at most, respectively, 4 i , 2 i and 3 i equivalence classes in the cases of directed graphs, tournaments and in that where no arc in G has an opposite arc.

Remarks 5.2 : (1) We obtain bounds for clique-width as it is no larger than linear clique-width.

(2) These upper bounds are obtained from arbitrary linear orderings of the vertices. Two different orderings may yield derivations of different widths. Consider for an example the path P 2n = 1 -2 -3 -... -2n. From the natural ordering 1 < 2 < ... < 2n, we get the exact clique-width 3. If we use the order 1, 3, 5, ..., (2n -1), 2, 4, 6, ..., 2n, we get a derivation of width n + 1.

Open question 5.3 : Can one improve the upper-bounds of Proposition 5.1 ?

Examples and questions 5.4 : (1) The maximum clique-width of a directed graph H such that U nd(H) is a forest is 3, as for an undirected forest.

(2) We know from [START_REF] Courcelle | The monadic second-order logic of graphs VIII: Orientations[END_REF] that tournaments have unbounded clique-width whereas cliques have clique-width 2. We might have an upper-bound to the clique-width of a tournament with n vertices of the form, say, 3n/4 for n larger than some value. It would be better than the one of Proposition 5.1 for n ≥ 33.

(3) The clique-width of the tournament 1 → 2 → 3 → 1 is 3. Tournaments having 4 vertices have clique-width 2 or 3. We checked that with TRAG, but a proof is not difficult to do. What about those with 5 vertices ? (4) The oriented Paley graph 13 with 7 vertices is a tournament of cliquewidth 5, where 5 is the upper-bound of Proposition 5.1 to its linear clique-width because 4 = 2 2 < 7 -2; see Figure 2.

The oriented Paley graph with 11 vertices is the union of the following directed cycles:

1 → 2 → 3 → 4 → 5 → 6 → 7 → 8 → 9 → 10 → 11 → 1 3 → 6 → 9 → 1 → 4 → 7 → 10 → 2 → 5 → 8 → 11 → 3 4 → 8 → 1 → 5 → 9 → 2 → 6 → 10 → 3 → 7 → 11 → 4
5 → 10 → 4 → 9 → 3 → 8 → 2 → 7 → 1 → 6 → 11 → 5 9 → 7 → 5 → 3 → 1 → 10 → 8 → 6 → 4 → 2 → 11 → 9.
It has clique-width 7 whereas the upper-bound of Proposition 5.1 to its linear clique-width is 9 as 4 = 2 2 < 11 -2 and 2 3 = 11 -3. These computations have been done with TRAG [START_REF] Courcelle | Online software TRAG[END_REF].

Vertex addition and deletion

Vertex addition means adding one vertex, and edges or arcs between it and the existing vertices. Vertex deletion means deleting one vertex and all incident edges or arcs. Proposition 5.5 : (1) Vertex addition applied to an undirected graph of clique-width k yields a graph of clique-width at most 2k.

(2) Vertex addition applied to a directed graph of clique-width k yields a graph of clique-width at most 4k.

(3) Vertex addition applied to a directed or undirected graph of linear cliquewidth k yield a graph of linear clique-width at most k + 2.

Proof : (1) is Theorem 8 of [START_REF] Gurski | The behavior of clique-width under graph operations and graph transformations[END_REF].

(2) follows from an easy adaptation of the proof of (1). In both cases, if x is the vertex added to G defined by a term t, the proof constructs a term that defines the new graph and has skeleton x ⊕ Sk(t).

(3) Let V := {y 1 , ..., y p } and G = (V, E) be defined by a linear term t with skeleton ⊕(y p , ⊕(y p-1 , ... ⊕ (y 2 , y 1 )...)). Then, it is easy to build a linear term t ′ with skeleton ⊕(y p , ⊕(y p-1 , ... ⊕ (y 2 , ⊕(y 1 , x))...)) that defines G ′ obtained from G by adding the vertex x and arcs or edges between it and the existing vertices. If t uses k labels, then t ′ uses k +2 labels. The term t read bottom-up sets the vertices in order y 1 , y 2 , ...y p by means of nullary symbols c 1 (y 1 ), c 2 (y 2 ), ..., c p (y p ) and, at each step i, it adds the edges between y i and previously defined vertices. The construction by t ′ starts with a(x). Each vertex y i is set by b(y i ), linked to x by add a,b if x is adjacent to y i in G ′ , and then relabelled by relab b→c i .

The above constructions for clique-width and linear clique-width are somehow opposite: the new vertex x is added at the top level of the existing term in case of clique-width (see Example 5.6( 1)) and at the bottom level in case of linear clique-width. where

ADD is add a,b • add a ′ ,b • add a,b ′ • add a ′ ,b ′ . However, cwd(G ′ ) = 3.
Hence, the construction of Proposition 5.5 [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF] is not optimal in this case.

(2) Let H be the cograph with vertex set [START_REF] Fellows | Clique-width is NP-Complete[END_REF] defined by ⊗(t 1 , t 2 , t 3 ) where: Deleting a vertex does not increase clique-width. In some cases, e.g., in Algorithm 1.2 (cf. Examples 2.2) we may need to know the exact clique-width of a graph G-a for which we know cwd(G). This observation motivates Proposition 6.10.

t 1 := ⊕(t 4 , t 5 ),

Edge contractions

In this section and the next one, we only consider undirected graphs. The graphs obtained by edge contractions from the graphs of clique-width 3 or linear cliquewidth 4 have unbounded clique-width [6]. It is easy to prove 14 that the class of cographs, equivalently, of undirected graphs of clique-width at most 2, is closed under edge contractions.

Open question 5.8 : Exhibit a graph of clique-width 3 whose clique-width increases by the contraction of a single edge.

It is possible to compute one by an intractable algorithm [6].

Erasing a vertex x of degree 2 consists in contracting on of the two edges incident to it. A path yxz is thus transformed into yz. (We consider graphs without parallel edges, hence y = z).

Erasing vertices in a graph of clique-width or linear clique-width k produces a graph of clique-width or linear clique-width at most 2 k+1 -1. The proof given in [6] for clique-width works for linear clique-width by using linear rank-width and vertex-minors.

Open question 5.9 : Can one find upper-bounds smaller than 2 k+1 -1?

Planar graphs

Planar graphs have unbounded clique-width since the clique-width of the square grid G n×n is n + 1 [START_REF] Golumbic | On the clique-width of some perfect graph classes[END_REF]. All graphs of tree-width at most 2 are planar. They have clique-width at most 6 (cf. [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]).

Open question 5.10 : Prove that graphs of tree-width 2 have clique-width at most 5 or construct one of clique-width 6.

Outerplanar graphs have planar embeddings where all edges are drawn inside the bounded region defined by a Hamiltonian cycle. They have tree-width 2 and clique-width at most 5 by [START_REF] Courcelle | On quasi-planar graphs: Clique-width and logical description[END_REF]. This upper-bound, verified by TRAG, is reached by the union of the three cycles C 12 = 1-2-...-12-1, 1-3-5-7-9-11-1 and 3 -7 -11 -3.

Outerplanar graphs have unbounded linear clique-width because there is a monadic second-order transduction mapping the set of outerplanar graphs to the set of rooted trees. Rooted trees have unbounded linear clique-width, hence, so must have outerplanar graphs by Theorem 7.41 of [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

The outer 1-planar graphs are similar to outerplanar graphs except that each edge that is not on the Hamiltonian cycle can be crossed by at most one edge. They are actually planar : some crossed edges can be drawn outside of the Hamiltonian cycle in order to avoid crossings. They have tree-width at most 3 [START_REF] Courcelle | On quasi-planar graphs: Clique-width and logical description[END_REF] and clique-width at most 6 by a technical proof.

Open question 5.11 : Prove that outer 1-planar graphs have clique-width at most 5 or construct one of clique-width 6.

A logical view of SAT checkable properties

A graph G = (V, E) is handled as a logical structure (V, edg) where edg is the binary adjacency relation on V . If the vertex set is ordered, the corresponding structure is (V, edg, ≤). This is the case in Example 3.5 and for clique-width in Section 4.

We will consider second-order formulas written with =, <, edg, constants a 1 , ..., a n denoting the vertices, first-order variables x 1 , ..., x m and second-order variables R 1 , ..., R p intended to denote relations on V of fixed arities respectively ρ(R 1 ), ..., ρ(R p ). We will write formulas with < denoting the strict order corresponding to ≤. The notation ϕ(x 1 , ..., x m ) indicates that the free first-order variables are among x 1 , ..., x m . A sentence is a formula without free variables. It expresses a graph property.

A quantifier-free (QF in short) formula is in conjunctive form (CQF in short) if it is a conjunction of disjunctions of atomic formulas and their negations. Every QF formula can be transformed into an equivalent formula in conjunctive form, by using the fact that, if b i,j , i ∈ [n], j ∈ [m] are atomic or negated atomic formulas, we have :

i∈[n] j∈[m] b i,j ≡ f ∈M i∈[n] b i,f (i)
where M is the set of functions f : [m] → [n], and similarly by exchanging ∨ and ∧. The size of the formula may increase exponentially. Definitions 6.1 : Existential second-order sentences. An existential second-order (∃SO in short) sentence is of the form ∃R 1 , ..., R p .ψ where ψ is a first-order (FO in short) formula whose free variables are R 1 , ..., R p . By Fagin's Theorem, ∃SO sentences define problems in the complexity class NP. We will review the construction of a SAT problem associated with an ∃SO sentence ψ and a (possibly ordered) graph G, that checks whether G |= ψ. Proposition 6.2 : From an ∃SO sentence ϕ of the form ∃R 1 , ..., R p .ψ and a (possibly ordered) graph G, one can build a SAT problem Σ ϕ (G) that is satisfiable if and only if G |= ϕ. Its number of variables is upper-bounded by p.n s where s is the maximal arity of some R i and n is the number of vertices.

Proof : The vertex set of G is V . For each i = 1, ..., p and each ρ(R i )-tuple (a 1 , ..., a ρ(Ri) ) of vertices, one defines a Boolean variable R i (a 1 , ..., a ρ(Ri) ).

A Boolean formula ψ G is obtained from ψ by the following transformations applied recursively: It is clear that G |= ∃R 1 , ..., R p .ψ if and only if ψ G is satisfiable. By converting ψ G in conjunctive form, we obtain a SAT problem as in Definition 3.1.

The number of clauses depends on the quantifier alternation in ψ.

The obtained SAT problems may be of exponential size in the size of the graph. For example, if ϕ is ∃R, x∀y.R(x, y), then the conversion of ∃x∀y.R(x, y) G in conjunctive form yields We consider restrictions on ∃SO sentences insuring that the associated SAT problems have of polynomial sizes (which by itself gives no guarantee of practical effectivity). Definitions 6.3 : Restricted existential second-order sentences.

(1) An ∃SO u sentence is an ∃SO sentence ϕ of the form ∃R 1 , ..., R p .ψ such that ψ is a universal FO formula, i.e., of the form ∀y 1 , ..., y q .θ(y 1 , ..., y q ) where θ is quantifier-free.

(2) It is an ∃SO u,c sentence if furthermore, θ(y 1 , ..., y q ) is in conjunctive form. Fact 6.4 : ∃SO u sentences define hereditary graph properties. Proof: This is clear because the validity of a universal FO formula is preserved under taking induced substructures. Examples 6.5 : (1) Colorability with p colors is defined by the ∃SO u,c sentence ∃C 1 , ..., C p ∀x, y.θ(x, y) where C 1 , ..., C p are unary relations, such that C i defines the vertices colored by i; the set of vertices is linearly ordered (cf. Example 3.5); the QF formula θ(x, y) is the conjunction of the following disjunctions (where A =⇒ B stands for ¬A ∨ B):

(i) C 1 (x) ∨ ... ∨ C p (x) (ii) C i (x) =⇒ ¬C j (x), for all 1 ≤ i < j ≤ p, (iii) x < y ∧ edg(x, y) ∧ C i (x) =⇒ ¬C i (x), for all 1 ≤ i ≤ p.
The construction of Proposition 6.2 produces the SAT problem of Example 3.2.

(2) Proposition 3.7 shows that the property "twd(G) ≤ k" is characterized by an ∃SO u,c sentence of the form ∃A, S 1 , ..., S k ∀x, y, z.ψ(x, y, z) where the existentially quantified binary relations are :

A, the ancestor relation of the normal forest T to be constructed, encoded by the variables a u,v , S i , for i = 1, ..., k: these relations, corresponding to the Boolean variables s u,v,i , are intended to express that each set f * T (u) has at most k elements.

(3) The case of clique-width is more complicated: the SAT problem CWD k,λ (G) used to check whether cwd(G) ≤ k (Theorem 4.9) has Boolean variables, e.g., c u,v,i , that depend on i < λ := nk + 1, hence, that do not correspond to binary relational variables depending only on k.

Most clauses of the SAT problems constructed in Section 4.1 implement an ∃SO u,c sentence (depending on k and λ). The only exceptions concern the clauses r v,i ∨ g 1,v,i ∨ g 2,v,i ∨ ... ∨ g (v-1),v,i of Definition 4.5(a) expressing that if vertex v is not representative at level i, it is not minimal in its group. They are defined for all integers i ∈ [1, λ] and vertices v (we recall that vertices are in [n]). They cannot be written (for each i a) as a universal FO formula written with a unary relation symbol R i such that R i (v) expresses the truth of r v,i and a binary relation symbol S i such that S i (u, v) expresses the truth of g u,v,i .

This encoding of representativity uses clauses of length at most n, that depends on the number n of vertices, which is not the case for ∃SO u,c properties, as we show next in Construction 6.6, where the maximal length of a clause depends only on the CQF formula θ.

The article [START_REF] Heule | A SAT approach to clique-width[END_REF] distinguishes this representative encoding, from a direct encoding, whose set of clauses implements an ∃SO u,c sentence. As it is computationally less efficient, the representative encoding is prefered. However, the construction using the direct encoding yields an ∃SO u,c expression of the property that G has a derivation of height λ and width at most k. Construction 6.6 : SAT problems of polynomial sizes from ∃SO u,c sentences.

Let P be a graph property defined by a sentence ϕ of the form ∃R 1 , ..., R p .ψ where : ψ is ∀y 1 , ..., y q .θ(y 1 , ..., y q ), θ is a CQF formula i∈ [r] δ i (y 1 , ..., y q ), where each δ i is a disjunction of atomic and negated atomic formulas.

The relation symbols are edg, <, = as we consider possibly ordered graphs, together with the quantified variables R 1 , ..., R p .

Given a graph G defined by (V, edg, <, =), we construct a SAT problem Σ P (G) to check P on G. Each formula δ i (y 1 , ..., y q ) can be written α i =⇒ β i where β i is the disjunction of the atomic formulas in δ i of the form R s (...) or their negations, and α i is the conjunction of the negations of the atomic formulas in δ i relative to edg, <, =.

As in Proposition 6.2, the Boolean variables are R j (a 1 , ..., a ρ(Rj ) ) for all j = 1, ..., p and ρ(R j )-tuples (a 1 , ..., a ρ(Rj ) ) of vertices. With each conjunct δ i (y 1 , ..., y q ), we associate the clauses β i (a 1 , ..., a q ) such that α i (a 1 , ..., a q ) is true in G. Each of them is a disjunction of litterals over the variables R j (a 1 , ..., a ρ(Rj ) ).

The desired SAT problem Σ P (G) is the set of all such clauses. Its number of clauses is bounded by r. |V | q . The size of a clause is bounded by its number of disjuncts.

With these hypotheses and notation : Proposition 6.7 : The graph G satisfies P if and only if the SAT problem Σ P (G) is satisfiable. Furthermore, the tuples of relations R 1 , ..., R p that confirm the validity of P (G) can be determined from the Boolean assignments that satisfy Σ P (G). The size of Σ P (G) is polynomial in that of G.

Proof : Clear from Construction 6.6.

Examples and remarks 6.8 :

(1) We consider directed loop-free graphs and the property defined by the ∃SO (it is not ∃SO u ) sentence : (2) Motivated by the aim of discovering bounds (Section 1.2) for hereditary properties P of graphs (or more generally of relational structures), we want to obtain easily the clauses for checking P (Ga) from those for checking P (G), where a is any vertex. (This is useful only if G does not satisfy P ).

If Φ is a SAT problem for checking P (G) and a is a vertex of G, we denote by Φ\a the SAT problem obtained by deleting all clauses containing a litteral built with a. Does it check P (Ga)? We define a class of sentences for which this is true.

(3) Proposition 6.10(2) applies to SAT problems defined from safe ∃SO u,c sentences. It may not apply to a SAT problem for a hereditary property constructed from an ∃SO sentence. We go back to Example 6.5 [START_REF] Courcelle | From tree-decompositions to clique-width terms[END_REF]. We observed that most clauses for checking cwd(G) ≤ k are based on ∃SO u,c sentences that are actually safe, so that the deletion method of Proposition 6.10(2) can be applied. However, for encoding representativity of vertices, we use the clauses r v,i ∨ g 1,v,i ∨ g 2,v,i ∨ ... ∨ g (v-1),v,i .

Assume we delete vertex 1. If we delete all clauses where vertex 1 occurs, then all clauses of type r v,i ∨g 1,v,i ∨g 2,v,i ∨...∨g (v-1),v,i disappear for v > 1. The representativity of vertices for G -1 is not described correctly in the resulting SAT problem CWD k,λ (G)\1.

Conclusion

We have clarified from a logical point of view constructions of SAT problems for checking ∃SO graph properties, along the lines of [START_REF] Heule | A SAT approach to clique-width[END_REF][START_REF] Samer | Encoding treewidth into SAT. Theory and Applications of Satisfiability Testing[END_REF]. It is easy to see that the verification of an existential second-order graph property reduces to a SAT problem. However, the resulting SAT problem may be much too large to be effectively solvable.

Although of polynomial size, actually O(n 5 ) in the number of vertices of the given graph G, the SAT problem that checks whether cwd(G) ≤ k cannot be solved in many interesting cases. This difficulty depends of the available SAT solver.

8 Appendix: Constructing a term from a derivation.

We adapt the construction of [START_REF] Heule | A SAT approach to clique-width[END_REF] on the basis of the variables s v,a,i which define labels.

We will build terms that use parallel relabellings (cf. Definition 2.1) and operations ⊕ with a single argument. A postprocessing can "clean" the term, so that it can be fed to a fly-automaton (cf [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Online software TRAG[END_REF]).

Given a graph G = (V, E), we assume that a derivation D of height λ and width at most k is known from the positively assigned variables c u,v,i , g u,v,i and s v,a,i (cf. Theorem 4.9). We recall that the validity of s v,a,i implies that r v,i is true, i.e., that v is representative 15 at level i. Hence, r v,i is equivalent to "there is a label a such that s v,a,i is true." At level 0, every vertex is a group and a component: it is representative with label 1 (see point 2) below).

Notation and observations. 8.1 1) Labels are taken from the set [k] and variables a, b, c designate labels. However, in examples and in the terms produced by TRAG, labels are letters a, b, c, ... rather than numbers (cf. Example 4.25). Vertex sets are of the form [n]. (A vertex set {1, 3, 6} is not allowed).

2) It is convenient for uniformity in the description below, to use s v,1,0 defined as always true.

3) For each component C of level i, we define G(C, i) as the induced graph G[C] labelled as follows: a vertex u has label a if its group at level i has representative vertex v and s v,a,i is true.

We will construct terms t(C, i) that define the labelled graphs G(C, i). Clearly, G will be defined by the term t(V, λ).

4) Each component C of level i will be encoded by the unique pair (v, i) such that v is the minimal vertex among the representative ones of some group in the component. At level 0, each component {v} is encoded by (v, 0). Then, (v, i) encodes the component of v at level i > 0 if and only if : r v,i is true and, if u < v and r u,i is true, then c u,v,i is false (otherwise, v is not the minimal representative vertex in its component of level i).

5) Label i (C), defined as the set of labels of the vertices of G(C, i) is: the set of a ∈ [k] such that s v,a,i is true for some v in C (i.e., a is the "group number" of some group in C of level i).

The arc 1 -→ 2 is defined twice.

(2) Consider the graph 1 -→ 2 -→ 3 -→ 1 together with 4 as an isolated vertex, that we check for clique-width 3 with derivations of height t = 4-3+1 = 2. The following derivation is correct:

T 2 : {1, 2 | 3 | 4} T 1 : {1 | 2 | 3}, {4}
T 0 : {1}, {2}, {3}, {4}.

All arcs are defined at level 1, that is the smallest level at which their ends are in a same component. Because of this minimality requirement, no arc is defined at level 2. Without it, we would get 1 -→ 3 that is not in the given graph.

  (a) If P (G) holds, this is a failure. Choose another graph G to continue. (b) If P (G) does not hold, we call G a candidate. We check whether P (Gu) holds for all vertices u. (b.1) If so, then G ∈ M inEx(P ). (b.2) Otherwise, each graph Gu such that P (Gu) does not hold is a new candidate, of smaller size than G. We repeat Step (b) for each such candidate. (c) At the end, we get all bounds H of P that are induced subgraphs of G. (d) One keeps only one bound in each isomorphic class if one is interested in the set of bounds u.t.i.. If in Step (b.2), the graph Gu is isomorphic to Gv, we need only check one of them if we want to determine the set of bounds u.t.i.. Examples 2.2 use this algorithm.

Examples 2 . 4 :

 24 The path abcd is not a cograph. It is a probe cograph, because we get a cograph by adding one of the edges ac or bd or ad . The path P 5 = abcde is a probe cograph because we get a cograph by adding the edges ac and ce. This is the only way to make it into a cograph. The path P 6 is a bound of the class of probe cographs. See [4]. Definition 2.5 : Relative clique-width.

Examples 2 . 6 :

 26 (a) Consider the term: t = add a,b (relab c→a (add b,c (⊕[a(1), b(2), ⊕{a(3), add a,c (⊕[a(4), c(5)])}]))).

Definition 4 . 1 :

 41 Derivations.

Definitions 4 . 5 :

 45 Representative vertices and group numbers.

1 .

 1 For all 1 ≤ i ≤ λ and all distinct u, v, w, x ∈ V : if uv, uw, xv ∈ E and xw / ∈ E, we set the clause g {u,x},i ∨ g {v,w},i ∨ c {u,v},i-We define in this way at most λ |E| + 2λ |E| (n -2) + λ |E| (n -2)(n -3)/2 < λ |E| n(n -1)/2 clauses and at least λ |E| (n -1) ones.Theorem 4.9 : A directed graph G with n vertices has clique-width at most k if and only if the SAT problem CWD k,λ (G) consisting of D(n, λ)∪W (n, λ, k)∪ Dir(n, λ, G) has a solution for λ := nk + 1.Proof : Immediate consequence of Theorem 4.2.For any λ, the problem CWD k,λ (G) has a solution if and only if cwd(G) ≤ k witnessed by a term of height λ and width at most k. This property is hereditary as one checks easily by inspecting Definition 4.1.For λ = n-k+1, CWD k,λ (G) needs approximately n((n+1) 2 -k 2 ) variables and a number of clauses bounded by n 2 (nk)(|E| + kn), which gives O(n 4 (nk)). The number of clauses is O(n 3 (nk)) for a p-sparse graph, i.e., such that |E| ≤ pn for fixed p. If k gets larger, the number of variables and clauses decreases, so that checking that cwd(G) ≤ k gets easier, which matches intuition. Remarks 4.10 : Let G be directed and G ′ := U nd(G). It is also directed, with possibly more arcs as we may need to add v → u for some arcs u → v. The arc property clauses in Dir(n, λ, G) and Dir(n, λ, G ′ ) are the same. Every neighborhood property clause of Dir(n, λ, G ′ ) is in Dir(n, λ, G): this is clear from Definition 4.8. There is no similar general inclusion for path property clauses. We give two examples.

  5 and c 1,2,2 , c 4,5,2 , c 4,6,2 , c 1,3,2 , c 3,4,2 and c 1,4,2 .

Definition 4 . 14 :

 414 Linear derivations. (a) A k-derivation is linear if each level has at most one component having more than one vertex.

Theorem 4 .

 4 16 : A graph G with n vertices has linear clique-width at most k if and only if the SAT problem consiting of CWD k,λ (G) ∪ L(n, λ) where λ = nk + 1 has a solution.

Example 4 . 18 :

 418 The clique-width of the (unlabelled) cycle C 4 = 1-2-3-4 -1 is 2. If we define Lab(1) = Lab(2) := a, Lab(3) := b then, it is 3: we can construct C 4 with labels a, c, b, c respectively for 1, 2, 3, 4 and then, we relabel c into a. If we require that Lab(1) = Lab(2) = a and Lab(3) = Lab(4) = b then, the clique-width of C 4 labelled in this way is 4. Definition 4.19 : Vertex labelling clauses. Let be given a partially labelled graph G = (V, E, Lab) such that Lab(V ) = [p]. Let k ≥ p and λ be the height of an intended term defining (V, E, π) (cf. Definition 2.1(b)).

Theorem 4 .

 4 20 : A partially labelled graph G = (V, E, Lab) has cliquewidth (resp. linear clique-width) at most k if and only if the set of clauses CWD k,λ (G) ∪ P (n, λ, Lab) (resp. CWD k,λ (G) ∪ L(n, λ) ∪ P (n, λ, Lab)) where λ = nk + 1 has a solution. Proof : Follows from Theorems 4.9 and 4.16 and Definition 4.19.

Figure 1 :

 1 Figure 1: Petersen's graph and the skeleton of an optimal term.

t 1 =

 1 relab e,b (add c,e (add a,b (⊕(t 2 , t 3 )))).

t 2 =

 2 relab e,c (relab b,d (add b,e (add c,d (⊕(t 4 , t 5 ))))).

t 3 =

 3 add d,e (add b,d (⊕(b[2], d[3], e[10]))).

t 4 =

 4 add a,e (add a,d (⊕(a[START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF], d[START_REF] Courcelle | The monadic second-order logic of graphs VIII: Orientations[END_REF], e[START_REF] Courcelle | Online software TRAG[END_REF]))).t 5 = add a,b (add a,c (⊕(c[6], a[START_REF] Courcelle | On quasi-planar graphs: Clique-width and logical description[END_REF], b[START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]))).The skeleton of t 0 is shown to the right of Figure1.The following families (from which we remove the singletons and the set[START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] of all vertices) are compatible with the derivation D corresponding to t 0 : B : {1,5,9}, {6,7,8}, B ′ : {2,3}, {1,5,6,7,8,9}, B ′′ : {2,3,10}, {1,5,9}, {6,7,8}.The following is not :B ′′′ : {2,3,4,10}, {1,5,9}, {6,7,8} because the first block overlaps the component {1,2,3,5,6,7,8,9,10}. The component {2,3,10} of D is the union of the blocks {2,3} and {10} of B ′ . The component {1,5,6,7,8,9} of D is the union of the blocks {1,5,9}, {6,7,8} of B ′′ .The family B is described by the unit clauses: b 1,1 , b 5,1 , b 9,1 , b 6,1 , b 7,1 , b 8,1 b 6,2 , b 7,2 , b 8,2 , b 1,2 , b 5,2 , b 9,2 .

Figure 2 :

 2 Figure 2: Oriented Paley graph with 7 vertices

Examples 5 . 6 :

 56 We illustrate Proposition 5.5(1). (1) Let G be the cograph (1 ⊕ 2) ⊗ (3 ⊕ 4) and G ′ be G augmented with vertex 5, adjacent to vertices 2 and 4. Then, G is defined by add a,b (⊕[a(1), a(2), b(3), b(4)]) and G ′ by add b,a ′ (add b,b ′ (⊕[b(5), relab b→a (ADD(⊕(a(1), a ′ (2), b(3), b ′ (4)))])),

t 4 :

 4 = ⊗[⊕(1, 2), ⊕(3, 4)], t 5 := ⊗[⊕(5, 6), ⊕(7, 8)], t 2 := ⊕(9, 10) and t 3 := ⊕(11, 12).The graph G obtained by adding to H a new vertex 13, adjacent to vertices 2, 4, 6, 8, 10, 12, has clique-width 4. Hence, the upper-bound of Proposition 5.5(1) can be reached if k = 2. A smaller upper-bound than 2k may exist for larger values of k. Open question 5.7 : When can one improve the bounds of Proposition 5.5 ?

  ∃x.θ(..., x, ...) is replaced by a∈V θ(..., a, ...), ∀x.θ(..., x, ...) is replaced by a∈V θ(..., a, ...), edg(a, b), a = b and a < b are replaced by their truth values in (V, edg, ≤).

  f ∈M a∈V R(a, f (a)) hence transforms a formula of size O(n 2 ) into one of size O(n n+1 ) where n = |V |. This construction can be however tractable in some cases, as shown in Example 6.8(1) below.

  ∃R.(∃x.R(x) ∧ ∀x.[R(x) =⇒ ∃y.(edg(x, y) ∧ R(y))]). It is valid if and only if the considered graph contains at least one directed cycle. (This property is not hereditary.) The vertices of such a cycle satisfy R. The formula ∀x.[R(x) =⇒ ∃y.(edg(x, y) ∧ R(y))] can be written : ∃R.(∀x.[¬R(x) ∨ ∃y.(edg(x, y) ∧ R(y))]. For a vertex set V, we obtain the existence of a unary relation R such that : a∈V [R(a) ∨ b∈V (edg(a, b) ∧ R(b))]. At first look, each conjunct R(a)∨ b∈V (edg(a, b)∧R(b)) can be rewritten as a conjunction of disjunctions of size more than 2 n , where n = |V |. However, each formula b∈V (edg(a, b) ∧ R(b)) can be replaced by the disjunction of the litterals R(b) such that a → b in G, which gives a SAT problem of size n + |E|. We need also the clause R(1) ∨ ... ∨ R(n) to express ∃x.R(x). The maximal length of a clause is n.

A similar reduction is done in[START_REF] Samer | Encoding treewidth into SAT. Theory and Applications of Satisfiability Testing[END_REF] for computing exact tree-width.

We do not claim that this property implies practical tractability, even by means of GLU-COSE[START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF].

The term "bound" translates the French term "borne" which means "boundary stone". We will use it and avoid conflicts with the independent notion of "upper-bound".

Exact clique-widths have been computed by TRAG[START_REF] Courcelle | Online software TRAG[END_REF] that implements the method of[START_REF] Heule | A SAT approach to clique-width[END_REF]

We write "at most" for the case of directed graphs having pairs of opposite arcs.

If the output is a normal forest, we make it into a tree by adding a root.

By adding O(n 4 ) more clauses, one could obtain a tree-decomposition (T, g) such that g(u) is the set of vertices v such that s u,v,i is true is a solution to T W D k (G).

Height is called length in[START_REF] Heule | A SAT approach to clique-width[END_REF], but we think of a derivation as encoding a tree, actually, the skeleton of a term.

In examples and in the terms produced by TRAG, letters a, b, c, ... replace numbers as vertex labels. Otherwise, there is confusion with the vertices that are positive integers.

0 Called "edge property clauses" in[START_REF] Heule | A SAT approach to clique-width[END_REF].

[START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF] The terms of clique-width n +

computed by TRAG for the grids G n×m such that m > n are actually linear terms.

2 TRAG rather writes t_0 = add_d_e(oplus(t_1,e[START_REF] Courcelle | On betweenness in order-theoretic trees[END_REF])) and ren_e_b instead of relab e,b . The clique-width is exactly 5.

[START_REF] Courcelle | From tree-decompositions to clique-width terms[END_REF] Paley graphs have q vertices where q = p r for a prime number p and q ≡ 3(mod .4). See[2,

22].

[START_REF] Courcelle | On betweenness in order-theoretic trees[END_REF] By using the fact that cographs are the graphs without induced paths P 4 .

[START_REF] Courcelle | The monadic second-order logic of graphs VIII: Orientations[END_REF] One might do otherwise, with less clauses. It is not clear how much this would affect the computation time for solving the SAT problem.

Definition 6.9 : Safe ∃SO u,c sentences An ∃SO u,c sentence ϕ can be written such that each formula δ i (y 1 , ..., y q(i) ) (cf. Construction 6.6) is α i =⇒ β i where β i is the disjunction of the atomic formulas in δ i of the form R s (...) and α i is the conjunction of the negations of the atomic formulas in δ i concerning edg, = and <. We assume that each variable y 1 , ..., y q(i) occurs in α i =⇒ β i .

We say that ϕ is safe if each variable occurring in α i also occurs in β i .

Proposition 6.10 : Let P be a graph property expressed by an ∃SO u,c formula ϕ and Σ P (G) be a SAT problem built with Construction 6.6 for a graph G. Let a be a vertex.

(1) We have Σ P (Ga) ⊆ Σ P (G)\a.

(2) If ϕ is safe we have Σ P (Ga) = Σ P (G)\a. Hence the SAT problem Σ P (G)\a checks correctly P (G-a). The tuples of relations that validate Σ P (Ga) are the restrictions to V -{a} of those that validate Σ P (G).

Proof : (1) A clause in Σ P (G-a) is also one of Σ P (G) and does not contain a. Hence, it is in Σ P (G)\a. If Σ P (G)\a is satisfiable, then so is Σ P (G-a) because of inclusion.

The inclusion of the sets of clauses may be strict.

(2) Conversely, let β i (b 1 , ..., b q ) be a clause in Σ P (G)\a, where a / ∈ {b 1 , ..., b q }. It arises from α i (b 1 , ..., b q ) =⇒ β i (b 1 , ..., b q ) where α i (b 1 , ..., b q ) is true and, because of safety, a does not occur in α i (b 1 , ..., b q ). Hence,

The tuples of relations that validate Σ P (G-a) are the restrictions to V -{a} of those that validate Σ P (G). (2) Here graphs may have loops. Let Property Q be defined by the following ∃SO u,c sentence that is not safe :

Let H be the graph a → c → b. Property Q does not hold for H as we should have R(a, b) and ¬R(a, b). However it holds for Hc with R = ∅.

We have ,y) for all x, y ∈ {a, b, c}. We also have:

Construction 8.2: A term from a correct derivation. The term is based on the tree of all components, where inclusion is the ancestor relation. The data for that are the positive variables c u,v,i . We use an induction on i.

At level 0, t(C, 0

At level i > 0 :

(ii) ADD C is the composition of the arc-defining operations --→ add a,b such that s u,a,i and s v,b,i are true, uv ∈ E, and u and v are in C but not in a same component at level i -1. If C is encoded by (w, i), then these conditions are expressed by the validity of

(iii) We define h(C ′ , C) = h that depends on C and C ′ , encoded as above by (w, i) and (u, i -1). We have

a is a label of a group of C ′ represented by w, that is, if s w,a,i-1 is true, and w is in the group of C with label b represented by x, that is, if s x,b,i is true, so that these conditions are expressed by the validity, for some w and x, of :

where v 1 , ..., v p are the vertices of C and a, b, ..., z are appropriate labels.

(2) If G is undirected, hence is a symmetric directed graph, the above construction works. However, in each composition ADD C , we have --→ add b,a whenever we have --→ add a,b . Both can be replaced by a unique occurrence of add a,b .

Theorem 8.4 : The construction is correct.

Proof : This fact follows from the definitions and an easy adaptation of Lemma 3.6 of [START_REF] Heule | A SAT approach to clique-width[END_REF]. We explain it nevertheless for justifying the construction of ADD C and the addition of arcs.

Assume that we have

where (w, i) encodes a component C at level i. The vertices u and v are representative in two different groups in C, respectively A and B. Hence, the operation --→ add a,b is in ADD C and adds an arc u → v.

Claim 1 : This operation adds arcs u ′ → v ′ for all u ′ ∈ A and v ′ ∈ B and no others. These added arcs are in G.

Proof: That no other arcs are added is clear as only the vertices in A (or B) have label a (or b).

If E contains no arc u → v ′ for some v ′ ∈ B then, the neighbourhood property yields that u and v are in a same component at level i -1. But we assumed the opposite. Hence,

for some u ′ ∈ A and v ′ ∈ B then, as we know that uv ′ ∈ E, u ′ v ∈ E and v, v ′ ∈ B, the path property yields that u and v are in a same component at level i -1. But we assumed the opposite.

Claim 2 : Every arc u ′ → v ′ of G is added in this way. Proof : Let C be the component at the lowest level i that contains u ′ and v ′ . We have i > 0. By the edge property, u ′ and v ′ are in different groups, say A and B of C. They have representative vertices u and v respectively. The proof of Claim 1 shows that uv ∈ E. For distinct labels a and b, we have s u,a,i ∧ s v,b,i . Hence, ADD C contains the operation --→ add a,b that defines the arc u → v and also u ′ → v ′ by Claim 1.

All other points of the construction are clear from the definitions. Remarks 8.5 : (1) Construction 8.2 produces terms with operations ⊕ of various arities. Those of arity 1 can be eliminated and those of arity more than 2 can be replaced by several operations ⊕ of arity 2.

This construction uses parallel relabellings relab h where h is a mapping. As said in Section 1, they can be replaced by a composition of elementary relabellings relab a -→b without needing new labels ([10] Proposition 2.118).

The produced terms may be redundant 16 [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] because arcs are added in a bottom-up way as early as possible. This means that an operation --→ add a,b can be applied to a graph having already an arc from an a-labelled vertex to a blabelled one. Consider the graph 1 -→ 2 ←-3 and the following derivation where | separates groups inside components.


Kariman Abelin-Genevois

Pascal Swider

Erik Estivalèzes

Jérôme Briot

Franck Accadbled

Jérôme Sales De Gauzy

Risk factors for adjacent segment degeneration after adolescent idiopathic scoliosis surgery (AIS)

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Open Archive TOULOUSE Archive Ouverte (OATAO)

OATAO is an open access repository that collects the work of Toulouse researchers and makes it freely available over the web where possible. Any correspondence concerning this service should be sent to the repository administrator: staff-oatao@listes-diff.inp-toulouse.fr Purpose: ldeal surgical management of adolescent idiopathic scoliosis (AIS) aims for an optimal correction of the deformity while preserving mobility. An unbalanced rigid spine puts the mobile segment at higher risk of disk degeneration. The goal of our study is to clarify the Iong term outcome of AIS after spinal fusion.

Method: Forty-five patients undergoing surgical treatment for AIS were prospectively followed with MRI at 2 years minimum follow-up. Modifications in total volume and nucleus size of the discs in the mobile segment were extrapolated from 3D reconstruction of the intervertebral discs. We analysed disc morphometric changes according to the fourth lumbar vertebra (LIV) position to the stable vertebra (SV), neutral vertebra (NV) and end vertebra.

Results:

In selective arthrodesis the main factors affecting the discs below fusion were the length of the free motion segment and position of LIV to SV and NV. In fusions extended to the lumbar spine, disc volumes were significantly influenced by the spino-pelvic morphology. Long term follow up (at average 5.5 years after fusion in 17 patients) however demonstrated the constant remodelling in the discs. Volumes remained in the range of postoperative values as hydration was constantly enhanced.

Conclusions: long spina1 fusions in AIS induce significant geometrical changes below the fusion. Significant differences were observed according to the level of distal fusion. Major mechanical forces applied to the junctional segments are transmitted through the intervertebral discs aggravated by the overloading mechanical stress between rigid and mobile segment.

Significance: Optimal positioning of the two first segments under a long spinal fusion for AIS is essential to avoid early degenerative changes and may protect from the adding on phenomenon. The authors define the concept of a disc stable zone.

To cite this version : Abelin

  This is an author-deposited version published in : http://oatao.univ-toulouse.fr/ Eprints ID : 15767 -Genevois, Kariman and Swider, Pascal and Estivalèzes,

	To link to this article :
	URL: http://link.springer.com/journal/11832/7/1/suppl/page/1

Erik and Briot, Jérôme and Accadbled, Franck and Sales de Gauzy, Jérôme Risk factors for adjacent segment degeneration after adolescent idiopathic scoliosis surgery: the intervertebral disc stability concept. (2013) In: EPOS 32nd

  Annual Meeting, 17 April 2013 -20 April 2013 (Athens, Greece).