Computing Twin-width with SAT and Branch & Bound

1 Introduction

Recently, Bonnet et al. [Bonnet et al., 2020] discovered the fundamental graph width measure twin-width based on a novel graph decomposition based on sequences of vertex contractions. They showed that bounded twin-width generalizes many previously known graph classes for which important problems are tractable, including first-order model checking (an important meta-problem in computational logic). The notion of twin-width is also helpful for problems beyond NP, like bounded-ones weighted model counting [Ganian et al., 2022]. Most notably, graphs of bounded treewidth, bounded clique-width, and planar graphs all have bounded twin-width [Bonnet et al., 2020]; hence twin-width provides a common generalization of other diverse notions. Due to its appealing properties, twin-width has already become the topic of extensive research [Bonnet et al., 2022f; Bonnet et All the mentioned algorithmic results for graphs of bounded twin-width require a certificate that the input graph's twin-width is bounded. So far, twin-width has been mainly studied from a theoretical and asymptotic perspective and very little is known about the computational aspects of twinwidth. An exception are the SAT encodings proposed by Schidler and Szeider [2022], which have been utilized for experiments on twin-width of model counting instances [Ganian et al., 2022] but still only scale to relatively small instances. The SAT encoding provided experimental insights and gave rise to the conjecture that Paley graphs of order n have twin-width (n-1)/2, later verified by Ahn et al. [2022]. Because of the great interest in the practical computation of twin-width, the organizers of the 2023 PACE competition 1 have chosen twin-width as the target problem.

This paper aims to advance our knowledge about the computational aspects of twin-width. In particular, we ask (1) whether the SAT encodings can be improved to admit better scalability and (2) whether algorithmic approaches different from SAT encodings are feasible and effective. We also ask for (3) structural results that allow us to prune the search space for twin-width decompositions explored.

Indeed, we could make considerable progress in all three points and provide an empirical evaluation..

1. We propose a new SAT encoding that is significantly more compact than the known SAT encodings and allows faster solving times. The encoding's small size results in improved scalability and the encoding's ability to find upper bounds for larger graphs.
2. We propose a new Branch & Bound algorithm BB-CCH that incorporates several new methods proposed in this paper. The caching and re-using of previous computations is a key contributor to BB-CCH's outstanding performance. BB-CCH is considerably faster than the SAT

1 Parameterized Algorithms and Computational Experiments Challenge (PACE), https://pacechallenge.org/2023/

• encodings and can compute reasonable upper bounds for large graphs far out of reach for the SAT encodings.
• We establish several results that can help to speed up the search for twin-width decompositions. The results include pre-and inprocessing techniques based on the new notion of a tri-twin and a result that allows us to assume a specific order of contractions (the elementary steps of twin-width decompositions) without losing optimality. Both help to significantly reduce the search space and speed up the twin-width computation.
• We evaluate our algorithms on two classes of benchmark graphs, structured graphs and graphs from the treewidth lib benchmark suite. The results show that our new SAT encoding scales better than the previous encodings, particularly for structured graphs. Furthermore, BB-CCH solves more instances in a shorter amount of time than any of the SAT encodings.

2 Preliminaries

A trigraph is an undirected graph G with vertex set V (G) whose edge set E(G) is partitioned into a set B(G) of black edges and a set R(G) of red edges. We consider an ordinary graph a trigraph with all its edges black. W.l.o.g., we assume that V (G) is lexicographically ordered. The set NG(v) of neighbors of a vertex v in a trigraph G consists of all the vertices adjacent to v by a black or red edge. We call u ∈ NG(v) a black neighbor of v if uv ∈ B(G), we call it a red neighbor if uv ∈ R(G), and denote the set of black and red neighborhoods of v by NG,B(v) and NG,R(v) respectively. Whenever G is clear from context, we drop G from the subscript. The red degree of a vertex v ∈ V (G) of a trigraph G is |NG,R(v)|. A d-trigraph is a trigraph where each vertex has red degree at most d, denoted by r(G) = d.

A bijection π:V (G) → V (H) between the vertex sets of trigraphs G and H is an isomorphism if for all u, v ∈ V (G) it holds that uv ∈ X(G) iff π(u)π(v) ∈ X(G), for X ∈ {B,R}. If an isomorphism between G and H exists, the trigraphs are isomorphic. If G = H then π is an automorphism. V (G) is partitioned into orbits where u, v ∈ V (G) belong to the same orbit if π(u) = v for some automorphism π of G.

A trigraph G′ is derived from a trigraph G by a contraction u → v, where u is being merged into v, as follows: V (G′ ) = V (G) \ {u} and every vertex in the symmetric difference NG(u)△NG(v) is made a red neighbor of v. If a vertex x ∈ NG(u) ∩ NG(v) is a black neighbor of both u and v, then v is made a black neighbor of x; otherwise, v is made a red neighbor of x. The other edges (not incident with u or v) remain unchanged. We denote a trigraph obtained from trigraph G by contracting u and v as Gu→v , and in the contraction u → v, u is the contracted vertex, and v is the contraction vertex. Gu→v is isomorphic to Gv→u , as only the name of the contraction vertex changes.

Twin-Width via d-Elimination Sequences. We give here a definition of twin-width via d-elimination sequences, slightly modifying the definition given by Schidler and Szeider [2022], as this definition is better suited for our purposes.

Let G be a trigraph, T a rooted forest-every tree in T is a rooted tree-with V (T) ⊆ V (G), set of non-roots N(T), and ≺ a linear ordering of N(T), where u ≺ v holds for any two vertices u, v ∈ N(T) such that v is the parent of u in T. We call T a contraction forest, ≺ an elimination ordering, and the pair D = (T, ≺) a twin-width decomposition of G. Let V ′ = V (G) \ N(T), k = |N(T)|, when we write V (G) = {v1,D, . . . , vk,D}∪V ′ such that v1,D ≺ · · · ≺ vk,D, then T and G define a sequence of trigraphs G0, . . . , Gk with V (Gi) = {vi+1,D, . . . , vk,D} ∪ V ′ . We denote by pi,D the parent of vi,D in T. We define Gi recursively as follows. For i = 0, we set G0 = G, and for 1 ≤ i ≤ k we set Gi = Gvi→pi,D i-1 .

We call the sequence G = G0, . . . ,Gk the elimination sequence for G defined by the twin-width decomposition (T, ≺); if for an integer d, all the Gi have a maximum red degree ≤ d, we call G = G0, . . . , Gk a d-elimination sequence. The width of the twin-width decomposition (T, ≺) of G is the smallest integer d such that (T, ≺) defines a d-elimination sequence.

Whenever k = |V (G)| - 1, we call (T,≺) a full twinwidth decomposition, and consequently ≺ a full elimination ordering, G0, . . . ,Gk a full elimination sequence, and T a full contraction forest. Observe that, in this case, T is a tree rooted at a single vertex. The twin-width of a trigraph G, denoted tww(G), is the minimum width over all See Figures 1 and 2 for examples. Recognizing graphs of twin-width 4 is NP-complete [Berg´e et al., 2022].

Partitions. The contractions of a graph G induce a partition on V (G) as follows. We view every vertex v ∈ V (G) as labeled by the singleton LG(v) = {v}. After contracting two vertices u → v, we label the contraction vertex v as LGu→v (v) = LG(u) ∪LG(v), and all other labels remain the same. Hence, the labels of a trigraph G = G0, . . . ,Gk derived from a graph G are always a partition of V (G). For 0 ≤ i ≤ k we refer to the partition of Gi as P(Gi) = {LGi (v) | v ∈ V (Gi) }.

3 Theory

For a graph with n vertices exist n!·(n-1)! 2n many possible sequences of contractions, each of them corresponding to a full twin-width decomposition. In this section, we discuss how we can reduce the number of twin-width decompositions we have to consider and speed up the twin-width computation for a given trigraph. We will use these results for our algorithms SAT-CPT and BB-CCH.

We first state two facts, let G be a trigraph, u, v ∈ V (G).

Fact 3.1. The red degree of any vertex w ∈ V (G) \ {u, v} can increase at most by one in Gu→v .

Fact 3.2. The red degree of any vertex w ∈ V (G) \ {u} can decrease at most by one in Gu→v .

3.1 Isomorphic Trigraphs

Trigraph isomorphisms can be used to eliminate many possible twin-width decompositions from consideration. Whenever we have a twin-width decomposition D = (T,≺) inducing a d-elimination sequence G = G0, . . . ,Gk and we have a full d-elimination sequence G = G′0 , . . . ,G′n-1 , such that Gk and G′k are isomorphic, then, G = G0, . . . ,Gk,G′k+1 ,G′n-1 is a full d-elimination sequence. Hence, we complete T and ≺ using the full twin-width decomposition, and we do not have to go through all possible contractions to complete D. Furthermore, whenever we cannot complete D to a full twin-width decomposition of width d, we know that no d-elimination sequence G = G′0 , . . . , G′j , where, for any i ∈ {1, . . . , j}, G′i is isomorphic to Gi, can be extended to a full d-elimination sequence.

Since checking if trigraphs are isomorphic can be computationally expensive, We give an easy sufficient criterion with the following theorem:

Theorem 1. Given twin-width decompositions D = (T,≺) and D′ = (T ′ ,≺′ ) inducing the d-elimination sequences G = G0, . . . ,Gk and G′0 , . . . ,G′k respectively. Whenever P(Gk) = P(G′k ), then Gk and G′k are isomorphic.

The theorem follows from the definition of partition coarsening introduced by Bonnet et al. [2020]. Hence, whenever two trigraphs represent the same partition, they are isomorphic. The opposite is not necessarily true, different partitions may represent the same trigraph. The following observations lead to complementary isomorphism checks:

Observation 3.1. Consider a trigraph G, vertices u, v,w ∈ V (G), and let A = R(Gu→w )△R(G) and B = R(Gv→w )△R(G). If either A = {vw} and B = {uw} or A = B = ∅, the trigraphs Gu→w and Gv→w are isomorphic.

Observation 3.2. If two vertices u, v ∈ V (G) belong to the same orbit, then for each u′ ∈ V (G) there exists a v′ ∈ V (G) such that Gu→u′ and Gv→v′ are isomorphic.

3.2 Twin Pre- and In-processing

We propose a new pre- and inprocessing method and extend the definition of twins from graphs to trigraphs.

Definition 1. Two different vertices u, v ∈ V (G) of a trigraph G are tri-twins if the following two properties hold: (i) (NB(u)△NB(v)) \ {u, v} = ∅, and (ii) NR(u) \ {v} ⊆ NR(v) or NR(v) \ {u} ⊆ NR(u).

Observation 3.3. Contracting tri-twins u, v does not increase the red degree of any vertex, and the red degree of the contraction vertex is at most the red degree of u or v.

Tri-twins have another interesting property, as the following theorem shows.

Theorem 2. Let Gj be a trigraph derived from some graph G via contractions, and u, v be tri-twins in Gj. Then, tww(Gj) ≥ tww(Gu→v j ).

The proof proceeds by showing that a full d-elimination sequence G = G0, . . . ,Gj, . . .Gn-1 can be modified such that u and v are contracted at position j + 1, which yields a d-elimination sequence Gu→v j = G′j+1 , . . . ,G′n-1 . Because contraction and contracted vertex are interchangeable, we can assume that V (Gn-1) = V (G′n-1 ) = {v}.

Theorem 2 allows us to apply the following pre- and inprocessing: whenever we have a partial elimination sequence up to Gj that we are trying to extend to Gj+1 and find tritwins in Gj , we can immediately contract them and disregard all other contractions. This can considerably reduce the number of elimination sequences we need to explore.

3.3 Ordering of Contractions

In general, the ordering of the contractions in an elimination sequence matters. Therefore, given a twin-decomposition (T,≺) of width d, changing ≺ may cause the width to increase. While generally true, the ordering of the contractions often does not matter, and reordering of many contractions still maintains the same width. This is important, as only having to consider different sets of contractions is less complex than also considering their ordering. Therefore, criteria that help us distinguish between cases where the ordering matters and does not matter, can significantly reduce the search space.

We give some intuition, before formalizing our criterion. Consider a twin-decomposition D = (T,≺) inducing a d-elimination sequence G = G0, . . . ,Gk-1. The key to this idea is Theorem 1: the maximum red degree of any vertex in Gk-1 only depends on the partition induced by the contractions. In particular, the order of the contractions does not matter, as reordering the contractions will still induce the same partition.

We can view the red degree of a vertex v ∈ V (Gk-1) by looking at Σk-1 j=1 |NGj,R(v)| - |NGj-1,R(v)|, i.e., the change of red degree from contraction to contraction. This allows us to incrementally maintain the red degrees: when adding one summand after the other, the intermediate result never exceeds d. Further, as long as this invariant holds for all vertices, we can freely move around the contractions.

In our criterion, we consider the contraction u → v to extend our elimination sequence G = G0, . . . ,Gk-1 to Gk = Gu→v k-1 . Let d′ = max{r(Gk), r(Gu→v k )}. The question we want to answer is: are there any vi,D ∈ (V (G)\V (Gk))\{u} such that there exists a twin-width decomposition D′ = (T ′ , ≺′ ) of Gi-1 that has width d′ and vi,D′ = u?

We give a general condition in the following theorem, but first, we introduce some necessary notations. Let D = (T, ≺) be a twin-width decomposition that induces a d-elimination sequence G = G0, . . . , Gk. For all 1 ≤ i ≤ k we define

Ri is the set of new red neighbors created when contracting vk,D and pk,D in Gi. Ni is the set of existing red neighbors of the two vertices. We can now formulate our theorem.

Theorem 3. Let G = G0, . . . ,Gk be the d-elimination sequence induced by a twin-width decomposition D = (T,≺) for trigraph G, and let j0 ∈ {0, . . . , k - 1} be the largest index such that at least one of the following conditions holds:

1. For some w ∈ (Rj0 \ Nj0 ) ∪ {vj0 } it holds that:
2. (a) |NGj0-1,R(w)| = d, and

1. |Rj0 ∪Nj0 | > d,
2. j0 = 0.

Then, for all j0 < j < k, there exists a twin-width decomposition Dj of G of width d where vj,Dj = vk,D and pi,Dj = pk,D.

Proof. We define for all 1 ≤ j ≤ k a twin-width decomposition Dj = (Tj , ≺j) as follows:

It can be verified that Dj is a twin-width decomposition of G of width d.

Intuitively, we need to ensure that the reordering does not lead to any vertices red degree exceeding d. Condition 1 states that any vertex whose red degree is increased by vk,D → pk,D cannot have red degree d or is eliminated. Condition 2 ensures that vk,D → pk,D does not cause the red degree of pk,D to exceed d. The following corollary is a special case.

Corollary 1. Let D = (T,≺) be a twin-width decomposition inducing a d-elimination sequence G = G0, . . . ,Gk. Whenever Gvk,D→pk,D k-2 is a d-trigraph and for all vertices v ∈ V (Gk) holds that either (i) |NGk,R(v)| < d, or (ii) |NGk-1,R(v)| = d, or (iii) |NGk-2,R(v)| ≤ |NGk-1,R(v)|, then Dk-1 is a d-elimination sequence.

This already gives us a strong criterion for finding equivalent reorderings of the given contractions. While it is easy to state a canonical criterion, such as that the contractions should occur in lexicographical order, except if it is necessary to execute them in a specific order. This can then be rather easily verified using Theorem 3. Converting a given elimination ordering into such a canonical ordering, on the other hand, is difficult, as each change in ordering requires re-evaluating the effects and which other vertices can then be reordered.

4 SAT Encoding

In this section, we propose our new compact SAT encoding SAT-CPT for determining the twin-width of a given graph G with n = |V (G)| many vertices. Schidler and Szeider [2022] proposed two SAT encodings, a relative (SAT-SSZ) and an absolute encoding. While their absolute encoding was comparatively succinct, using only O(n3 ) many clauses, it cannot solve any non-trivial instances. The relative encoding uses O(n4 ) many clauses, which makes it considerably larger, but outperforms the absolute encoding. Our encoding SAT-CPT implements the basic idea of the absolute encoding in a way that is even more succinct and performs much better. Our encoding uses O(n3 ) many clauses, which makes it more succinct than the relative encoding, and the different cardinality encoding, discussed in Section 4, makes SAT-CPT also significantly more succinct than the absolute encoding.

In the remainder of this section, we present SAT-CPT by, given a graph G and an integer d, constructing a propositional formula F(G, d) that is satisfiable if and only if tww(G) ≤ d. For this purpose, we encode a twin-width decomposition D = (T, ≺) and ensure that the induced elimination sequence G = G0, . . . ,Gn-1 is a d-elimination sequence. We start with our representation of D, followed by our representation of G0, . . . ,Gn-1, and finish the encoding with our handling of cardinality constraints. In the last part, we discuss optional techniques to speed up the solving process.

Encoding the Twin-Width Decomposition. We represent D by using for each u ∈ V (G) the variables vu,t and pu,t, where vu,t is true if and only if vt,D = u and pu,t is true if and only if pt,D = u. Since the maximum red degree of a trigraph with k vertices is k-1, we can limit t to 1 ≤ t < n-d-1 and eliminate the last d + 2 vertices in any order. Therefore, encoding D takes asymptotically O(n2 ) many variables, where the actual number depends on d.

Both sets of variables pv,t and vv,t, v ∈ V (G), 1 ≤ t < n - d - 1, are constrained such that exactly one vertex is eliminated at once and that vt,D ≺ pt,D holds.

This way of encoding D splits the definition of T between the variables vu,t, and pu,t, as pt,D can only be determined using both sets of variables. This is a significant difference to both the absolute and relative encoding by Schidler and Szeider [2022]: both encodings use variables that directly represent pu,t. Our way of encoding T allows us to use only cubically many clauses, as we will discuss next.

Red Edges. Before we can constrain the red degrees of the vertices, we have to encode G1, . . . ,Gn-d-2. We use variables rt,u,w for all 1 ≤ t < n - d - 1 and u, w ∈ V (G) such that u is lexicographically smaller than w. A variable rt,u,w is true if and only if uw ∈ R(Gt).

The asymptotic succinctness of SAT-CPT is due to how the semantics of rt,u,v is encoded. The red edges of a trigraph Gt with 1 ≤ t < n - d - 1 are encoded in three steps. First, we maintain all red edges from Gt-1, which is straightforward. Next, we encode the new red edges between pt,D and vertices u ∈ ((NG,B(vt,D)△NG,B(pt,D)) ∩ V (Gt)) \ {pt,D}. The constraints are straightforward, as we can easily compute NG,B(vt,D)△NG,B(pt,D) when creating the encoding, and add the condition that u must not yet have been eliminated.

Finally, we encode that for all u ∈ NGt-1,R(vt,D) it must hold that u = pt,D or u ∈ NGt,R(pt,D), i.e., red neighbors get transferred from the contracted to the contraction vertex. Here, splitting the encoding of the contraction and the contracted vertex pays off. We use auxiliary variables mt,u for all 1 < t < n - d - 1 and u ∈ V (G) that are true if and only if uvt,D ∈ R(Gt-1). The desired property can then be easily encoded while maintaining the number of clauses in O(n3 ); here, SAT-SSZ requires O(n4 ) many clauses for encoding the elimination sequence.

Cardinality Constraints. We ensure that the red degree of any vertex never exceeds d using cardinality constraints that encode conditions of the form |NGt,R(u)| ≤ d.

SAT-SSZ uses one cardinality constraint for each vertex in each trigraph of the elimination sequence. Hence, the encoding uses n2 many cardinality constraints. Since a cardinality constraint on its own adds O(n · logn) many variables and O(n2 ) many clauses [Bailleux and Boufkhad, 2003; Sinz, 2005], this adds O(n4 ) many clauses in total.

We use Facts 3.1 and 3.2 for a much more succinct solution. Since only the red degree of the contraction vertex can increase by more than one in a single contraction, we use the following trick. First, we constrain the red degree of the contraction vertex in each trigraph using totalizer cardinality constraints [Bailleux and Boufkhad, 2003]. This adds n - d - 2 many cardinality constraints.

Next, we constrain each vertex using an adapted sequence counter [Sinz, 2005]. This sequence counter uses the fact that all vertices other than the contraction vertex can change their red degree by at most one during a single contraction. Hence, for each v ∈ V (G) and 1 ≤ t < n - d - 1, the counter changes as follows from t - 1 to t: (i) whenever v = pt,D, the counter uses the corresponding totalizer constraint to determine the red degree, (ii) whenever v has a red edge to both the contraction and contracted vertex in Gt-1, the counter decreases by one, (iii) whenever v has a red edge to either the contraction or contracted vertex in Gt-1, the counter stays the same, and (iv) whenever v has neither a red edge to the contraction nor the contracted vertex in Gt-1, but a red edge to the contraction vertex in Gt, the counter increases by one.

In total, we use only 2 · |V | - d - 2 many cardinality constraints, each adding O(n2 ) many clauses, which are significantly fewer variables and clauses compared to SAT-SSZ.

Symmetry Breaking. We use two ideas from Section 3 for symmetry breaking, often speeding up the solving process. First, we use Observation 3.2 to restrict the choices for vu,1 to a single vertex per orbit. Further, we encode Corollary 1 for more symmetry breaking.

For encoding Corollary 1, we require the definition of a critical vertex: let t ∈ {2, . . . , n - d - 2} and u ∈ V (G), then u is a critical vertex in Gt, if |NGt,R(u)| = d, |NGt-1,R(u)| = d-1, and |NGt-2,R(u)| = d. We use this for vertices u,w ∈ V (G) where u is lexicographically smaller than w. Whenever vt,D = u and vt-1,D = w it must also hold that either |NGt,R(pt,D)| = d and |NGt-1,R(pt,D)| < d, or any vertex u ∈ V (Gt) is critical. This enforces a lexicographical ordering and thereby eliminates equivalent twinwidth decompositions. We can express this with O(n2 ) many variables cu,t, 2 ≤ t < n - d - 1 and u ∈ V (G), where cu,t is true if and only if u is critical in Gt.

It seems that encoding Theorem 3 would improve the performance even further. Unfortunately, this doubles the encoding size, while the performance gains do not compensate for the increase in size.

5 Branch &Bound

In this section, we propose our branch & bound algorithm BB-CCH, shown in Algorithm 1. The algorithm incrementally constructs a twin-width decomposition, adding one contraction in each recursive call and thereby constructing the elimination sequence. In each recursive call, whenever we find tri-twins, we immediately contract them (Theorem 2), and skip all other contractions (Line 5). Otherwise, the algorithm considers all possible contractions, and prioritizes those contractions that minimize the maximum red degree.

Central to the algorithm is the contraction filtering in Line 9. We can remove any contraction from consideration, where a rule applies. The given order ensures that computationally more expensive rules are applied later.

The simplest rule is that no trigraph should reach or exceed the upper bound, which is verified first. The orbit rule states that only the contractions of one vertex per orbit are considered; as stated in Observation 3.2. The quick isomorphism rule states that, given two contractions u → v and u′ → v′ with u ̸= u′ that derive isomorphic trigraphs according to Observation 3.1, we only perform one and filter the other. Finally, we reuse previous results from a cache.

Caching for Isomorphisms. The algorithm's core idea is based on the idea to cache the results for partial elimination sequences. Whenever we have computed all possible extensions of Gi to a full elimination sequence, we know the lowest integer best such that there exists a best-elimination sequence Gi, . . . ,Gn-1. In case, every possible extension reaches or exceeds the upper bound ub, we use best = ub. We then store (Gi, best) in our cache, where Gi is the key used to access the result (Line 20). In later iterations, whenever the current trigraph is isomorphic to a trigraph in a cache entry, we can use the cached result instead of computing all extensions (Line 9).

Instead of the trigraph itself, we use the partition of the trigraph as the key due to Theorem 1. This requires less memory and comparing two partitions is faster than comparing two trigraphs. The potential downside of using the partition is that a trigraph can be represented by multiple partitions. Consequently, using the trigraph as the key would increase the chance for a successful lookup. In our experiments, using the trigraph over the partition as the key could increase the num-

Algorithm 1 Branch & Bound Algorithm for Twin-Width

Input: A graph G Output: The twin-width of the graph. 1: Let ub = |V (G)| - 1 2: return TWW RECURSION(G, 0) 3: function TWW RECURSION(Gi, d) 4: if |V (Gi)| = 1 then return 0 5: if any u, v ∈ V (Gi) are tri-twins (Theorem 2) then 6: return TWW RECURSION(Gu→v i , d) d ← max(d, r(Gi)) ▷ Add all possible contractions to queue. 7: Q← { (u, v) | u, v ∈ V (Gi), u lex smaller v } ▷ Filter queue entries. 8: for all (u, v) ∈ Q where 9: Maximum red degree of Gu→v i reaches ub, or (i = 0 and automorphism (Observation 3.2)), or Quick isomorphism check (Observation 3.1), or Gu→v i is in partition cache (Theorem 1), or Reordering succeeds (Theorem 3), or Gu→v i is in graph isomorphism cache do 10: Q ← Q \ (u, v) ▷ Process queue and recurse. 11: best ← ub 12: while |Q| > 0 do 13: Select (u, v) ∈ Q minimizing r(Gu→v i ) 14: Q ← Q \ (u, v) 15: r ←TWW RECURSION(Gu→v , d) 16: if r < best then 17: Clear caches. 18: best ← r 19: ub ← max(best, d) 20: Store best in the two caches. 21: return max(d, best)

ber of successful cache lookups by less than 1%, which does not compensate for the decreased performance. We name this cache the partition cache.

We sometimes use a second cache, the graph isomorphism cache, where we use the canonical trigraph as the key: if two trigraphs are isomorphic than they have the same canonical trigraph. Hence, using the canonical trigraph increases the chances for a successful cache lookup. The canonical trigraph is found using the graph automorphism tool nauty [McKay and Piperno, 2014]. Unfortunately, computing the canonical trigraph takes very long compared to all other operations in a recursive call, and storing the whole trigraph takes up considerable memory. Therefore, we use it only for instance specific parts of the elimination sequence, where successful lookups are most likely.

Contraction Reordering. Let G = G0, . . . ,Gk be the current d-elimination sequence in our recursive call and we consider extending it to Gk+1 = Gu→v k . Before we perform the contraction, we compute j0 from Theorem 3. Hence, we check if there is a twin-width decomposition, where u ≺ vk,D and the same contractions are performed, just in a different order, such that the twin-width decomposition still induces a d-elimination sequence.

We perform the following partition cache lookups, whenever j0 < k - 1. For all j0 < j ≤ k, we check whether P (Gu→v j ) is in our partition cache; if so, and the cached result is larger than d, we know that we cannot extend our current elimination sequence to a full d-elimination sequence.

This concludes the description of BB-CCH. Next, we discuss our experimental evaluation of our new methods.

6 Experiments

We implemented SAT-CPT and BB-CCH in C++ compiled with GCC 7.5.0 2 . We used nauty 2.8.6 [McKay and Piperno, 2014] 3 as a libary for detecting trigraph isomorphisms and automorphisms, as well as Cadical [Biere et al., 2020] 4 as a SAT solver. We use standard hash maps as caches and a simple least recently used rule to manage a cache's memory consumption. We compare our methods to the relative SAT encoding (SAT-SSZ) by Schidler and Szeider [2022] 5 . We ran the experiments on servers with two AMD EPYC 7402 CPUs, each with 24 cores running at 2.8 GHz, and using Ubuntu 18.04.

Structured Graphs. We start our experiments by looking at graph families where the number of vertices can be adapted. We choose from each family a graph whose size makes determining the twin-width difficult but possible. We examine the results for 5 different graphs: The Paley-73, Grid 8 × 6, and Rook 6 × 6 graphs as they were used by Schidler and Szeider [2022], as well as the line graph for the complete graph K10, and the Queen 7 × 7 graph. Table 1 shows that SAT-CPT is indeed much more succinct than the previous encoding. This succinctness reflects itself in the runtime, where SAT-SSZ consistently required much more time than SAT-CPT. In Table 1, we omit the data for BB-CCH, as it solved all five instances within a second. Indeed, BB-CCH could solve the Rook 20×20, Queen 13×13, Line K25, and Paley-421 graphs within a minute. Unfortunately, we could not determine the twin-width of larger grid graphs.

Treewidth Lib. We expand our comparison to the Treewidth Lib 6 instances. These instances are used as benchmarks for computing treewidth, a related width measure, and give a wider variety of graphs. We used all instances with 20 to 200 vertices and tested them using a 6-hour time limit and 32 GB memory limit. All three methods were most effective for graphs of up to 50 vertices. Out of these 25 instances, only one remained unsolved. Many of the remaining 217 instances were too difficult for any method. Nonetheless, the largest solved instance had 197 vertices.

2 The source code is available under https://doi.org/10.5281/ zenodo.7944399 and https://github.com/ASchidler/tww-bb. Experimental results are available under https://doi.org/10.5281/zenodo. 7944391

3 https://pallini.di.uniroma1.it/

4 https://github.com/arminbiere/cadical

5 https://github.com/ASchidler/twin width

6 http://www.cs.uu.nl/research/projects/treewidthlib/

Table 2 shows how many instances the different methods solved, how often an upper bound could be found, and how comparatively good this upper bound was. BB-CCH solved by far the most instances and was also much faster than the other methods: on all instances solved by both BB-CCH and SAT-SSZ (on average in 802 seconds), BB-CCH was faster (on average 107 in seconds). Interestingly, BB-CCH also produced upper bounds for all instances that were as good, and mostly better, than those obtained by the SAT encodings.

The comparison between the two SAT encodings suggests that SAT-SSZ performed better than SAT-CPT, as the former solved more instances. On closer look, SAT-CPT found more and better twin-width decompositions than SAT-SSZ. Furthermore, SAT-CPT also found more optimal twin-width decompositions but failed to show optimality. Hence, SATCPT is the better encoding for obtaining good twin-width decompositions, particularly for structured graphs. SAT-SSZ performed better for finding provably optimal twin-width decompositions on unstructured graphs. Finally, the scalability of SAT-SSZ is restricted by its size, while SAT-CPT can be used for larger graphs.

Difficult Instances. In the last part, we examine instances that were difficult for BB-CCH and how well the different methods proposed in Section 3 performed in practice. Table 3 shows the results. By far, most contractions are filtered due to reaching the upper bound (Exceeded). Interestingly, the ratio between recursive calls and successful partition cache lookups (PCache) is roughly equal for all instances, while the other methods performed very instance specific. This shows how effective caching is and that each method is important to adapt to different instances, as each method performed well for at least one instance in Table 3.

7 Conclusion

We have advanced our knowledge about the computational aspects of twin-width in several ways. We proposed two approaches for computing the twin-width of graphs, SAT-CPT and BB-CCH, utilizing new theoretical results on twin-width decompositions. These theoretical results are of independent interest as they might be helpful for other twin-width algorithms developed in the future.

SAT-CPT's advantage over its predecessor SAT-SSZ lies in being significantly more compact and scalable to larger instances. BB-CCH's advantages include being significantly faster than the SAT approaches and being able to compute good upper bounds for the twin-width of graphs much larger than SAT encodings can handle.

We hope that our results bring the compelling theoretical concept of twin-width a step closer to some practical use in the future. Further, as practical solvers can often help to verify theoretical results, we hope that computing the twin-width or good upper bounds for twin-width can provide new insights for researchers working on twin-width.

Future work can build upon and extend our theoretical results to improve the performance of BB-CCH and SAT-CPT, which could benefit from external symmetry-breaking tools.

Acknowledgments

We acknowledge the support from the Austrian Science Fund (FWF), projects P32441, P36420, and W1255; and from the Vienna Science and Technology Fund (WWTF), project ICT19-065.