The Impact of Treewidth on ASP Grounding and Solving

1 Introduction

Answer set programming (ASP) [Marek and Truszczy´nski, 1999; Brewka et al., 2011; Gebser et al., 2012a] is a wellestablished logic programming paradigm based on the stable model semantics. Its main benefit is an intuitive, declarative language, and the fact that, generally, each answer set of a given logic program describes a valid solution of the original problem. Solving ASP programs is usually a two-step process. First, a (usually fixed) encoding for a given problem is written in the language of non-ground ASP. This encoding, together with a set of input facts representing the actual problem instance, gets passed to a grounder which transforms it into an equivalent propositional ASP program. In the second step, this ground program is then evaluated by a solver. Such ASP solvers are now readily available (e.g., [Gebser et al., 2012b; Alviano et al., 2015; Elkabani et al., 2005; Leone et al., 2006]) and have made huge strides in efficiency.

This leads to the following interesting practical question: What is the relationship of solver efficiency and different parameters of the ground input program, and how is the solving time influenced by these parameters? On the theoretical side, computational complexity investigations were carried out for the classical parameter of input size [Eiter and Gottlob, 1995;

Truszczy´nski, 2011; Dantsin et al., 2001], while several structural parameters were studied in the field of parameterized complexity [Gottlob et al., 2010; Pichler et al., 2014; Fichte and Szeider, 2015]. This has also led to specialized implementations that try to explicitly exploit these parameters [Jakl et al., 2009; Fichte et al., 2017]. While these theoretical investigations provide us with valuable insight into the problem of ASP solving, it is not obvious what conclusions can be drawn for the actual practical solving performance of today's top-of-the-line ASP solvers. It would be interesting to see how current CDCL-based solvers are influenced, in practice, by variations in such structural parameters and whether guidelines for ASP modeling can be derived from such interactions. One of the few results in this direction is the discovery of a strong correlation between the rule-to-atom ratio of a ground ASP program and the solving time [Zhao and Lin, 2003], a property that carries over from similar studies for SAT [Selman et al., 1996]. A more recent study on phase transitions in ASP also deals with this topic [Wen et al., 2016]. Beside these results, however, the practical impact of structural parameters on solving time has not, in the authors' opinion, received adequate attention in the literature.

In this paper we focus on the parameter of treewidth, a measure of how closely a ground ASP program structurally resembles a tree. Our goal is to study how the performance of modern ASP solvers is influenced by the treewidth of the given ground input program and to investigate the consequences of this relationship. To this end, our first main contribution is to carry out an extensive experimental evaluation of two top-of-the-line ASP solver implementations and investigate how the solving performance behaves when the solvers are presented with hard instances of uniform size and construction, but variable treewidth, using a carefully crafted ASP problem encoding and adequately generated, tree-like instances. Our experiments show that the solving time for programs of the same size and construction indeed increases drastically with the treewidth. This is an interesting result, which shows that similar results for SAT solvers and resolution-width [Atserias et al., 2011] do indeed carry over to the more complex world of ASP. Our observations suggest that, when encoding problems in (non-ground) ASP, it is not only important that the resulting ground program is small, but also that its treewidth is kept as small as possible, given a set of input facts.

Example 1. Reachability can be modeled in different ways using ASP. One way would be to model the transitive closure of a graph as follows (where e is the predicate representing graph edges and r the predicate to mark reachable vertices):

t(X,Y) :- e(X,Y). t(X,Z) :- t(X,Y), e(Y,Z). r(Y) :- t(X,Y), start(X).

However, when used as a sub-program that the grounder has to instantiate, such an encoding causes any two (connected) vertices in the input graph to appear together in a rule after grounding (in place of the variables X and Z in the second rule). This then causes the graph representation of the ground program to contain a clique whose size equals the number of vertices of the original input graph, resulting in a high treewidth. Conventional wisdom in ASP would recommend the following encoding:

r(X) :- start(X). r(Y) :- e(X,Y), r(X).

Here, not only is the grounding smaller, but also the treewidth decreases dramatically. In fact, it now solely depends on the treewidth (and not the size) of the input graph.

