Enumerating Potential Maximal Cliques via SAT and ASP

1 Introduction

Bounded treewidth of graphs and its generalizations to hypergraphs are central structural restrictions that characterize tractable fragments in a variety of settings, from constraint satisfaction [Freuder, 1985; Dechter, 2006], discrete optimization [Bodlaender and Koster, 2008] and knowledge representation [Gottlob et al., 2010] to probabilistic reasoning [Lauritzen and Spiegelhalter, 1988; Darwiche, 2003]. Determining treewidth and generalized hypertreewidth is NPhard [Arnborg et al., 1987; Gottlob et al., 2009], which makes the development of practical algorithms for computing the associated optimal decompositions a non-trivial challenge. In answer to this challenge, various types of exact algorithms, ranging from specialized algorithms [Gogate and Dechter, 2004; Moll et al., 2012; Tamaki, 2017; Korhonen et al., 2019] to declarative approaches [Samer and Veith, 2009; Berg and J¨arvisalo, 2014; Lodha et al., 2016; Lodha et al., 2017; Fichte et al., 2018; Ganian et al., 2019], have been recently proposed for treewidth [Samer and Veith, 2009; Berg and J¨arvisalo, 2014; Tamaki, 2017; Korhonen et al., 2019], its generalizations to hypergraphs [Moll et al., 2012; Fichte et al., 2018; Korhonen et al., 2019], and related width notions [Lodha et al., 2016; Lodha et al., 2017; Ganian et al., 2019]. Among these approaches is the BT algorithm of Bouchitt´e and Todinca (2001) which operates dynamic programming over the so-called potential maximal cliques (PMCs). Originally proposed for treewidth, BT has recently been shown to be a practically efficient approach to treewidth as well as to various other NP-hard optimization problems related to graph triangulations [Tamaki, 2017; Dell et al., 2018; Korhonen et al., 2019], outperforming declarative approaches to determining treewidth, and constituting currently the most effective exact approach to determining generalized hypertreewidth [Korhonen et al., 2019].

The enumeration of PMCs, using a specialized enumeration algorithm [Bouchitt´e and Todinca, 2002], has been acknowledged as a bottleneck both in terms of worst-case analysis [Fomin et al., 2008] and scalability of BT in practice [Korhonen et al., 2019]. The question of whether PMCs can be enumerated with polynomial delay is currently open [Bodlaender et al., 2006]. Thus developing more effective approaches to enumerating PMCs is both a non-trivial challenge and a key to improving the scalability of BT in practice.

We propose the use declarative solvers for PMC enumeration as a substitute for the specialized PMC enumeration algorithms employed in current BT implementations. We develop both direct Boolean satisfiability (SAT) [Biere et al., 2009] and answer set programming (ASP) [Gelfond and Lifschitz, 1988; Niemel¨a, 1999] encodings as well as a SAT-based lazy approach for the task of PMC enumeration. We integrate these constraint-based enumeration approaches effectively to an iterative variant of BT which at the same time allows for avoiding the enumeration on all PMCs on graphs with low (tree or generalized hypertree)width. As a result, we obtain a novel iterative hybrid variant of BT, combining SAT solving and dynamic programming. Empirically, we show that integrating the proposed approaches into a recent BT implementation compares favorably with the use of specialized enumeration on the tasks of determining treewidth and generalized hypertreewidth. Furthermore, harnessing declarative solvers for enumerating PMCs opens up further opportunities for improving the efficiency of BT approaches to triangulationbased graph optimization problems through further improvements in SAT and ASP solvers.

2 Preliminaries

We consider undirected, simple graphs. We denote by V (G) and E(G) the set of vertices and edges, resp., of a given graph G. The neighbourhood N(v) of a vertex v ∈ V (G) consists of vertices u with {u, v} ∈ E(G). For a set S ⊂ V (G), N(S) = ∪v∈SN(v) \ S. A graph G is chordal if every cycle of length at least 4 has a chord, i.e., an edge joining two nonadjacent vertices in the cycle. A triangulation H of G is a chordal graph that contains G, specifically, a graph for which V (H) = V (G) and E(G) ⊂ E(H). A triangulation H of G is minimal if no proper subgraph of H is a triangulation of G. We denote the set of minimal triangulations of G by MT(G).

