Improved Encodings of Acyclicity for Translating Answer Set Programming into Integer Programming

1 Introduction

Answer set programming (ASP) features highly expressive, rule-based languages for knowledge representation and reasoning (see, e.g., [Brewka et al., 2011] for an overview). Typically, the solutions of a search problem are captured as answer sets of the respective logic program encoding the problem. Besides native answer set solvers, the search for answer sets can be implemented (i) by translating rules into other kinds of constraints, e.g., propositional clauses [Janhunen, 2006] or linear (in)equalities [Liu et al., 2012], (ii) by calling alternative solvers capable of satisfying such constraints, and (iii) by extracting answer sets from satisfying assignments. To capture answer sets and extended rules [Simons et al., 2002] properly, such translations must address aggregated conditions, recursive definitions, and default negation. E.g., the Liu et al. [2012] translation from ASP to integer programming (IP) conforms to this structure. In particular, the translation deploys level numbers to rule out self-supporting (circular) recursive definitions and, thus, essentially puts them subject to an acyclicity constraint, cf. [Bomanson et al., 2016].

One important aspect of translating complex problems into IP is coming up with programs whose linear programming (LP) relaxations are reasonably restrictive. Restrictive LP relaxations are important, especially when coupled with advanced optimization techniques such as the branch-and-cut method [Mitchell, 2002]. By relaxing integer constraints in IP, i.e., by allowing variables to take fractional values, a corresponding linear programming relaxation is formulated. The incorporation of restrictive LP relaxations, involving additional constraints or tightened versions of existing ones, becomes synergistic with the branch-and-cut method. This sophisticated optimization approach systematically explores the solution space by iteratively branching on variables and utilizing cutting planes derived from the LP relaxations. The interplay of restrictive relaxations and the branch-and-cut method improves the overall efficiency of optimization, enabling the resolution of more complex problems.

In this work, we introduce two new translations from ASP to IP, building on the prior IP translation [Liu et al., 2012]. In our first translation, we refine the representation of acyclicity constraints using vertex elimination graphs in analogy to [Rankooh and Janhunen, 2022]. The resulting integer programs have more restrictive linear relaxations, enabling IP solvers to prune the search space more efficiently. In our second translation, we improve the representation of the acyclicity constraint in IP based on any feedback vertex set of the underlying dependency graph. The latter translation is particularly effective in settings where vertex elimination becomes computationally costly. The experimental evaluation reveals the superior performance of the new translations in contrast with the Liu et al. [2012] translation. The new vertex elimination based translation with CPLEX is competitive against Clingo, a leading native ASP solver, especially in non-tight Answer Set Optimization (ASO) benchmarks.

While the focus of this paper is on improving answer set solving, it is essential to note that the improved representations of the acyclicity constraint are not exclusive to ASP. Consequently, these can be effectively employed to enhance any IP problems that incorporate acyclicity constraints. This versatility underscores the potential impact and usefulness of the proposed techniques beyond the specific realm of ASP.

We continue with preliminaries in Section 2 and recall the basics of translations in Sections 3 and 4. Our new translations are presented in Sections 5 and 6. Experimental evaluation in Section 7 is followed by conclusions in Section 8.

2 Preliminaries

In the sequel, weight constraint programs (WCPs) [Simons et al., 2002] consist of rules the following three forms:

The symbols a, b1 , . . . , bn where n ≥ 0, and c1 , . . . , cm where m ≥ 0 occurring in the rules signify (propositional) atoms, and the symbol "not" is employed to denote negation by default. The bound k and the weights w1 , . . . ,wn+m in (3) are non-negative integers. Rules of the forms (1)-(3) are classified as normal, choice, and weight rules, respectively, as detailed in [Simons et al., 2002]. Essentially, each rule r provides a basis for deriving its head head(r) = a if the conditions in its body body(r) are fulfilled. In other words, atoms involved can be either derived by other rules or not. For a choice rule r of the form (2), the derivation of head(r) is optional. In the case of a weight rule r of the form (3), head(r) is to be derived when the sum of weights associated with satisfied body conditions must be at least k.

We use body+(r) and body-(r) to denote the sets of atoms b1 , . . . , bn (resp. c1 , . . . , cm) occurring positively (resp. negatively) in body(r). The rules of a positive logic program satisfy m = 0, i.e., are negation free. Given a WCP P, the definition of an atom a in P is the set of rules def(a) = {r ∈ P | head(r) = a}. The signature of a WCP P is defined as the set of atoms At(P ) = ⋃r∈P ({head(r)}∪ body+(r)∪body-(r)). This set comprises atoms that occur in P. The positive dependency graph of P is represented as DG+(P) = 〈At(P),⪰〉, where the relation a ⪰ b holds for a, b ∈ At(P) if head(r) = a and b ∈ body+(r) for some rule r ∈ P. Within this graph, a strongly connected component (SCC) is a maximal subset S ⊆ At(P) wherein all distinct atoms a, b ∈ S are mutually dependent (transitively) on each other through a directed path in DG+(P).