This example illustrates that the way a problem is encoded can influence the treewidth of the ground program considerably. Due to the grounding step, however, it is not obvious at the time of writing a non-ground ASP encoding how to achieve a low-treewidth grounding and the benefits that come with it. This is as opposed to, for example, SAT formulas that can be generated directly while keeping treewidth in mind. The second main contribution of this paper addresses this issue and allows us to leverage the treewidth-sensitivity of ASP solvers: We define the class of connection-guarded programs, which guarantees that the treewidth of a program after grounding does not increase arbitrarily but only depends on the treewidth (and degree) of the input facts. We also show that programs in our class are, at the same time, expressive enough to encode relevant problems from the second level of the polynomial hierarchy. In our proofs, we use the notion of MSO transductions [Courcelle and Engelfriet, 2012] to formally represent the grounding process and investigate its influence on the treewidth. To our knowledge, this is the first time that this technique has been used in the context of ASP.

The remainder of the paper is structured as follows. In Section 2, we give relevant definitions for ASP, treewidth, and MSO transductions. Section 3 deals with our first main contribution, the experimental evaluation of solver performance with respect to treewidth, and shows that there is a significant correlation. Section 4 presents our second main contribution, namely, proposing the class of connection-guarded ASP programs that aims to preserve the treewidth of the given instance after grounding. We also address implications of our results for ASP solving and modeling. Finally, we conclude the paper with a discussion in Section 5.

2 Preliminaries

Answer Set Programming (ASP). ASP is a declarative problem modeling and solving framework with a complex language that we only briefly introduce here. For a full, formal introduction, we refer to other sources [Brewka et al., 2011; Gebser et al., 2012b]. A non-ground disjunctive logic program Π consists of a set of rules of the form r : h1 ∨ · · · ∨ hk ← p1, . . . , pn, ¬n1, . . . , ¬nm, where hi, pi and ni are atoms, called head (H(r)), positive and negative body atoms (B+(r) and B-(r)), respectively. An atom a is of the form s(X, c) and consists of a predicate name s, a sequence of variables X, and a sequence of constants c, where |X|+|c| is the arity of s. We denote variables by capital letters, and constants and predicates by lower-case words. We assume rules to be safe, that is, all variables appear in the positive body. A rule is ground if it contains no variables. A fact is a ground rule with an empty body and just one head atom. A predicate is extensional in Π if it appears only in rule bodies of Π. We also call an atom extensional if its predicate is extensional.

A non-ground rule can be seen as an abbreviation for all possible instantiations of the variables with domain constants. In ASP, this instantiation is explicitly performed by a grounder that transforms a (non-ground) program into an equivalent set of ground rules. Grounders implement many advanced techniques to generate ground programs that are as small as possible. Since these techniques are sometimes quite involved and hinder theoretical investigation, for the purposes of this paper we define an idealized grounder as follows:

Definition 2. Let Π be a non-ground ASP program, let Π+ denote the positive program obtained from Π by removing all negated atoms and replacing disjunctions with conjunctions (i.e., splitting disjunctive into normal rules), and let M + be the unique minimal model of Π+. For every rule r ∈ Π and substitution s from variables to constants, the grounding of Π, denoted gr(Π), contains s(r) iff s(B+(r)) ⊆M +.

Ground ASP programs are intended to be interpreted according to the stable model semantics [Gelfond and Lifschitz, 1988]. Given a non-ground program Π (called encoding) together with a set of facts A (called instance) as input, the main reasoning task considered in this paper is to decide whether the corresponding grounding gr(Π ∪ A) has a stable model (or answer set). For fixed programs Π, this problem is ΣP 2 - complete [Eiter and Gottlob, 1995].

In ASP code listings, we represent the ← symbol in rules by :-. In Section 3, we will make use of advanced ASP constructs like inequality and aggregate functions, as described in the ASP language specification [Calimeri et al., 2015].

Graphs, Tree Decompositions, and Treewidth. We assume all graphs to be undirected, simple, and ordered, which means that there is an arbitrary but fixed total order over the vertices of the graph. For a graph G, V (G) denotes the set of vertices and E(G) the set of edges. A graph H is a minor of a graph G if H can be obtained from G by deleting edges or vertices, or by contracting edges. The Cartesian product G□H of graphs G and H has vertices V (G□H) = V (G) × V (H) and an edge between vertices 〈u, u′ 〉 and 〈v, v′ 〉 iff u = v and (u′ , v′ ) ∈ E(H), or u′ = v′ and (u, v) ∈ E(G). A (square) grid of size n is the Cartesian product of two paths of length n. The line graph GL of a graph G has V (GL) = E(G), and (e1, e2) ∈ E(GL) iff edges e1 and e2 share a vertex in G.