For a graph G, the graph G[S] induced by S ⊂ V (G) has V (G[S]) = S and E(G[S]) = E(G) ∩ {{u, v} | u ∈ S, v ∈ S}. We use the notation G \ S = G[V (G) \ S]. A set ω ⊂ V (G) is a clique (of G) if G[ω] is complete, and a maximal clique if no other clique ω′ satisfies ω ⊊ ω′ . We denote the set of maximal cliques of G by MC(G).

The width W(H) of a triangulation H ∈ MT(G) of G is maxω∈MC(H){|ω| - 1}, i.e., the size of the largest clique of H minus one. The treewidth TW(G) of a graph G is minH∈MT(G){W(H)}, i.e., the minimum width over all triangulations of G.

A set Ω ⊂ V (G) is a potential maximal clique (PMC) of G if there is a H ∈ MT(G) such that Ω ∈ MC(H). We denote the set of potential maximal cliques of G by Π(G), and the set of PMCs of size at most k by Πk(G). For a subset Πs ⊂ Π(G), we denote by MT(G,Πs) the minimal triangulations H of G for which MC(H) ⊂ Πs; and by TW(G,Πs) the minimum width of all triangulations in MT(G, Πs); TW(G, Πs) = ∞ if MT(G, Πs) = ∅. Note that MT(G,Π(G)) = MT(G), TW(G,Π(G)) = TW(G), and TW(G) = TW(G, Πk(G)) ≤ k-1 if TW(G, Πk(G)) < ∞.

Example 1 Consider the graph G in Figure 1 left: G is not chordal, witnessed by the cycle (s, u, b, t, v). One of its minimal triangulations H ∈ MT(G) is shown in Figure 1 right. The sets {a, s, v} and {s, v, u} are examples of maximal cliques of H and thus also examples of PMCs of G. As the largest clique of H has 3 vertices, we have H ∈ MT(G, Π3(G)) and W(H) = 2.

We denote the set of connected components of G by C(G). For a S ⊂ V (G), a component C ∈ C(G \ S) is full wrt S if N(C) = S, and S is a minimal separator of G if G \ S has at least two full components wrt S. We denote the set of minimal separators of G by ∆(G). Alternatively, a set S is an {u, v}-separator (or separates the vertices u and v) if u and v are not connected in G \ S and is further minimal if no S′ ⊊ S separates u and v. The set ∆(G) of minimal separators contains all sets S that are minimal separators of some pair of vertices u and v. Note that several different vertex-pairs can share a minimal separator, and that minimal separators of different vertex-pairs can be subsets of each other.

We will use the following characterization of PMCs.

Proposition 1 ([Bouchitt´e and Todinca, 2001]) A set K ⊂ V (G) is a PMC of a graph G if and only if (i) G \ K has no full components associated to K, and (ii) completing N(C) into a clique for each C ∈ C(G \ K) makes K a clique.

In particular, the conditions (i) and (ii) of Proposition 1 can be stated in terms of connectivity outside of specific sets of vertices. Given a set K ⊂ V (G) and t, u ∈ V (G), the vertices t and u are connected outside K if there is a path (t, v1, . . . , vn, u) in G such that vi ∈ V (G) \ K for all i = 1, . . . , n. Note that t and u can be connected outside of K even if they are in K. Thus Proposition 1 can be restated as follows for a basis of declarative encodings of PMCs.

Corollary 1 A set K ⊂ V (G) is a PMC of a graph G if and only if (i) for every vertex v ∈ V (G) \ K, there is a vertex u ∈ K such that v and u are not connected outside K and (ii) any two vertices v, u ∈ K are connected outside of K.