An interpretation I ⊆ At(P) specifies the atoms a ∈ At(P) that are considered true (a ∈ I) and those that are considered false (a ̸∈ I). An interpretation I ⊆ At(P) is deemed to satisfy a rule r ∈ P in the forms (1) and (3), denoted as I |= r, if the fulfillment of the body, expressed as I |= body(r), implies that head(r) ∈ I, i.e., I |= head(r). In the case of a choice rule r of form (2), I |= r unconditionally. Furthermore, the interpretation I is considered a (classical) model of P if I |= r holds for every r ∈ P. For every positive program P, there exists a unique least model denoted as LM(P), obtained as the intersection ⋂{I ⊆ At(P) | I |= P}, the least fix-point of TP operator.

Given an interpretation I, the reduct rI of r concerning I is computed by partially evaluating the negative conditions of r. In the case of a normal rule (1), rI = ∅ if ci ∈ I for some 1 ≤ i ≤ m and rI = {a ← b1 , . . . , bn} otherwise. For a choice rule (2), the latter case additionally necessitates that a ∈ I. Regarding a weight rule (3), rI = {a ← l ≤

[b1 = w1 , . . . , bn = wn]}. Here, the updated bound l is determined from k by subtracting wn+i for each 1 ≤ i ≤ m such that ci ̸∈ I. Finally, for an entire WCP P, the reduct P I = ⋃{rI | r ∈ P} and I is considered a stable model of P if and only if I = LM(P I ). It is also beneficial to distinguish the supporting rules of P with respect to I, denoted as SRP (I) = {r ∈ P | head(r) ∈ I, I |= body(r)}. Then, a model I |= P is supported (by P) when I = {head(r) | r ∈ SRP (I)}. Every stable model of P is supported by P, but supported models are not necessarily stable, as exemplified by I = {a} for the program P = {a ← a.}.

Example 1. Consider a WCP P consisting of the rules:

The signature At(P ) = {a1, a2, a3} and DG+(P ) has SCCs S1 = {a1, a3} and S2 = {a2}. There are two stable models M1 = {a2} and M2 = {a3} justified by reducts P M1 = {a1 ← a2, a3. a2. a3 ← 3 ≤ [a1 = 1, a2 = 2].} and P M2 = {a1 ← a2, a3. a3 ← 0 ≤ [a1 = 1, a2 = 2]}. But the model M2 = {a1, a2, a3} is only supported, not stable. ■

3 Instrumentation with Acyclicity Constraint

Our next objective is to revisit the acyclicity translation TrACYC(P) of a WCP P [Bomanson et al., 2016], which employs special dependency atoms dep(a, b) to represent the activation of the corresponding arc 〈a, b〉 ∈ DG+(P) in the acyclicity constraint. This transformation is applied on an atom-by-atom basis and is necessary only for atoms a ∈ At(P) involved in a non-trivial SCC S of P with |S| > 1. For such an S and an atom a ∈ S, the approach is to instrument P with additional rules that capture well-support for a (cf. [Bomanson et al., 2016]). For every arc 〈a, b〉 ∈ DG+(P) that is specific to S, the potential dependency of a on b is articulated through a choice rule {dep(a, b)} ← b. In addition to the dependency atoms, special atoms are introduced to enforce well-support for the atom a with respect to its defining rules {r1 , . . . , rk} = def(a). These special atoms are denoted as ws(r1) , . . . , ws(rk), and they are utilized in a constraint that ensures well-support for a: f ← a, not ws(r1) , . . . , not ws(rk), not f Here, f is introduced as a new atom. Given the SCC S of a in P, it is assumed that each body+(r) in (1)-(3) is ordered in such a way that for some 0 ≤ l ≤ n, b1 ∈ S , . . . , bl ∈ S while bl+1 ̸∈ S , . . . , bn ̸∈ S. Then, if a defining rule r ∈ def(a) is of the form (1) or (2), the rule (4) below captures well-support mediated by r. If the defining rule r is of the form (3), then the corresponding rule for well-support is (5).

For the program TrACYC(P) constructed in this manner, the distinction between stable and supported models disappears when we specifically consider acyclic models I. An acyclic model I is one in which the digraph induced by the set of arcs {〈a, b〉 | dep(a, b) ∈ I} is acyclic.