Let G be a graph, T a rooted tree, and χ a labeling function that maps every node t of T to a subset of V (G) called the bag of t. The pair (T, χ) is a tree decomposition of G if the following holds: (i) for each v ∈ V (G), there exists a t ∈ T , such that v ∈ χ(t); (ii) for each {v, w} ∈ E(G), there exists a t ∈ T , such that {v, w} ⊆ χ(t); and (iii) for each r, s, t ∈ T , such that s lies on the path from r to t, we have χ(r)∩χ(t) ⊆ χ(s). The width of a tree decomposition is defined as the cardinality of its largest bag minus one. The treewidth of a graph G, denoted by tw(G), is the minimum width over all tree decompositions of G. For a minor H of a graph G it holds that tw(G) ⩾ tw(H). Trees have treewidth 1. Grids of size n, the complete graph Kn with n nodes, and the complete bipartite graph Kn,n all have treewidth n.

Graph Representations and Treewidth of ASP Programs. The primal graph of a ground ASP program Π is a graph whose vertices are the atoms in Π and there is an edge (a, b) if atoms a and b appear together in a rule in Π. The incidence graph of Π is a bipartite graph whose vertices are the atoms and rules in Π and there is an edge between a rule r and an atom a if a appears in r. The primal treewidth or incidence treewidth of an ASP program Π is the treewidth of its primal or incidence graph, respectively. By treewidth we generally refer to the primal treewidth. For ASP programs of bounded treewidth, the answer set existence problem can be solved in linear time [Gottlob et al., 2010]. The instance graph of an instance A is a graph whose vertices are the constants in A, and which has an edge (a, b) if constants a and b appear together in a fact from A. The treewidth or degree of an instance A is the treewidth or degree of its instance graph, respectively.

MSOTransductions. Monadic second-order (MSO) logic is an extension of first-order logic by quantification over sets. We omit a formal definition as all formulas in this work will be first-order. MSO can be used to specify MSO transductions [Courcelle and Engelfriet, 2012], which are mappings from graphs to graphs. The idea is that an MSO transduction formalizes how a graph G can be transformed into a graph G′ by the following operations: (1) copying G a fixed number of times, (2) filtering vertices that satisfy an MSO-definable property, (3) defining the edges of G′ in terms of the edges of G via MSO formulas. This is achieved by specifying MSO formulas (δi)i∈I, (θi,j)(i,j)∈I×I, where I is an arbitrary finite set, each δi has one free variable, each θi,j has two free variables, and the signature of the formulas consists of the binary predicates edge and succ. For every graph G, we write Str(G) to denote the relational structure with domain V (G), that interprets edge by E(G) and succ by the successor relation according to the vertex ordering. We call the graphs for which τ is defined input graphs, and the image of τ the output graphs. The δi formulas specify which vertices exist in τ(G). For each v ∈ V (G), there can be up to |I| copies of v in τ(G): There is a copy vi in τ(G) iff Str(G) ⊨ δi(v). Finally, the edges in τ(G) are specified using the θi,j formulas. For each pair of vertices (v, w) ∈ V (G) × V (G), there is an edge (vi,wj) ∈ E(τ(G)) iff Str(G) ⊨ θi,j(v,w) in addition to Str(G) ⊨ δi(v) and Str(G) ⊨ δj(w).

MSO transductions allow us to prove statements about how a graph transformation affects the treewidth of a graph:

Proposition 3 ([Courcelle and Engelfriet, 2012, Corol-

1 a s s i gn (X,Y, 1 ) | a s s i gn (X,Y, 0 ) :- edge (X,Y) . 2 sum(V, S\2) :- ve r t ex (V) , S = #sum{ A,W : a s s i gn (W,V,A) ; A,W : a s s i gn (V,W,A) } . 3 :- sum(V, S) , c apa c i t y (V,C) , S != C.

Listing 1: Finding valid assignments in capacitated graphs.

lary 1.53]). Let τ be a fixed MSO transduction. For every input graph G, the treewidth of τ(G) depends only on the treewidth of G and the degree of τ (G). 1

3 Impact of Treewidth on ASP Solvers