Example 2 Consider the graph G in Figure 1 (left) and let K = {s, v, u}. The graph G \ K has 2 connected components: C(G \ K) = {{a}, {t, b}}. Neither component is full wrt K, since N({t, b}) = {v, u} ̸= K ̸= {s, v} = N({a}). Thus K is not a minimal separator. One minimal {a, b}- separator within K is {s, v}. Completing N({t, b}) to a clique adds the edge {v, u}, making K a clique. Thus K satisfies the conditions of Proposition 1 and hence K ∈ Π(G). In terms of Corollary 1, a is not connected to u outside of K, and neither of t and b is connected to s outside of K. On the other hand, vertices in K are connected pairwise outside of K. Finally, no set containing only 2 vertices satisfies condition (i) of Corollary 1. Hence Π2(G) = ∅ and MT(G,Π2(G)) = ∅, and thus TW(G,Π2(G)) = ∞ and TW(G) = TW(G, Π3(G)) = 2.

Hypergraphs generalize graphs by allowing arbitrary subsets of vertices as (hyper)edges. We denote the set of vertices and edges of a hypergraph G by V (G) and E(G), resp. The primal graph PRIM(G) of G has V (PRIM(G)) = V (G) and E(PRIM(G)) = {{u, v} | ∃e ∈ E(G), {u, v} ⊂ e}. For a subset K ⊂ V (G), a set E ⊂ E(G) is an edge cover of K if K ⊂ ∪E. We denote the size of the smallest edge cover of K by COVG(K). For a hypergraph G, the width of a triangulation H ∈ MT(PRIM(G)) is W(H) = maxω∈MC(H){COVG(ω)}, and can be determined by computing the smallest edge covers of each clique ω ∈ MC(H). The generalized hypertreewidth of G is GHTW(G) = minH∈MT(PRIM(G)){W(H)} [Moll et al., 2012; Gottlob et al., 2002; Grohe and Marx, 2014]. Note that, as all edges of PRIM(G) are over two vertices, definitions related to (nonhyper) graphs are applicable via the primal graph. In particular, MT(PRIM(G),Πs) contains all of the triangulations H of PRIM(G) for which MC(H) ⊂ Πs and GHTW(G, Πs) = minH∈MT(PRIM(G),Πs){W(H)}.

3 The Bouchitt´e-Todinca Algorithm

Enumeration of potential maximal cliques forms the basis of the BT algorithm [Bouchitt´e and Todinca, 2001] which gives the best known exact algorithm for treewidth in terms of worst-case analysis [Fomin and Villanger, 2008] and yields a competitive approach to various triangulation-related graph optimization problems in practice [Tamaki, 2017; Dell et al., 2018; Korhonen et al., 2019]. In the following we overview BT focusing on treewidth; we refer to [Bouchitt´e and Todinca, 2001; Fomin et al., 2008] for further details. We will explain later in Section 5 how BT and the constraint-based enumeration approaches proposed in this work are adapted for generalized hypertreewidth.

The BT algorithm works in two phases: (i) Π(G) is computed, i.e., the potential maximal cliques of G are enumerated (ENUM-PMC); (ii) dynamic programming over Π(G) is used to determine the treewidth of G (BT-DP). Phase (ii) decomposes the computation of TW(G,Π(G)) into the computation of TW(G[S ∪ C],Π(G)) for minimal separators S ∈ ∆(G) and full components C ∈ C(G \ S) [Bouchitt´e and Todinca, 2001; Fomin et al., 2008]. The enumeration of PMCs (the first phase) in the original BT algorithm works by inductively defining Π(G) based on Π(G \ {v}) for some v ∈ V (G) and the minimal separators ∆(G) of the graph [Bouchitt´e and Todinca, 2002]. This requires enumeration of ∆(G), using the algorithm of Berry et al. (1999).

The dynamic programming phase of BT runs in time O(poly(n)·|Π(G)|), where n is the number of vertices. There are no known algorithms for enumerating Π(G) with similar time complexity [Bodlaender et al., 2006]. The enumeration phase of the original BT algorithm has time complexity Ω(poly(n) · |∆(G)|2 ). This suggests that the bottleneck of the overall efficiency of the BT algorithm is the enumeration of PMCs, which is also the case in practice [Korhonen et al., 2019]. This motivates developing alternative PMC enumeration approaches compatible with BT.