Proposition 1 ([Bomanson et al., 2016, Theorem 3.11]). Let P be a WCP.

1. If M is a stable model of P, then TrACYC(P) has an acyclic supported model N such that M = N ∩ At(P ).
2. If N is an acyclic supported model of TrACYC(P), then M = N ∩ At(P) is a stable model of P and wellsupported by R = {r ∈ P | ws(r) ∈ N, head(r) ∈ N}.

Example 2. Consider the program in Example 1. Remember that S = {a1, a3} is the only non-trivial SCC. Let r1 be the defining rule for a1, and r2 the one for a3. By adding rules

we can ensure that all acyclic supported models of the program are stable. In particular, we note that the model N = {a1, a2, a3, dep(a1, a3), dep(a3, a1), ws(r1), ws(r2)} is supported, but not acyclic and, therefore, not stable. ■

4 Translation into Integer Programming

Once the acyclicity translation TrACYC(P) of a WCP P is obtained, translating P to an integer program is possible. This translation has previously been done in [Liu et al., 2012], which we review here. We proceed by breaking down the translation into two parts: (i) translation of rules in TrACYC(P) and (ii) translation of acyclicity. For the rest of this paper, we assume that DG+(P) only includes arcs with both ends in the same SCC. This assumption does not harm the generality of our arguments in the sequel, as such arcs are the only ones of value as long as acyclicity is concerned.

4.1 Translation of Rules

Given a WCP P, for the sake of simplicity, we assume that members of At(P) are indexed in the form of a1, ..., an. We define a mapping V that maps every atom a ∈ At(P) to a binary variable a, and every atom dep(ai, aj) ∈ At(TrACYC(P)) to a binary variable x〈i,j〉 to represent the respective atoms. Also, for each rule in TrACYC(P), we consider a binary variable bdr to represent the notion of r causing the truth of its head. We construct an integer program IPrP by adding inequalities (6) and (7) from below. For every normal rule r of TrACYC(P) in the form (1), we include

and

Inequality (6) guarantees that if the body of r is satisfied, bdr must be set to one. Inequality (7) is for the completion and prevents bdr to be one unless the body holds. For every choice rule r of TrACYC(P) in the form (2), only inequality (7) is needed. That is because even if the body of r is satisfied, r may not cause its head to be in the answer set. For every weight rule r of TrACYC(P) in the form (3), we include

Similarly to the case of normal rules, (8) guarantees that if the body of r is satisfied, bdr must be set to one, and the inequality (9) prevents bdr from being one unless the body holds. For every atom a ∈ At(TrACYC(P)) we include

and

Inequality (10) guarantees that if at least one rule causes a ∈ At(TrACYC(P)) to be in the answer set, then V(a) must be set to one. Inequality (11) causes V(a) to be zero in the case that no rule is causing a to be included in the answer set.

4.2 Translation of Acyclicity

For a ∈ At(P), let SCC(a) denote the strongly connected component of DG+(P) = 〈At(P), ⪰〉 including a. We construct integer program IPoP by adding for every 〈ai, aj〉 ∈ ⪰,

Inequality (12) is a translation of the Bellman-Ford equation [Bellman, 1958] into integer programming, which causes every model M to set xi to the length of the longest path reaching ai in the graph induced by {〈ai, aj〉 | M(x〈i,j〉) = 1}. As a result every assignment causing a cycle in its induced graph cannot be consistent. It should be clear that for every variable xi, the upper bound on the value assigned by any model to xi is |SCC(ai)|.

It has been shown that the union of IPrP and IPoP is a correct IP translation of P .

Proposition 2 ([Liu et al., 2012]). Let P be a WCP.

1. If M is a stable model of P, then IPrP ∪IPoP has a model N such that if x ∈ M then N(V(x)) = 1.
2. If N is a model of IPrP ∪IPoP , thenM = {x|N(V(x)) = 1} ∩ At(P ) is a stable model of P .

5 Acyclicity via Vertex Elimination

The concept of vertex elimination graphs, originally introduced by Rose and Tarjan [1975], has been recently shown effective for guaranteeing acyclicity in constraint programs with underlying graphs [Rankooh and Rintanen, 2022; Rankooh and Janhunen, 2022; Zhou et al., 2023]. Here, we show that using vertex elimination graphs, one can produce IP translations of answer set programs with more restrictive LP relaxations compared to that of IPrP ∪ IPoP . Furthermore, we prove that a feedback vertex set (a subset of vertices that contains at least one vertex from every cycle in the graph) of a graph can be obtained as a byproduct of the vertex elimination process. We later use the obtained feedback vertex set to improve the IP encoding (12) of the Bellman-Ford equation.