In this section we will demonstrate, by experimental evaluation, that state-of-the-art ASP solvers have an inherent sensitivity to treewidth in practice, that is, they perform faster on ground programs of small treewidth. To show this claim, a carefully designed experiment is needed in order to actually reveal the influence of the treewidth (and not some other parameter) on the solving time. Ground programs used for testing therefore need to (1) have the same number of answer sets, (2) have a uniform structure, (3) have constant size, and (4) vary in treewidth. To this end, we consider the problem of deciding whether a capacitated graph has a valid assignment:

Definition 4. A capacitated graph is a pair (G, c), where G is an undirected graph and c a function mapping each vertex to 0 or 1. An assignment is a function mapping each edge to 0 or 1, and we call it valid if for each v ∈ V (G) the sum modulo 2 of the values assigned to incident edges equals c(v).

This problem was used by Urquhart to construct hard SAT formulas [Urquhart, 1987] using the method of Tseitin [1983]. Listing 1 shows an ASP encoding for this problem. Line 1 assigns either 0 or 1 to each edge. Line 2 calculates for each vertex the sum modulo 2 of the values assigned to incident edges. Finally, Line 3 eliminates all assignments where for some vertex the sum and capacity do not agree.

Input Instances. In order to satisfy condition (1), we will only construct unsatisfiable instances. It is known that a connected capacitated graph has a valid assignment iff the sum of all vertex capacities is even [Urquhart, 1987]. To construct unsatisfiable instances, we thus generate graphs where all vertices except for one have capacity 0.

To satisfy condition (2), we choose Listing 1 as our fixed problem encoding and construct instances in the following way: We generate so-called grid-tree instances, which are random binary trees of grids as illustrated in Figure 1, according to two parameters: treesize (the number of grids in the tree) and gridsize (the size of each grid).

Given a grid-tree instance, we can find other grid-tree instances that lead to the same grounding size by increasing the treesize while decreasing the gridsize (or vice versa). Thus, in order to satisfy condition (3), we first fix a grounding size (in terms of the number of atoms), and then find combinations of treesize and gridsize to achieve this grounding size.

Finally, we establish condition (4). For a graph G consisting only of a disjoint union of grids G1, . . . ,Gk plus

1 In fact, our MSO transductions preserve bounded cliquewidth; however, bounded cliquewidth and bounded treewidth coincide on graphs of bounded degree [Courcelle and Olariu, 2000].

1 a t l e a s t ( v7 , 1 ) :- 1 { a s s i gn ( v3 , v7 , 1 ) , a s s i gn ( v6 , v7 , 1 ) , a s s i gn ( v7 , v8 , 1 ) , a s s i gn ( v7 , v11 , 1 ) }. 2 a t l e a s t ( v7 , 2 ) :- 2 { a s s i gn ( v3 , v7 , 1 ) , a s s i gn ( v6 , v7 , 1 ) , a s s i gn ( v7 , v8 , 1 ) , a s s i gn ( v7 , v11 , 1 ) }. 3 a t l e a s t ( v7 , 3 ) :- 3 { a s s i gn ( v3 , v7 , 1 ) , a s s i gn ( v6 , v7 , 1 ) , a s s i gn ( v7 , v8 , 1 ) , a s s i gn ( v7 , v11 , 1 ) }. 4 a t l e a s t ( v7 , 4 ) :- 4 { a s s i gn ( v3 , v7 , 1 ) , a s s i gn ( v6 , v7 , 1 ) , a s s i gn ( v7 , v8 , 1 ) , a s s i gn ( v7 , v11 , 1 ) }. 5 sum( v7 , 0 ) :- not a t l e a s t ( v7 , 1 ) . 6 sum( v7 , 0 ) :- a t l e a s t ( v7 , 2 ) , not a t l e a s t ( v7 , 3 ) . 7 sum( v7 , 0 ) :- a t l e a s t ( v7 , 4 ) . 8 sum( v7 , 1 ) :- a t l e a s t ( v7 , 1 ) , not a t l e a s t ( v7 , 2 ) . 9 sum( v7 , 1 ) :- a t l e a s t ( v7 , 3 ) , not a t l e a s t ( v7 , 4 ) .

some edges that do not create any new cycles, it holds that tw(G) ≤ max{tw(G1), . . . , tw(Gk), 1}, since we can easily obtain an appropriate tree decomposition of G from those of G1, . . . ,Gk. Hence the treewidth of a grid-tree instance A only depends on the gridsize. We now need to show that the treewidth of A determines the treewidth of the grounding.