In terms of lower bounds for PMCs enumeration, a concrete example of a graph class with an exponential number of minimal separators is the "melon" graphs {MELONn}, which consist of n paths of length three between two distinct vertices a and b; see Fig. 2 for MELON4. In particular, it has been shown that |∆(MELONn)| = Ω(3n ) [Fomin et al., 2008]. Intuitively, the exponentiality is due to the fact that each way of selecting a single vertex from each of the paths forms a minimal separator. Thus any algorithm that enumerates all minimal separators, including the original BT algorithm, will have an unpractical running time for even small melon graphs such as MELON50. The declarative approaches to PMC enumeration proposed in this work solve MELON50 in a few seconds.

Iterative BT. For integrating declarative approaches to PMC enumeration into the BT framework, we employ an iterative BT variant that alternates between two phases. The critical observation here is that the dynamic programming of the second phase determines TW(G,Π′ ) for each subset Π′ ⊂ Π(G). Hence only PMCs of size bounded by the treewidth are required. In particular, if TW(G) ≤ k-1, then TW(G,Πk(G)) = TW(G). Thus BT-DP requires only the enumeration of Πk(G), i.e., the PMCs with at most k vertices, to determine the treewidth of G. This suggests an iterative variant of BT that alternates for different values of k between

(i) ENUM-PMC(G, k), consisting of computing Πk(G) and (ii) BT-DP(G,Πk(G)), which either returns ∞, indicating that TW(G) ≥ k, or returns the treewidth of G. The original BT algorithm fits this formalism by setting k = |V (G)| during the first iteration, enumerating all PMCs and terminating after the first call to BT-DP. Using declarative approaches for PMC enumeration, we will start with k = 1, and increment k after each iteration in order to enumerate the least number of PMCs needed for determining TW(G).

4 Constraint-Based Enumeration of PMCs

We propose three declarative approaches to enumerating PMCs using SAT and ASP solvers: direct SAT and ASP encodings of the size-k PMCs of a given graph G, which allow for using a SAT/ASP solver to enumerate PMCs, as well as a lazy SAT-based enumeration approach. Each approach can be integrated into the iterative BT algorithm as a substitute for the ENUM-PMC component.

The declarative encodings consist of two parts: (i) encoding of the two conditions of Corollary 1 in terms of connectivity outside of a PMC, and (ii) enforcing that only PMCs of size k are enumerated. Central to the approaches is how the connectivity constraints are encoded in part (i). The encoding of the connectivity constraints is further split to two directions: the "if"-direction, and the "only if"-direction. In particular, the declarative approaches we propose differ in terms of how the "only if"-direction is handled. The direct SAT approach encodes the existence of paths of length m inductively based the existence of paths of length m- 1. The direct ASP approach essentially differs from this by not having to explicate path-lengths. The lazy SAT approach uses minimal separators of G to prove that two vertices are not connected outside of a PMC. As the number of minimal separators of a graph can be large, the minimal separator constraints are added on demand instead of up front.

For discussing the encodings, let G be a graph with n vertices, and k the size of the PMCs to be enumerated. We assume w.l.o.g that G is connected. We assume familiarity with propositional logic, CNF representations, and answer set programming.

4.1 Direct SAT Encoding of PMCs

We use Boolean variables Pi for i = 1, . . . , n to indicate the inclusion of vertex vi in a PMC, and Cij for i, j = 1, . . . , n as auxiliary variables for encoding the connectivity constraints; for a model τ of the SAT encoding, we will have Ωτ = {vi | τ(Pi) = 1}, and τ(Cij) = 1 iff vertices vi and vj are connected outside of Ωτ .

Encoding Corollary 1. The Pi and Cij variables are bound together with the following constraints.

Constraint 1 encodes Condition (i) of Corollary 1, enforcing that for every vertex vi /∈ Ωτ there is a vertex vj ∈ Ωτ such that vi and vj are not connected outside of Ωτ . Constraint 2 encodes Condition (ii), enforcing that if vi and vj are in Ωτ , then they are connected outside of Ωτ .