5.1 Vertex Elimination Graphs

Given a digraph G = 〈V,E〉, an ordering of V is a bijection α : {1, . . . , n} → V . The fill-in F(v) for a vertex v in a directed graph is essentially the set of arcs that, if added, would form a complete neighborhood around the vertex v. In other words, it is the set of arcs from the in-neighbors of v to the out-neighbors of v, formally defined as

The v-elimination graph of G is obtained by removing the vertex v from G, and adding the fill-in of v to the resulting graph. Formally, it is represented as G(v) = 〈V \ {v},E(v) ∪F(v)〉, where E(v) = {〈x, y〉 | 〈x, y〉 ∈ E, x ̸= v, y ̸= v}.

Given a digraph G and an ordering α of its vertices, the elimination process of G according to α is the a sequence denoted as G = G0, G1, . . . , Gn-1, where Gi is the α(i)- elimination graph of Gi-1 for i = 1, . . . , n - 1. This elimination process is performed iteratively for each vertex in the specified ordering α. At each step, a vertex is eliminated, and the associated fill-in arcs are added to the graph, resulting in a sequence of graphs.

The fill-in of the digraph G according to the ordering α, denoted by Fα(G), is the set of all arcs added to G in the vertex elimination process. Formally, Fα(G) is defined by (14) where f(v) is the fill-in of v = α(i) in the graph Gi-1:

The vertex elimination graph of G according to α, denoted by G ∗α, is defined as the union of all graphs produced in the elimination process of G according to α:

The elimination width of α [Hunter and Kreutzer, 2008] is defined by the maximum number of outgoing arcs of vertex α(i) in Gi-1, for i = 1, ..., |V |. The asymptotic number of arcs in G ∗α is then O(|E| + δ|V |), where δ is the elimination width of α. The problem of finding the optimal ordering function, one with the smallest elimination width, has been shown to be NP-complete [Rose and Tarjan, 1975]. Nevertheless, there are effective heuristics for finding empirically useful orderings. Examples are the minimum fill-in and minimum degree that accordingly choose a vertex for removal at each step during the elimination process. An important property of the vertex elimination process is that if the original graph G has a directed cycle, then G ∗α will have a cycle of length 2. This property is independent of the specific ordering α and is inherent to the nature of the elimination process in the presence of directed cycles.

Theorem 1. Let G = 〈V,E〉 be a digraph, α an ordering of its vertices, and G ∗α the vertex elimination graph of G according to α. For every cycle v1, ..., vk, v1 in G, there exists some vi, vj ∈ {v1, ..., vk} such that arcs 〈vi, vj〉 and 〈vj, vi〉 are both present in G ∗α.

Proof. We give the proof by induction on k. For the case of k = 2, we have the cycle v1, v2, v1. The conclusion holds because G is a subgraph of G ∗α. Now assume that the conclusion holds for every cycle of length k. Let v1, ..., vk+1, v1 be a cycle of length k + 1 in G. Let vl be the first member of {v1, ..., vk+1} that is eliminated according to α. Assume without loss of generality that 1 < l < k + 1 (otherwise we can always reorder indices of the cycle to make this assumption hold). Now v1, ..., vl-1, vl+1, ..., vk+1, v1, produced after eliminating vl, is a cycle of length k in G ∗α. By the induction hypothesis, there exist some vi, vj ∈ {v1, ..., vl-1, vl+1, ..., vk} such that arcs 〈vi, vj〉 and 〈vj, vi〉 are both present in G ∗α.

Theorem 1 shows how every cycle of a directed graph can be represented by a pair of vertices in it. As a result, by choosing one vertex out of each of such pairs, one can obtain a feedback vertex set.

Corollary 1. Let G = 〈V,E〉 be a digraph, α an ordering of its vertices, and G ∗α the vertex elimination graph of G according to α. Let F be the set of all vertices v ∈ V such that for some u ∈ V ordered by α after v, arcs 〈v, u〉 and 〈u, v〉 are both present in G ∗α. Then F is a feedback vertex set of G.

5.2 Vertex Elimination Based Translation

Let α be an ordering of vertices of DG+(P), and G0, . . . , Gn-1 the elimination process of DG+(P) according to α. We produce the IPve P by adding the following. For every arc 〈ai, aj〉 in DG+(P), we add

For every 〈ai, aj〉 ∈ f(ak), we add

and for every i and j with 〈ai, aj〉 ∈ G ∗α and 〈aj , ai〉 ∈ G ∗α,