Proposition 5. Given program Π from Listing 1 and a gridtree instance A, the primal treewidth and incidence treewidth of gr(Π ∪ A) are both linear in the treewidth of A.

Assume, for simplicity, that A is just a single grid of size 4. We call the nodes in the first row of the grid v1, . . . , v4, the nodes in the second row v5, . . . , v8, and so on. In order to show the above proposition, first note that Line 1 and Line 3 in Listing 1 cannot cause any cycles in the primal graph of gr(Π∪A). Now consider Listing 2, which shows the grounding for Line 2 of Listing 1 for vertex v7 of A. Figure 2b shows the primal graph of this partial grounding (where M,N represents the atom assign(vM,vN,1)). Clearly, the rule bodies of the first four lines in Listing 2 cause the central clique between vertices 3, 7; 7, 8; 7, 11; and 6, 7 to appear. Note that this forms a clique precisely between the incident edges of vertex v7. Now, take only the rule bodies of Lines 1 to 4 in Listing 2, and the same also from the analogous groundings of every other vertex in A. The corresponding partial primal graph is shown in Figure 2a. In fact, this is precisely the line graph of the grid in A. The full primal graph of gr(Π ∪ A) can now be obtained by replacing every clique in Figure 2a (which represents some vertex v from A) with a gadget analogous to the one in Figure 2b, but for vertex v. Note that this gadget has constant size (and, therefore, treewidth). We thus have that the treewidth of gr(Π ∪ A) is asymptotically

(a) The line graph of a grid

of size 4.

sum(v7,0)

(b) Primal graph of Listing 2.

Figure 3: Clasp and WASP running time.

upper-bounded by the treewidth of the line graph of A. It is not difficult to extend this argument to the case where A is a grid-tree instead of a single grid.

To complete our line of argument, note that it is known that the treewidth of the line graph is linear in the treewidth of the original graph if the maximum degree of the latter is bounded by a constant, as is the case for grids [C˘alinescu et al., 2003]. Since the incidence treewidth is upper-bounded by the primal treewidth [Szeider, 2003], this establishes condition (4).

Benchmark Setting. In our tests we used two batches of instances constructed as presented before, each batch for a different grounding size. For the first batch the number of atoms in the grounding is approximately 10350 and for the second 16700, ± 100. In each batch there were 20 instances for each treewidth between 2 and 10. 2 Grounding was done using the grounder gringo 4.5.4 [Gebser et al., 2011]. We then measured the running time of the ASP solvers clasp 3.1.4 [Gebser et al., 2011] and WASP 2.0 [Alviano et al., 2015].

Results and Discussion. Figure 3 shows how the average solving time of clasp and WASP changes with the treewidth for our two batches of instances. Recall that the treewidth of the corresponding ground program is linear in the input treewidth by Proposition 5. Since the running time in Figure 3 is denoted on a logarithmic scale, we can thus see that the running time increases exponentially with the treewidth while the grounding size remains the same. Moreover, the running time for small programs with high treewidth can be substantially longer than for large programs with small treewidth.

2 Full archive: http://dbai.tuwien.ac.at/proj/ decodyn/ijcai17-benchmarks.zip

We thus conclude that the treewidth of the grounding has a major impact on the running time of current ASP solvers and that, for good solving performance, it is important to keep the treewidth of ground programs as low as possible.

4 A Treewidth-Preserving Class of Programs

As we showed in the previous section, treewidth has a strong influence on the solving time of ASP solvers. In order to exploit this relationship in practice, whenever possible, an ASP encoding Π should be written in such a way that, for a given instance A, it does not arbitrarily increase the treewidth of gr(Π ∪A) compared to the treewidth of A. To this end, we introduce the class of connection-guarded ASP programs.

Definition 6. Given an ASP programΠ, the extensional join graph of a rule r in Π is the graph whose vertices are the variables in r and which has an edge between two variables if these variables occur together in a positive extensional body atom in r. We call Π connection-guarded if the extensional join graph of each rule in Π is connected.

The proposition below follows directly from this definition.

Proposition 7. Let Π be a connection-guarded program, r a rule in Π, and A an instance. For any two constants a and b in any ground rule r′ ∈ gr(Π ∪ A) obtained from r during grounding, the distance between a and b in the instance graph of A is at most the number of variables in r.