"If"-direction of the connectivity constraints. What remains is the encoding of the "if" and "only-if" directions of the connectivity constraints over the Cij variables. The "if"- direction is naturally enforced as follows.

Here Constraint 3 enforces that if there is an edge between vertices vi and vj, then they are connected outside any PMC Ωτ . Constraint 4 ensures that connectivity information is propagated fully: if vi and vk are connected outside of Ωτ , vk /∈ Ωτ , and there is an edge between vk and vj, then also vi and vj are connected outside of Ωτ .

"Only if"-direction of the connectivity constraints. Note that Constraint 4 is always satisfied by setting τ (Cij) = 1 for all Cij , which is why also the "only if"-direction needs to be enforced explicitly in the direct SAT encoding. This is done using auxiliary variables C[t]ij for t = 1, . . . , n indicating the existence of a path of length at most t between vi and vj that does not containing vertices in Ωτ . These variables are defined by the following constraints.

Constraints 5 and 6 define the base conditions for being (not) connected. Constraint 7 enforces that if vertices without a direct edge between are connected, there must be a shorter path that supports this connectivity. Constraint 8 binds the path-length variables and the connectivity variables Cij . The redundant constraint Cij [t] → Cij [t + 1] for all t = 1..n - 1 and i, j = 1..n is included for additional propagation.

Restricting the size of enumerated PMCs. The restriction to size-k PMCs is enforced through the cardinality constraint

For encoding Eq. 9 in CNF, here we use the Totalizer encoding [Bailleux and Boufkhad, 2003] which is both compact and can be used incrementally.

Enumeration of models of the direct SAT encoding, consisting of constraints 1-9, corresponding to the set of sizek PMCs of G, is done in a standard way by incrementally calling a SAT solver, and adding the clause ∨τ(Pi)=1 ¬Pi ∨ ∨τ(Pi)=0 Pi that blocks out each found model τ from further consideration until the SAT solver reports unsatisfiability.

4.2 Direct ASP Encoding of PMCs

As an alternative to the direct SAT encoding we propose a direct ASP encoding. The potential benefits of employing ASP come in terms of the answer set semantics [Gelfond and Lifschitz, 1988], which circumvents-in contrast to the SAT encoding-the need to explicate the lengths of paths in enforcing that the existence of a path must be supported by the existence edges forming the path. The answer set semantics requires natively that all true atoms must have an external support, and the semantics is enforced internally within the ASP solver during SAT-solver like complete search. Furthermore, ASP natively supports cardinality constraints, and ASP solvers offer built-in support for model enumeration.

The ASP encoding analogous to the direct SAT encoding is as follows. The predicate vertex/1 represents the N = n vertices (r1), and pmc/1 the inclusion of vertices in a PMC; each vertex may be included in a PMC through the choice rule (r2), which also enforces the size of the PMC to be k using built-in support for cardinality constraints.

The input predicate edge/2 represents the input graph, and c/2 represents connectivity in the graph (in analogy with the direct SAT encoding) with the following rules r3-r6.

Finally, condition (i) of Corollary 1 is enforced through the integrity constraint

where

4.3 SAT-based Lazy Approach

As a third alternative declarative approach to handling the connectivity constraints, we propose a lazy SAT approach. The approach is based on enforcing the "only-if"-direction of connectivity constraints through the minimal separators of G. Specifically, vi and vj are only connected outside of Ωτ if Ωτ does not contain a minimal vi, vj separator.

For a fixed minimal separator S ∈ ∆(G), we use an auxiliary variable MS to indicate that S is a subset of Ωτ . If we were given the set all minimal separators, the above condition can then be enforced by adding the following constraints for each S ∈ ∆(G).

Constraint 10 "activates" the minimal separator if it is a subset of Ωτ , and Constraint 11 enforces that vi and vj are not connected outside of Ωτ if a minimal separator separating them is activated. In the following we denote by SEP(S) these constraints for a minimal separator S.