Let Var(X) denote the set of variables in an integer/linear program X. Considering Proposition 1, Theorem 2 shows that there is a correspondance between the set of stable models of P and the set of integer models of IPrP ∪ IPve P .

Theorem2. If IPrP ∪IPve P has amodelM, then the restriction of M on Var(IPrP ) is an acyclic model of IPrP . If N is an acyclic model for IPrP , then there is an extension of N that is a model for IPrP ∪ IPve P .

Proof. Let M be a model for IPrP ∪ IPve P . Then M is a model of IPrP . Assume M is not acyclic. Without loss of generality (regarding the indices of vertices) assume that the graph induced by {〈ai, aj〉 | M(x′〈i,j〉 ) = 1}, denoted by H, has a cycle a1, ..., ak, a1. According to Theorem 1, there are vertices ai and aj such that 〈ai, aj〉 and 〈aj, ai〉 are both present in H∗α. However, because H is a subgraph of G = DG+(P), H∗α is clearly a subgraph of G ∗α, and by (16) and (17), we have: M(x′〈i,j〉 ) = 1 and M(x′〈j,i〉 ) = 1. Therefore, M(x′〈i,j〉 ) +M(x′〈j,i〉 ) = 2 that contradicts (18).

Let N be an acyclic model for IPrP . We construct a model N ′ for IPrP ∪ IPve P as an extension of N by letting N ′ (x) = N(x) for x ∈ Var(IPrP ). The graph induced by {〈ai, aj〉 | N(x〈i,j〉) = 1}, denoted by D is acyclic, and there is a topological total ordering β of vertices of DG+(P) according to D. We set N ′ (x′〈i,j〉 ) to 1, for arcs 〈ai, aj〉 in D∗α if and only if ai is ordered before aj according to β. We show that N ′ satisfies (16) to (18), by these settings.

• If N(x〈i,j〉) = 1, then there is an arc from ai to aj in D, and therefore aj is ordered after ai according to β. Thus, N ′ (x′〈i,j〉 ) = 1 and inequality (16) is satisfied.
• For every 〈ai, aj〉 ∈ f(ak), if either N ′ (x′〈i,k〉 ) = 0 or N ′ (x′〈k,i〉 ) = 0, then inequality (17) is trivially satisfied. However, if N ′ (x′〈i,k〉 ) = 1 and N ′ (x′〈k,i〉 ) = 1, then ai is ordered before ak, and ak is ordered before aj according to β. Therefore, ai is ordered before aj according to β. Thus, N ′ (x′〈i,j〉 ) = 1 and inequality (17) is satisfied.
• For every i and j such that 〈ai, aj〉 ∈ G ∗α, if N ′ (x′〈i,j〉 ) = 1, then ai is ordered before aj according to β, and N ′ (x′〈j,i〉 ) = 0. We conclude that (18) is satisfied.

We now show that the linear relaxation of our vertex elimination based translation is at least as restrictive as the linear relaxation of the translation introduced by Liu et al. [2012].

Lemma 1. Let LPve P be the LP relaxation of IPrP ∪ IPve P , and v1, ..., vk, vk+1 = v1 be a cycle in G ∗α. If M is a model for LPve P , then ∑i=1,...,k M(x′〈i,i+1〉 ) ≤ k - 1.

Proof. We give the proof by induction on k. For k = 2, the conclusion holds because M satisfies constraint (18). Assume that the conclusion holds for any cycle of length k. Let v1, ..., vk+1, vk+2 = v1 be a cycle in G ∗α of length k + 1. Assume the vj is the first vertex in this cycle eliminated according to the ordering α. Then v1, ..., vj-1, vj+1, ..., vk+2 = v1 must be a cycle of length k in G ∗α. Therefore ∑i=1,...,j-2,j+1,...,k+1 M(x′〈i,i+1〉 ) + M(x′〈j-1,j+1〉 ) ≤ k - 1. However, since according to (17), M(x′〈j-1,j〉 ) + M(x′〈j,j+1〉 ) - 1 ≤ M(x′〈j-1,j+1〉 ), we have ∑i=1,...,j-2,j+1,...,k+1 M(x′〈i,i+1〉 ) + M(x′〈j-1,j〉 ) + M(x′〈j,j+1〉 ) - 1 ≤ k - 1, and therefore, ∑i=1,...,k+1 M(x′〈i,i+1〉 ) ≤ k

Let LPve P and LPoP be the LP relaxation of IPrP ∪ IPve P and IPrP ∪ IPoP , respectively. Assume that LPve P has a feasible model M. We produce LPo,M P , by replacing (12) in LPoP with