The intention of connection-guarded programs is to guarantee that the treewidth of the grounding remains bounded, provided that the treewidth and degree of the input instance is also bounded. The following theorem is the main result of this section and states this formally.

Theorem 8. Let Π be a fixed connection-guarded program, and A an instance. If A has bounded treewidth and degree, then both the primal graph and the incidence graph of gr(Π∪ A) also have bounded treewidth and degree.

Before we prove this, we define several auxiliary notions. Our proof relies on MSO transductions and in this context we treat instances as relational structures. We build a transduction for program Π that transforms the instance graph of an ASP instance A into the incidence graph of gr(Π ∪ A). For this, we use the following auxiliary formulas.

Firstly, for any positive integer i, the following formula expresses that a vertex y is the i-th neighbor of a vertex x. (Recall that we assume ordered graphs. The transitive closure of the succ relation is MSO-definable and we denote it by <.)

A path identifier π = 〈i1, . . . , ik〉 of length k is a k-tuple of positive integers. It is called bounded by some integer d, if each integer in the tuple is bounded by d. We define the formula pathπ(x, y) to express that vertex y is reachable from vertex x via a sequence of vertices v0, v1, . . . , vk such that v0 = x, vk = y, and vj is the ij-th neighbor of vj-1, for 1 ⩽ j ⩽ k. We write ε to denote the empty tuple.

We define the total order ≺d over path identifiers bounded by d such that π ≺d π′ if π is lexicographically smaller than π′ . The formula fpdπ (x, y), defined below, represents that π is (according to ≺d) the first path identifier bounded by d that identifies a path to vertex y when starting from vertex x.

For all nonnegative integers k, ℓ, d and path identifiers π1, . . . , πk each of length at most ℓ and bounded by d, we define the formula uidℓ,d π1,...,πk (x, y1, . . . , yk). It represents that x is the smallest vertex connected to all the vertices y1, . . . , yk via paths of length at most ℓ, and that each πi is the first path identifier that identifies a path to yi when starting from x. For ease of notation, let reachℓ(x, y) be the formula representing that vertex y is reachable from vertex x in at most ℓ steps along the edge predicate.

Note that for the empty tuple ε, the formula uidℓ,d ε (x) ≡ ¬∃z (z < x) holds only for the smallest vertex of the graph.

Having the above definitions at our disposal, we are now ready to proceed to the proof of Theorem 8.

Proof of Theorem 8. We will, for the moment, assume that Π is constant-free; we will show later how to handle the general case. Let ℓ be the maximum number of variables in any rule of Π. Furthermore, assume that A has bounded treewidth and degree, and let d denote the degree of A.

From Π and d, we will construct a fixed MSO transduction τΠ,d that transforms the instance graph of A into the incidence graph of gr(Π ∪ A) with bounded degree. By Proposition 3, this is sufficient to show our claim. To this end, let τΠ,d = (∆a ⊎ ∆r,Θ), where ∆a contains formulas generating the atom vertices of the incidence graph, ∆r contains formulas generating the rule vertices, and Θ contains formulas generating the edges between them.

The Set ∆a. For each predicate p of arity k occurring in Π and for each k-tuple of path identifiers 〈π1, . . . , πk〉 each of length at most ℓ and bounded by d, let ∆a contain the formula

The Set ∆r. For each rule r ∈ Π with k variables and for each k-tuple of path identifiers 〈π1, . . . , πk〉 each of length at most ℓ and bounded by d, let ∆r contain the formula

The Set Θ. Since we need to link atoms and rules, we have to check compatibility between an instantiation of an atom and the instantiation of a rule. To this end, let p be a predicate of arity k, let r be a rule with variables Y1, . . . , Yn, and let Ap,r be the set of all those tuples 〈i1, . . . , ik〉 of integers where the atom p(Yi1 , . . . , Yik ) occurs in r. We define the formula

This auxiliary formula is true if the variables xi (representing the instantiation of an atom with k-ary predicate p) agree with the variables yj (representing the instantiation of a rule r with n variables) in such a way that the p-atom would appear in the instantiation of rule r.

We are now ready to give the formulas in Θ. For each predicate p of arity k occurring in Π and each k-tuple of path identifiers 〈π1, . . . , πk〉 each of length at most ℓ and bounded by d, as well as for each rule r ∈ Π with n variables and each n-tuple of path identifiers 〈ρ1, . . . , ρn〉 each of length at most ℓ and bounded by d, let Θ contain the formula