As the number of minimal separators of a graph can be exponential in the number of vertices of G (recall Sect. 3), we do not introduce these constraints for all minimal separators up front. Instead, we propose a lazy approach which iteratively adds these constraints whenever the condition to be enforced is violated by a solution reported by a SAT solver, in which case we can easily obtain a minimal separator for ruling out the unwanted candidate solution from further consideration. The initial number of variables and clauses is O(n2 ) and O(nm) in the lazy approach, compared to O(n3 ) and O(n2m) in the direct approach.

Algorithm 1 details the lazy SAT-based approach to PMC enumeration. A working formula F is maintained, initialized as the conjunction of Constraints 1-4 and 9 (i.e., not including the "only if' encoding of the connectivity constraints). When a model τ of the working formula is obtained via SAT-SOLVE, we check if Ωτ is an actual PMC of G. This check is straightforward to implement based Corollary 1 and has negligible runtime also in practice. In the positive case, Ωτ is added to Πk and blocked from being rediscovered by adding a blocking clause to F . Otherwise, constraint SEP(Sτ ) is added to F for a minimal separator Sτ to rule out τ as a model for F. Specifically, since F contains constraints defining that Ωτ is a PMC except the "only if"-direction of connectivity constraints, the fact that Ωτ is not a PMC implies that there is a pair vi and vj such that τ(Cij) = 1 even though vi and vj are not connected outside of Ωτ . The function VIOLATING-PAIR(G, τ) returns such a pair of vertices. Next a minimal {vi, vj}-separator Sτ ⊂ Ωτ is computed by starting from Sτ = Ωτ \ {vi, vj} and iteratively removing all vertices u ∈ Sτ for which Sτ \ {u} still separates vi, vj, i.e. SEPARATES(Sτ \ {u},G, vi, vj) is true (the existence of such Sτ follows from vi and vj not being connected outside of Ωτ ). Finally, τ is ruled out as a model of F by adding the constraints SEP(Sτ ). (In addition to τ, the constraints SEP(Sτ ) may also rule out other models of F that do not correspond to actual PMCs of G.) The function SEPARATES is easy to implement with standard graph traversal algorithms. Algorithm 1 iterates until F becomes unsatisfiable, at which point all PMCs of G of size k have been found.

5 Adaptations to Generalized Hypertreewidth

While we have so far described the BT framework and the declarative approaches to PMC enumeration in the context

Algorithm 1 SAT-based lazy enumeration of size-k PMCs

of treewidth, adapting them to determining generalized hypertreewidth of a given hypergraph G requires only minor changes [Moll et al., 2012]; an implementation of BT for GHTW is already available [Korhonen et al., 2019]. In detail, the iterative BT algorithm is adapted for computing GHTW(G) essentially by making the set of PMCs to be enumerated during iteration k to be the PMCs Ω of PRIM(G) for which COVG(Ω) ≤ k. The edge covers are computed with a branch-and-bound set cover algorithm. In the declarative approaches, this change corresponds to altering the size-k constraint to restrict COVG(Ωτ ) instead of restricting |Ωτ |. Concretely, in the SAT-based approaches this is done by replacing Constraint 9 by the constraints

where the auxiliary variables Oe for each hyperedge e ∈ E(G) indicates inclusion of the edge in the edge cover of a PMC. Constraint 12 enforces that a chosen set of edges forms an edge cover, i.e., that the edges cover all vi ∈ Ωτ . The cardinality constraint 13 limits the size of the smallest edge cover to COVG(Ω) ≤ k; in our implementation we again use the Totalizer encoding.

As for the ASP encoding, rule r2 is replaced by

hyper(X) :- X = 1..N, hyperedges(N). { selected(X) : hyper(X) } = K :- size(K). { pmc(X) : vertex(X) }. covered(X) :- inhyper(X,Y), selected(Y).

to select the hyper edges to the edge cover (selected/1) and to determine the covered vertices (covered/1) via the input predicate inhyper/2 representing the end-points of hyperedges. Further, an actual edge cover is enforced with the integrity constraint :- not covered(X), pmc(X).

6 Experiments

We integrated the three declarative approaches to PMC enumeration to the recent BT implementation Triangulator [Korhonen et al., 2019] that supports both treewidth and generalized hypertreewidth. The implementation is available at https://github.com/Laakeri/pmcenum-ijcai. Triangulator implements PMC enumeration with the original algorithm [Bouchitt´e and Todinca, 2002] (recall Sect. 3). This allows us to evaluate the effectiveness of the hybrid approaches resulting from replacing the PMC enumeration of Triangulator with the declarative approaches. We made no modifications to the dynamic programming and preprocessing [Bodlaender and Koster, 2006] implemented in Triangulator.

In the experiments, we used Clingo 5.3.0 [Gebser et al., 2016] as the de-facto ASP solver, and-based on preliminary experiments of several state-of-the-art SAT solvers-Glucose 4.1 as the SAT solver [Audemard and Simon, 2018] through its incremental API. For ASP, we used Clingo's built-in support for enumerating all answer sets. All experiments were run single-threaded on computing nodes with 2.4-GHz Intel Xeon E5-2680-v4 processors. A per-instance 2-hour time limit and 32-GB memory limit was imposed.

For empirical corroboration for the claim that the declarative approach circumvents worst cases of the original PMC enumeration within BT, we generated melon graphs (recall Sect. 3) for increasing n. (External preprocessing implemented in Triangulator was disabled for this experiment, as it would determine TW(MELONn) = 2 for all n ≥ 2 without BT. Constructions with non-trivial treewidth exhibiting similar behavior may exist.) For treewidth, the original PMC enumeration did not scale beyond n = 10 within 2 h, while our lazy SAT-based enumeration allows for determining treewidth for n = 200 within 7.5 minutes; see Table 1

For further experiments, we used all of the benchmarks instances from [Korhonen et al., 2019], consisting of 589 graphs for treewidth and 265 for generalized hypertreewidth gathered from various different sources (including PACE 2016 and 2017 instances). The results are shown in Figure 3 (left) for treewidth and (middle) for generalized hypertreewidth, as the number of instances solved for each of the approaches (x-axis) under different time limits (y-axis). The direct SAT enumeration is not competitive with the other approaches. In contrast, the lazy SAT approach yields best performance, solving 343 treewidth instances compared to 308 solved using Triangulator's original PMC enumeration implementation, also yielding slight improvement for GHTW. ASP enumeration also improves on Triangulator for treewidth, although with some overhead compared to lazy SAT. The largest graph for which treewidth could be determined by the direct SAT, ASP, and lazy SAT methods has 125, 559, and 559 nodes, respectively. For treewidth instances solved with lazy SAT approach, the maximum and median numbers of SAT solver iterations were 157555 and 655. Figure 3 (right) further motivates the lazy SAT approach with a per-instance comparison of the number of minimal separators enumerated by it and the total number of minimal separators. Furthermore, the lazy (direct) approach could decide "treewidth ≤ k?" for k = 3, 5, 10, 20 on 570 (475), 557 (444), 482 (390), 426 (350) instances, respectively. Overall, the results show that declarative PMC enumeration is a promising alternative in the context of BT. In comparison to other state-of-the-art approaches, the PIDDT [Tamaki, 2017] and Jdrasil [Bannach et al., 2017] approaches to treewidth solved 467 and 457 instances, respectively, and the fraSMT [Fichte et al., 2018] approach to GHTW solved 25 instances.

7 Conclusions

We proposed the use of declarative solvers for PMC enumeration within the BT approach to treewidth and generalized hypertreewidth, developing direct SAT and ASP encodings, and as a lazy SAT-based approach for PMC enumeration that circumvents particular exponential behavior of the original PMC enumeration approach for BT. Empirically, declarative PMC enumeration is a promising alternative within BT, improving its performance on treewidth and generalized hypertreewidth.

Acknowledgements

This work was financially supported by Academy of Finland grants 276412 and 312662.