Lemma 2. For every model M of LPve P , LPo,M P has a model N such that N(a) = M(a) for every a ∈ Var(IPrP ).

Proof. From M, we construct a model N for LPo,M P . For every variable a ∈ Var(IPrP ), let N(a) = M(a). Let GM be a weighted graph with the same vertices as in DG+(P). For every arc 〈ai, aj〉 in DG+(P), we add 〈ai, aj〉 to GM with weight (-M(x′〈i,j〉 ) + 1)|SCC(ai)| - 1, denoted by w〈i,j〉. We show that there is no simple directed cycle with negative total weight in GM. Assuming the necessary renaming of variables, let a1, ..., ak, ak+1 = a1 be a simple directed cycle in GM. Then a1, ..., ak, ak+1 = a1 is also a simple directed cycle in G ∗α, the vertex elimination graph of DG+(P). Therefore, according to Lemma 1 we have ∑i=1,...,k M(x′〈i,i+1〉 ) ≤ k - 1. On the other hand, we have: ∑i=1,...,k w〈i,i+1〉 = -k + k|SCC(ai)| - |SCC(ai)| ∑i=1,...,k M(x′〈i,i+1〉 ) ≥ -k + k|SCC(ai)| - (k - 1)|SCC(ai)| = |SCC(ai)| - k ≥ 0. Now, let N(ai) be the minimum total weight over all simple paths leading to ai in GM. Since there is no simple directed cycle with negative total weight in GM, N is well-defined. Moreover, for every 〈i, j〉 in DG+(P), since there is an arc with weight (-M(x′〈i,j〉 ) + 1)|SCC(ai)| - 1 from ai to aj, we have N(xi) - N(xj ) ≥ (M(x′〈i,j〉 ) - 1)(|SCC(ai)|) + 1.

Theorem 3. If LPve P is feasible, so is LPoP .

Proof. We construct LPo,M P , where M is a model of LPve P . According to Lemma 2, LPo,M P has some model N such that N(a) = M(a) for every a ∈ Var(IPrP ). Therefore, (6) to (11) are satisfied by N. According to (16), for all arcs 〈i, j〉 of DG+(P), we have M(x′〈i,j〉 ) ≥ M(x〈i,j〉) = N(x〈i,j〉). Therefore, for every arc 〈ai, aj〉 in DG+(P), we have N(xi) - N(xj ) ≥ (M(x′〈i,j〉 ) - 1)(|SCC(ai)|) + 1 ≥ (N(x〈i,j〉) - 1)(|SCC(ai)|) + 1. Thus N satisfies (12).

Theorem 3 shows that LPve P is at least as restrictive as LPoP . Moreover, Lemma 2 shows that if LPve P is feasible, then for every single model M of LPve P , the linear program LPo,M P , which is at least as restrictive as LPoP , is feasible. This suggests that using IPrP ∪ IPve P could often result in a more efficient pruning of the search space compared to IPrP ∪ IPoP . By an example we demostrate how LPve P could easily be strictly more restrictive than LPoP .

Example 3. Consider the program presented in Example 2. Since the positive dependency graph of P has only two arcs 〈a1, a3〉 and 〈a3, a1〉, the vertex elimination process does not add any other arcs. Let M(x〈1,3〉) = 0.5 and M(x〈3,1〉) = 0.6. Because of inequalities (16) and (18), M cannot be a model for LPve P . Since there is no other node in the same SCC, then M can neither be a model for LPoP . However, if there was one other node a4 in the same SCC, then, regardless of the values assigned by M to variables relevant to x4, inequalities in the form of (12) become x1 - x3 ≥ -0.5 and x3 - x1 ≥ -0.2, which can be satisfied by letting M(x1) = M(x3) = 0. From this example it should also be clear how larger SCCs weaken the linear relaxation of inequality (12) even more. ■

6 Acyclicity via Feedback Vertex Sets

As mentioned in Section 5, the asymptotic number of arcs added by vertex elimination is O(δ|V |), where δ and V represent the elimination width and the number of vertices, respectively. In cases where both δ and |V | are high, our vertex elimination based method may generate integer programs of considerable size, potentially negating the benefits of its more informative linear relaxation.

To address this issue, we introduce an alternative method in this section. This approach utilizes the same set of variables as in LPoP but imposes (implicit) constraints on the domains of variables involved in cycle detection. We achieve this by taking advantage of feedback vertex sets (FVSs). FVSs have previously been used in SAT-based ASP to reduce the number of variables while guaranteeing that number of models remains fixed [Hecher and Kiesel, 2023]. Here, however, we use FVSs to restrict the possible values of integer variables, while maintaining the satisfiability (or optimal value of the objective function) of our translation.