This completes the construction of the MSO transduction τΠ,d. Let G be the instance graph of A with degree bounded by d. Clearly, since Π, d and ℓ are fixed, so is τΠ,d. From the construction of Θ, it is easy to verify that τΠ,d(G) has bounded degree as well. It now remains to show that τΠ,d(G) yields the incidence graph of gr(Π ∪ A) as desired. In fact, τΠ,d(G) does not precisely produce the incidence graph of gr(Π ∪ A), as it differs from it in two respects. Firstly, the rules in ∆a produce a vertex for any atom instantiating a predicate, irrespective of whether these atoms actually appear in gr(Π∪A). However, this is not a problem since vertices that do not appear in the grounding are isolated in τΠ,d(G) and thus do not increase the treewidth or the degree of τΠ,d(G). The second difference is the fact that τΠ,d(G) does not contain vertices for the facts from A. However, the incidence graph of gr(Π∪A) contains, for each fact a ∈ A, a rule vertex ra connected only to the vertex for atom a. Adding these vertices and edges increases the treewidth at most by one. These observations and the fact that G, by assumption, has bounded treewidth and degree, together with Proposition 3, prove our claim for the incidence graph of constant-free programs Π. Given a tree decomposition T of the incidence graph, by replacing each rule vertex in a node of T with all adjacent atom vertices in the incidence graph, we obtain a tree decomposition of the primal graph. The fact that, since Π is fixed, the number of atoms in any rule is bounded proves our claim also for the primal graph.

It is tedious, but straightforward, to generalize this proof to programs with constants, and we will only give the general idea here. For each constant occurring in Π, we need to add a constant symbol to our MSO signature. Then we need to adapt the formulas uidℓ,d π1,...,πk , δp[π1,...,πk] and θp[π1,...,πk],r[ρ1,...,ρn] in such a way that they allow any πi or ρj to also be a constant from Π (instead of just a path identifier), representing the fact that the corresponding position in the atom or rule is already filled by a constant.

The proof of Theorem 8 relies on the rather primitive notion of grounding from Definition 2. Incidence graphs obtained from state-of-the-art grounders are generally subgraphs of the output of our transduction. However, since degree and treewidth of a graph can only decrease for a subgraph, Theorem 8 applies also to state-of-the-art grounders.

Thus connection-guarded programs preserve bounded treewidth of an instance A in the grounding, under the condition that the degree of A is also bounded. Unfortunately this condition is necessary, as witnessed by the rule p(X,Z):- e(X,Y), e(Y,Z), where e is extensional: When given a tree of height 1 (and thus of treewidth 1) with n vertices, the incidence graph of the grounding has linear treewidth, as the complete bipartite graph Kn-1,n-1 is a minor of it. Also the restrictions in Definition 6 cannot easily be relaxed without destroying bounded treewidth already with very simple programs: If we allow "unconnected" rules like p(X,Y):- v(X), v(Y), then the complete graph Kn is a minor of the incidence graph of the grounding for any n-vertex instance.

It turns out that, despite their restricted syntax, connectionguarded programs are rather expressive. Straightforward encodings for problems like Graph Coloring or Hamiltonian Cycle directly fall into our class (cf. the second encoding in Example 1). Our final result shows that our class preserves the theoretical complexity bounds of full ASP. Since the encoding for 2QBF in [Leone et al., 2006, Section 3.3.5] is clearly connection-guarded, the following theorem can be immediately obtained:

Theorem 9. For fixed connection-guarded programs, the answer set existence problem is ΣP 2 -complete.

5 Discussion

In this paper we experimentally showed that modern ASP solvers perform better when the ground input programs have small treewidth, all other things being equal. This is strong evidence that one should not only aim for small groundings when encoding problems in ASP, but also for groundings of small treewidth. We furthermore defined the class of connection-guarded non-ground ASP programs, and we proved that grounding such programs together with input facts whose representation as a graph has small treewidth and degree leads to a ground program whose treewidth is also small. Thus we provided an effective tool for exploiting the relationship between treewidth and solving performance in order to obtain more efficient ASP encodings. Future work includes the investigation of alternative classes of programs that preserve small treewidth.

Acknowledgments

This work was funded by the Austrian Science Fund (FWF) under grant number Y698.