Let F be any feedback vertex set of DG+(P). We construct integer program IPfP by adding for every ai ∈ F and 〈ai, aj〉 ∈ DG+(P), the inequality

and for every ai /∈ F and 〈ai, aj〉 ∈ DG+(P), the inequality

Theorem4. If IPrP ∪IPfP has amodelM thenM is an acyclic model of IPrP . If N is an acyclic model for IPrP then there is an extension of N that is a model for IPrP ∪ IPfP .

Proof. Let M be a model for IPrP ∪ IPfP . Then M is a model of IPrP . Assume that M is not acyclic. Then, assuming the necessary renaming of variables, the graph induced by {〈ai, aj〉 | M(x〈i,j〉) = 1} has a cycle a1, ..., ak, a1, and thus, M(x〈1,2〉) = ... = M(x〈k,1〉) = 1. Since F is a feedback vertex set for DG+(P), at least one of a1, ..., ak, say aj, must be in F. We can assume that j ̸= k, otherwise we reorder the indices to make this assumption hold. According to (20), M(xj) > M(xj+1) and according to (20) and (21), M(x1) ≥ M(x2) ≥ ... ≥ M(xk) ≥ M(x1). We conclude that M(x1) > M(x1), a contradiction.

Let N be an acyclic model for IPrP . We construct a model N ′ for IPrP ∪ IPfP as an extension of N by letting N ′ (a) = N(a) for a ∈ Var(IPrP ). Let GN be a weighted graph with the same vertices as in DG+(P). For every arc 〈ai, aj〉 in DG+(P), we add 〈ai, aj〉 to GN iff N(x〈i,j〉) = 1. Every arc 〈ai, aj〉 of GN is assigned a weight of one if aj ∈ F, and a weight of zero otherwise. Since N is acyclic, GN is a weighted DAG, and therefore, the set of all directed paths leading to any given vertex is finite. Now, for every vertex xi we set N ′ (xi) to the maximum total weight over all directed paths leading to ai in GN. We show that N ′ satisfies inequality (20) and (21). If N(x〈i,j〉) = 0, (20) and (21) are satisfied because, (i) if N ′ (ai) = 0, ai has no incoming arc in GN, and no path to aj can have a total weight greater than |F ∩SCC(ai)|-1; and (ii) by the definition of N ′ , for every vertex ai ∈ F we have: 0 ≤ N ′ (xi) ≤ |F ∩ SCC(ai)|. On the other hand, if N(x〈i,j〉) = 1, there is an arc in GN from ai to aj. Then N ′ satisfies inequality (20) because if aj ∈ F, the weight of 〈ai, aj〉 is one. Similarly, inequality (21) holds because if aj /∈ F, the weight of 〈ai, aj〉 is zero.

From the proof of Theorem 4, it should be clear that for every model M of IPrP ∪IPfP , M(xi) is at most |F ∩SCC(ai)|, which is a lower bound of |SCC(ai)|, the bound necessary in IPrP ∪ IPoP for xi.

7 Empirical Evaluation

We have taken the Acyc2solver tool from the ASPTOOLS collection 1 , and incorporated our encoding methods into it. With the exception of acyclicity encoding, all other features of the Acyc2solver tool remain unaltered in our implemented translators. Consequently, the translation results for all ASP rules in both our translators' outputs and the original Acyc2solver tool's output are identical. We have added the resulting translators to the ASPTOOLS collection.

All experiments were conducted on a Linux cluster featuring Intel Xeon 2.40 GHz CPUs, employing a timeout of 600 seconds per problem and a memory limit of 8 GB. For our vertex elimination based method, the order of elimination was determined using the minimum degree heuristic. This involves eliminating a vertex with the minimal total number of incoming and outgoing arcs in the graph produced after eliminating previously processed vertices. In our feedback vertex set based method, we utilized the feedback vertex set generated by an implementation of Corollary 1.

We assess our two translations: the vertex elimination based translation VE and the feedback vertex set based translation FVS. Our opponents include the original implementation of the Acyc2solver tool (A2S) and Clingo 5.4.0 [Gebser et al., 2019], a prominent native ASP solver, using both Branch and Bound (BB) and Unsatisfiable Core (USC) guided optimization strategies of Clingo for optimization problems. Additionally, we employ Gurobi Optimizer version 11.0.0 2 and IBM ILOG CPLEX Optimization Studio 20.1 3 as IP solvers, known for their efficiency. The number of available threads has been set to one for all solvers. Although both Gurobi and CPLEX offer a variety of parameters to control the search, we only use the default ones. Therefore, the solvers' parameters have not been tuned to produce the best performance for our new methods.

The benchmark set comprises non-tight problem sets from previous ASP competitions. A problem is considered nontight if its positive dependency graph has at least one nontrivial strongly connected component. It is important to note that for tight problems, our translations are not of particular interest, as they yield results identical to the original Acyc2solver tool. Our evaluation encompasses both decision and optimization problem sets.

1 https://github.com/asptools/software

2 https://www.gurobi.com/solutions/gurobi-optimizer

3 https://www.ibm.com/products/ilog-cplex-optimization-studio

The optimization problem sets (with their corresponding competition year in parantheses) consist of Bayesian Network Learning (2017), Connected Maximum-Density Still Life (2015), Markov Network Learning (2017), Traveling Salesman Problem (2017), and Valves Location Optimization (2015), abbreviated as Bayes, Connect, Markov, TSP, and Valve in our table presentations, respectively. The decision problem sets include Combined Configuration (2015), Knight Tour With Holes (2015), Labyrinth (2015), Maze Generation (2011), and Random NonTight (2007), shortened as Comb, Knight, Lab, Maze, and Rand. It is important to note that we have not included the Steiner Tree problem set from the 2017 competitions in our experiments. This is due to the acyc2solver tool's inability to generate the integer programs within the specified time and memory constraints for this benchmark. Additionally, we incorporate the Hamiltonian cycle encoding from [Niemel¨a, 1999], denoted as Ham, which comprises 30 randomly generated planar graphs with 60, 70, . . . , 150 nodes, totaling 300 instances. The numbers of problems solved for optimization and decision problem sets are detailed in Tables 1 and 2, respectively.

Several observations can be drawn from our empirical results. A comparison between Gurobi and CPLEX in Tables 1 and 2 reveals that Gurobi performs better for optimization problems, while CPLEX exhibits superior performance for decision problems. When contrasting our translators (VE and FVS) with A2S, a consistent trend emerges: VE outperforms FVS and A2S when coupled with Gurobi in optimization problems, and with CPLEX in decision problems. An exception to this trend is the Knight Tour With Holes problem set, where both FVS and A2S significantly outperform VE. This anomaly is attributed to the large elimination widths (ranging in the order of hundreds, the largest among all problem sets) and substantial SCC sizes (ranging in the order of thousands, also the largest among all problem sets) in the positive dependency graphs of this problem set. This results in adding hundreds of thousands of extra variables to the integer program when vertex elimination is used, explaining the low efficiency of the solvers. Additionally, it is noteworthy that FVS solves at least as many problems as A2S across all problem sets, outperforming it in several of them.

Table 1 illustrates that VE with Gurobi as the solver exhibits competitive performance compared to both BB and USC strategies of Clingo. However, Clingo demonstrates superior efficiency compared to VE and other integer programming based methods when solving decision problems, as depicted in Table 2. The primary advantage of IP methods lies in their exploitation of the branch and cut search strategy using linear relaxation. However, this strategy is less advantageous in integer problems without an objective function, where linear relaxation is informative only if it is not feasible. Thus, the gains from using these methods are expected to be less prominent in the decision problem set. This study represents an effort to bridge the efficiency gap between these two paradigms of solving answer set programs, leaving further investigation in this direction for future research.

8 Conclusions

In this paper, we investigate novel translation techniques that could be used to speed up the computation of answer sets when logic programs are translated into integer programs and the respective IP solvers, such as CPLEX and Gurobi, are used for computations. The latest ASP competition results [Gebser et al., 2017; Gebser et al., 2020] suggest that the performance of CPLEX is quite much behind the native ASP solvers on benchmarks in the optimization categories of the competitions. However, based on the experimental results of Section 7-as collected in Tables 1 and 2-the performance gap seems to be closing. In our view, this study serves as a validation for a key motivation behind translation-based Answer Set Programming, emphasizing the utilization of the strengths from both knowledge representation and constraint solving domains.

Besides promising experimental results, this paper has a number of technical contributions that may turn out very useful otherwise. First of all, we present new ways to encode the acyclicity constraint when embedded in integer programming, but the idea is more generic and potentially applicable in other contexts as well. Second, the exploitation of feedback vertex sets in the simplification of the translation opens up new avenues for further research. In particular, it is an interesting generalization of [Chen et al., 2008] where loops with only one externally supporting rule are distinguished.

Acknowledgements

This research is supported by the Research Council of Finland project XAILOG (#345633).