Eliminating Disjunctions in Answer Set Programming by Restricted Unfolding

1 Introduction

Disjunctive logic programs extend normal logic programs by permitting disjunctions to appear in rule heads, which increases the expressive power of logic programs under the answer set semantics [Baral, 2003] and brings computational penalty as well. In particular, deciding whether a disjunctive program has an answer set is ⌃P2 -complete [Eiter and Gottlob, 1995] while deciding whether a normal program has an answer set is NP-complete. In practice, significant performance difference can be observed after adding disjunctive rules into normal programs, even if only a very small number of disjunctive rules are involved. Meanwhile, it is arguable that many real-life problems can be characterized by programs consisting of a large number of normal rules and a few disjunctive rules. Hence, an interesting question is whether such a disjunctive program can be efficiently rewritten to an equivalent normal program under the answer set semantics.

⇤Corresponding author

Ben-Eliyahu and Dechter [1994] identified a class of disjunctive programs, called "Head-Cycle-Free" (HCF), and showed that each HCF program can be converted into an equivalent normal program in polynomial time by shifting head atoms into the body. The class of HCF programs is further generalised to that of Head-Elementary-loop-Free (HEF) programs [Gebser et al., 2011], which can be transformed into normal programs in polynomial time by shifting too. One could identify another proper super class of HEF programs that are polynomial time convertible to normal programs but it would be getting harder to check if a given disjunctive program is in such a class [Ji et al., 2015].

On the other hand, it is well known that a disjunctive program can be equivalently transformed into a negative disjunctive program by a set of program transformations including the unfolding transformation [Brass and Dix, 1997; Eiter and Wang, 2008]. Since shifting preserves the answer set semantics for negative disjunctive programs, each disjunctive program can be equivalently transformed into a normal program [Zhou, 2014]. Given that the unfolding transformation is exponential in the worst case, an exponential blowup may occur in the unfolding-based rewriting. One source for this blow-up is from that unfolding can be applied on all atoms in the given disjunctive program. However, it has not been explored how the efficiency of unfolding can be improved in the context of disjunctive answer set programming. Especially, it is unclear if the unfolding transformation can be applied on only some atoms that are necessary.

A natural idea is to apply unfolding on atoms of the program one by one until the resulting program is HCF. However, unfolding may introduce new head-cycles and increase the set of atoms to be unfolded. Hence, generally speaking, one may need to unfold at all the atoms to achieve an HCF program, which indeed results in a negative program as in [Zhou, 2014]. In this paper, we show that we can restrict unfolding to "culprit" atoms, i.e., atoms that prevent the initial program to be HCF, and ignore new atoms that prevent the resulting program to be HCF. We prove that the result of our restricted unfolding, although not necessarily HCF, can be equivalently transformed to a normal program via shifting.

This result is of both theoretical and practical interests-it not only shows that the complexity penalty is closely tied to these "culprit" atoms, but also suggests the practicality of our rewriting approach on disjunctive programs that are "almost" HCF, i.e., with only a small number of "culprit" atoms. We make the following contributions:

• ÷ We provide an answer-set-preserving rewriting from a disjunctive program to a normal program by only unfolding at "culprit" atoms and shifting the resulting program, which is efficient for "almost" HCF programs.
• ÷ If ⇧0 is a normal program rewritten from a disjunctive program ⇧ by restricted unfolding and shifting, we show that the computation of answer sets for ⇧0 can be improved. In particular, although the rewriting may introduce new loops to ⇧0 , we only need to consider loops constructed from loops of ⇧ for computing answer sets of ⇧0 . This result suggests that although our rewriting to a normal logic program may lead to an exponential blow-up, there is not necessarily a blow-up in loop formulas.
• ÷ As another application of the rewriting, we present an anytime algorithm to compute answer sets of a disjunctive program ⇧ by calling solvers for normal logic programs. In each iteration, the algorithm outputs the answer sets of the shifted program ⇧0 obtained from ⇧ by unfolding at a set A of atoms. The algorithm will output more answer sets of ⇧ when a larger A is applied.
• ÷ At last, we extend the rewriting to non-ground answer set programs on finite structures. As a result, we are able to compute answer sets of some first-order disjunctive logic programs by a solver for first-order normal programs such as [Asuncion et al., 2012].

2 Preliminaries

2.1 Disjunctive Logic Programs

We consider fully finite logic programs based on a propositional language L until Section 7. A (disjunctive) logic program (DLP) is a finite set of (disjunctive) rules of the form

where n ≥ m ≥ k ≥ 1 and a1↪ ▷ ▷ ▷ ↪ an are atoms. If k = 1, it is a normal rule; if k = m, it is a negative rule; if m = n, it is a positive rule. A normal logic program (NLP) is a finite set of normal rules and a negative logic program (resp. positive logic program) is a finite set of negative (resp. positive) rules.

We will also write a rule r of form (1) as

where head(r) is a1 _ · · · _ ak, body(r) = body+(r) ^ body-(r), body+(r) is ak+1 ^ · · · ^ am, and body-(r) is ≻am+1 ^ · · · ^ ≻an, and we identify head(r), body+(r), body-(r) with their corresponding sets of atoms, and body(r) the set ¶ ak+1↪ ▷ ▷ ▷ ↪ am↪ ≻am+1↪ ▷ ▷ ▷ ↪ ≻an ♦. Given a DLP ⇧, we use Atoms(⇧) to denote the set of atoms occurring in ⇧. We use tr(r) to denote the propositional formula body(r) ⊃ head(r) and tr(⇧) = Vr2⇧ tr(r).

A set S of atoms satisfies a rule r if S [ ¶≻p ♣ p ◁2 S♦ ♣= tr(r) in the sense of propositional logic. S satisfies a program ⇧ if S satisfies every rule in ⇧.

The answer sets of a DLP are defined in [Gelfond and Lifschitz, 1991]. Given a DLP ⇧ and a set S of atoms, the Gelfond-Lifschitz reduct of ⇧ on S, written ⇧S , is obtained from ⇧ by deleting:

1. each rule that has a formula not p in its body with p 2 S,
2. all formulas of the form not p in the bodies of the remaining rules.

A set S of atoms is an answer set of ⇧ if S is a minimal set satisfying ⇧S . We use AS(⇧) to denote the set of answer sets of ⇧.

2.2 Loops and Loop Formulas

Lee and Lifschitz [2003] extended the notions of loops and loop formulas [Lin and Zhao, 2004] to DLPs. For a DLP ⇧, the positive dependency graph of ⇧, written G⇧, is the directed graph whose vertices are atoms in ⇧, and there is an arc from p to q if there is a rule r 2 ⇧ such that p 2 head(r) and q 2 body+(r). A set L of atoms is a loop of ⇧ if the L-induced subgraph of G⇧ is strongly connected. Note that, every singleton whose atom occurs in ⇧ is also a loop of ⇧. We use Loop(⇧) to denote the set of loops of ⇧.

Given a DLP ⇧ and a loop L of ⇧, a rule r 2 ⇧ is an external support of L under ⇧ if head(r) \ L 6= ; and L \ body+(r) = ;. Let R-(L↪ ⇧) be the set of external support rules of L under ⇧. The (conjunctive) loop formula of L under ⇧, written LF(L↪ ⇧), is the following implication:

Theorem 1 (Theorem 1 in [Lee and Lifschitz, 2003])

For a DLP ⇧ and a set S of atoms, S is an answer set of ⇧ iff S [ ¶≻p ♣ p ◁2 S♦ is a model of tr(⇧) ^ VL2Loop(⇧) LF (L↪ ⇧)▷

2.3 Unfolding and Shifting

We first review the unfolding transformation [Gergatsoulis, 1997; Brass and Dix, 1997].

Definition 1 (Elementary unfolding) Let r1, r2 be two rules and there is an atom a 2 head(r1) \ body+(r2). The rule obtained by elementary unfolding r2 using r1 at a, denoted by unfold(r1↪ r2↪ a), is the rule r such that head(r) = (head(r1) ∩ ¶a♦) [ head(r2) and body(r) = body(r1) [ (body(r2) ∩ ¶a♦).

Definition 2 (Unfolding rules at an atom) Let ⇧ be a DLP and a an atom in ⇧. The set of rules obtained by unfolding rules at a in ⇧, denoted by unfold⇧(a), is the set ¶unfold(r1↪ r2↪ a) ♣ r1↪ r2 2 ⇧ and a 2 head(r1) \ body+(r2)♦.

Let ⇧ be a DLP and a 2 Atoms(⇧). We denote

Example 1 Consider the logic program⇧1:

unfold⇧1 (a) is the set of rules:

From Theorem 13 in [Gergatsoulis, 1997], we have the following theorem.

Theorem 2 Let ⇧ be a DLP and a an atom in ⇧. Then AS(⇧) = AS(remove(⇧↪ a)).

Given a DLP ⇧, E ✓ Atoms(⇧), and a 2 E, we can inductively define remove(⇧↪ E) as follows:

• ÷ remove(⇧↪ ¶a♦) = remove(⇧↪ a),

Corollary 3 Let ⇧ be a DLP and E ✓ Atoms(⇧). Then AS(⇧) = AS(remove(⇧↪ E)).

• ÷ remove(⇧↪E) = remove(remove(⇧↪ E ∩ ¶a♦)↪ ¶a♦).

Gelfond et al. [1991] provided a mapping from a DLP to an NLP by "shifting" head atoms into the bodies. We denote sh(⇧) to be the NLP obtained from a DLP ⇧ by substituting every rule of form (1) with the k rules

It is known that every answer set of sh(⇧) is also an answer set of ⇧, but the converse is not true in general. BenEliyahu and Dechter [1994] identified a class of DLP, called "Head-Cycle-Free" (HCF), and showed that the converse is true if ⇧ is an HCF program. In particular, a DLP ⇧ is called HCF, if ♣head(r) \L♣  1 for every rule r of ⇧ and every loop L of ⇧, and the answer sets of an HCF program ⇧ coincide with the answer sets of the NLP sh(⇧).

Given a DLP ⇧, remove(⇧↪Atoms(⇧)) is equivalent to a negative program [Brass and Dix, 1997], which is HCF. Then AS(⇧) = AS(remove(⇧↪Atoms(⇧))) = AS(sh(remove(⇧↪Atoms(⇧)))). Based on this result, Zhou [2014] provided a syntactic transformation from a DLP to an NLP by first applying the unfolding transformation on all the atoms, then shifting the resulting program to the NLP.

3 Eliminating Disjunctions by Restricted Unfolding

In this section, we show that a disjunctive program can be equivalently translated to a normal program by first applying the unfolding transformation only on "culprit" atoms, i.e., atoms that prevent the program from being HCF.

For a DLP ⇧, we denote

Intuitively, HC(⇧) specifies the set of atoms that prevent ⇧ to be HCF.

Now we provide the lemmas that draw a sketch of the proof for our main result.

Lemma 1 Let ⇧ be a DLP and E ✓ Atoms(⇧). Then

Lemma 2 Let ⇧ be a DLP, E ✓ Atoms(⇧), and L 2 Loop(remove(⇧↪E)). If L \ HC(⇧) = ; then LF (L↪ remove(⇧↪ E)) ⌘ LF (L↪ sh(remove(⇧↪ E))).

As discussed in Introduction, unfolding may introduce new head-cycles and hence increase the set of atoms in HC.

Example 1 (Continued) ¶b↪ c↪ e♦ is not a loop of ⇧1, while it is a loop of the program remove(⇧1↪ ¶a♦), then HC(remove(⇧1↪ ¶a♦)) = ¶b↪ e♦ while HC(⇧1) = ¶a↪ b♦.

For some DLP ⇧ and E ✓ Atoms(⇧), exponentially many loops can be introduced by unfolding and HC(remove(⇧↪ E)) can be greatly larger than HC(⇧).

Example 2 Consider the logic program⇧2:

Lemma 3 Let ⇧ be a DLP and E ✓ Atoms(⇧). Then for each L 2 Loop(remove(⇧↪ E)), either L \ E = ; or L = ¶a♦ for some a 2 E.

where n ≥ 1. Note that Loop(⇧2) = Sp2Atoms(⇧2) ¶¶p♦♦ [ ¶¶a↪ b♦♦, HC(⇧2) = ¶a↪ b♦. remove(⇧2↪ a) = (⇧2 ∩ ¶e a↪ d▷ b a▷♦) [ ¶b _ e c↪ d▷ b c▷ e b↪ d▷♦. For any nonempty set S ✓ ¶a1↪ ▷ ▷ ▷ ↪ an♦, S [ ¶b↪ d♦ is a loop of remove(⇧2↪ a). Then ♣Loop(remove(⇧2↪ a))♣ = 4+n+2n , ♣Loop(⇧2)♣ = 6+n, and HC(remove(⇧2↪ a)) = ¶b↪ d↪ a1↪ ▷ ▷ ▷ ↪ an♦.

From Theorem 1 and above lemmas, we get our main result. Theorem 4 For any DLP ⇧,

Then we can equivalently rewrite a DLP ⇧ to the NLP sh(remove(⇧↪ HC(⇧))).

Now we discuss some optimizations for the new rewriting.

Given a DLP ⇧ with n different atoms and m different rules, (the number of rules) ♣remove(⇧↪ a)♣ for an atom a is m+m2 in the worst case, ♣remove(⇧↪HC(⇧))♣ is O(m2n ), and ♣sh(remove(⇧↪HC(⇧)))♣ is O(n · m2n ). As proved in [Eiter et al., 2004], any answer-set-preserving rewriting of a DLP to an NLP must lead in general to an exponential blow-up, providing the polynomial hierarchy does not collapse. However, when ⇧ is "almost" HCF, the rewriting could be efficient. In particular, if ♣HC(⇧)♣ = k for a constant k, then ♣sh(remove(⇧↪ HC(⇧)))♣ is O(n·m2k ), which is polynomial for the size of ⇧, i.e., n and m.

We can further reduce the number of unfolded atoms by considering only special loops.

Firstly, HC(⇧) can be replaced by one of its subsets in the rewriting. For a DLP ⇧, we denote

Clearly, HC ⇤ (⇧) ✓ HC(⇧). From Theorem 1, if HC ⇤ (⇧) = ;, then AS(⇧) = AS(sh(⇧)), even when ⇧ is not HCF. So the class of HCF programs can be extended to HCF⇤ programs with HC ⇤ (⇧) = ;, for which shifting is answer-setpreserving. We have the following corollary of Theorem 4.

Corollary 5 For any DLP ⇧,

Secondly, based on the notions of elementary loops and proper loops, HC ⇤ (⇧) can be further reduced to some of its subsets in the rewriting.

Gebser et al. [2011] showed that not all loops are necessary for identifying the answer sets among the models of a DLP. They introduced the subclass elementary loops of loops, and refined Theorem 1 by considering elementary loops only. Later, Ji et al. [2015] introduced the subclass proper loops of elementary loops and refined Theorem 1 by considering a special form of loop formulas for proper loops only. As recognizing elementary loops and proper loops for DLPs are coNPcomplete, Ji et al. [2015] introduced weak elementary loops and weak proper loops which can be identified in polynomial time.

Based on these notions, we can further refine HC ⇤ (⇧) in the rewriting. For a DLP ⇧, we denote

HPL(⇧), HWEL(⇧), and HWPL(⇧) denote the sets specified by the definition of HEL(⇧) by replacing "elementary loop" with "proper loop", "weak elementary loop", and "weak proper loop", respectively. Then we have the following corollary of Theorem 4.

Corollary 6 For any DLP ⇧,

• = AS(sh(remove(⇧↪ HWPL(⇧))))▷

4 Reducing Loop Formulas for Computing Answer Sets of Rewritten Programs

From Theorem 1, answer sets can be identified from models of the program that satisfy loop formulas of all loops. In this section, we show that we only need to consider a subset of loops of an unfolded program, i.e., remove(⇧↪E) for a DLP ⇧ and E ✓ Atoms(⇧), for obtaining answer sets. This result could be beneficial for SAT-based answer set programming solvers, such as ASSAT [Lin and Zhao, 2004], cmodels [Giunchiglia et al., 2006], and clasp [Gebser et al., 2007], for computing answer sets of remove(⇧↪E) and sh(remove(⇧↪ E)).

We first provide a lemma to specify relations of loops and loop formulas between a DLP ⇧ and the unfolded program remove(⇧↪ a) for an atom a.

Lemma 4 Let ⇧ be a DLP and a an atom in ⇧. Then the following statements hold:

• ÷ ¶L ♣ L 2 Loop(⇧)↪ a ◁2 L♦ ✓ Loop(remove(⇧↪ a)).
• ÷ For any set L ✓ Atoms(⇧), if a 2 L then LF(L↪ ⇧) ⌘ LF (L↪ remove(⇧↪ a)).
• ÷ ¶L ∩ ¶a♦ ♣ L 2 Loop(⇧)♦ ∩ ; ✓ Loop(remove(⇧↪ a)).
• ÷ For any set L ✓ Atoms(⇧), if a ◁2 L then
• tr(⇧) ⊃ (LF(L↪ remove(⇧↪ a)) ⊃ LF(L↪⇧)), and
• (LF(L[ ¶a♦↪⇧) ^LF(L↪⇧)) ⊃ LF (L↪ remove(⇧↪ a)).

Given a DLP ⇧ and E ✓ Atoms(⇧), we denote

From Lemma 4, Loop⇤ (⇧↪ E) ✓ Loop(remove(⇧↪ E)). remove(⇧↪ E) may have loops that are not in Loop⇤ (⇧↪ E). For some DLPs, the size of Loop(remove(⇧↪E)) can be exponentially larger than the size of Loop⇤ (⇧↪ E).

The following theorem shows that, we only need to consider loops in Loop⇤ (⇧↪E) for identifying answer sets among the models of tr(remove(⇧↪ E)).

Theorem 7 Let ⇧ be a DLP and E ✓ Atoms(⇧). Then S 2 AS(remove(⇧↪ E)) iff S [ ¶≻p ♣ p ◁2 S♦ is a model of

Recalling Theorem 1, we can improve the computation of answer sets for remove(⇧↪E) on SAT-based answer set programming solvers by only considering loop formulas for loops in a subset of Loop(remove(⇧↪ E)).

Corollary 8 Let ⇧ be a DLP and E ✓ Atoms(⇧). Then S 2 AS(sh(remove(⇧↪ E))) iff S [ ¶≻p ♣ p ◁2 S♦ is a model of

Theorem 7 and Corollary 8 show that although our transformation to NLP may result in an exponential blow-up, there is not necessarily a blow-up in loop formulas for the computation. In particular, ♣Loop⇤ (⇧↪E)♣  ♣Loop(⇧)♣ for any set E ✓ Atoms(⇧), then the number of loops that need to be considered for computing answer sets of remove(⇧↪E) or sh(remove(⇧↪E)) is not larger than that of ⇧.

5 Approximating a DLP by Restricted Unfolding

In this section, we consider another application of the new rewriting for approximating a DLP ⇧ by an NLP. First, we specify the notion of approximation.

Definition 3 (Sound Approximation) A DLP ⇧⇤ is a (sound) approximation of a DLP ⇧, if AS(⇧⇤ ) ✓ AS(⇧).

The intuition behind the definition is that, when it is hard to compute answer sets of a DLP ⇧, we would like to construct an approximation ⇧⇤ of ⇧ so that ⇧⇤ can compute some answer sets of ⇧ easier. The approximation is sound in the sense that every computed answer set is an answer set of ⇧.

Definition 4 (Closed Sequence of Sound Approximations) A sequence of DLPs h⇧1↪ ▷ ▷ ▷ ↪⇧ni is a closed sequence of (sound) approximations of a DLP ⇧, if AS(⇧i) ✓ AS(⇧i+1) for each 1  i  n - 1, and AS(⇧n) = AS(⇧).

Intuitively, given a closed sequence of sound approximations of a DLP ⇧, we can construct an anytime algorithm by computing answer sets of ⇧i's one by one, which is expected to find better solutions the more time it keeps running. Eventually, the algorithm would return all answer sets of ⇧.

In the following, we specify a closed sequence of sound approximations of a DLP by restricted unfolding and shifting.

Lemma 5 For any DLP ⇧ and a 2 Atoms(⇧), AS(remove(sh(⇧)↪ a)) ✓ AS(sh(remove(⇧↪ a))).

Theorem 9 Let ⇧ be a DLP and E1 ✓ E2 ✓ HC(⇧). Then

AS(sh(⇧)) ✓ AS(sh(remove(⇧↪ E1))) ✓ AS(sh(remove(⇧↪ E2))) ✓ AS(⇧)▷

From Theorem 9, we can construct a closed sequence of sound approximations of a DLP.

Corollary 10 Let ⇧ be a DLP, HC(⇧) = ¶a1↪ ▷ ▷ ▷ ↪ an♦. Then

hsh(⇧)↪ sh(remove(⇧↪ ¶a1♦))↪ sh(remove(⇧↪ ¶a1↪ a2♦))↪ ▷ ▷ ▷ ↪ sh(remove(⇧↪ ¶a1↪ ▷ ▷ ▷ ↪ an♦))i

is a closed sequence of sound approximations of ⇧.

Example 1 (Continued) AS(sh(⇧1)) = ; and AS(⇧1) = AS(remove(⇧1↪ a)) = AS(sh(remove(⇧1↪ a))) = ¶¶a↪ b↪ c↪ d↪ e♦♦.

Now we provide an anytime algorithm (Algorithm 1) to compute answer sets of a DLP by using NLP solvers.

Algorithm 1: Computing answer sets of a DLP ⇧

1 H :=HC(⇧); 2 as := AS(sh(⇧)); 3 output as; // current computed answer sets of ⇧ 4 for each a 2 H do 5 ⇧ := remove(⇧↪ a); 6 as := AS(sh(⇧)); 7 output as; 8 return as;

We can apply the approaches discussed in previous sections to optimize Algorithm 1 as well. In particular, we can replace HC(⇧) by HC ⇤ (⇧) or HWEL(⇧) in the algorithm. We can also use the approach proposed in Section 4 to improve the computation of answer sets for sh(⇧).

Algorithm 1 provides an approach to compute an answer set of a DLP by calling NLP solvers. Janhunen et al. [2006] also provided such an approach. In their approach, a DLP ⇧ is first rewritten to an NLP Gen(⇧) to produce candidate models S, then another NLP Test(⇧↪ S) is constructed to check whether S is an answer set of ⇧. The rewriting proposed in [Janhunen et al., 2006] is different from our rewriting in the sense that AS(⇧) ✓ AS(Gen(⇧)), i.e., Gen(⇧) is not a sound approximation of ⇧, while we provide a closed sequence of sound approximations.

6 Some Experiments

We have implemented a program 1 for rewriting a DLP P to an NLP P n , where P n is a simplified program from sh(remove(P↪HC(P))) by removing redundancies like rules r with head(r) \ body+(r) 6= ; or body+(r) \ body-(r) 6= ;. By Theorem 4, AS(P) = AS(P n ). If the size of the NLP P n is similar to the size of the DLP P , it will be more efficient to compute answer sets of P n using NLP solvers than to compute answer sets of P using DLP solvers.

To corroborate this observation, we tested our program on some benchmarks constructed from Niemel¨a's [1999] encoding H of the Hamiltonian Circuit (HC) problem. Specifically, we constructed programs of the form Q = Q0 [H [G where H is Niemel¨a's encoding for the HC problem, G is the encoding of the graph for a given HC instance, and the program Q0 is given as the following:

where reached(1) is an atom in H and a, b are new atoms not appearing in H.

Our program will rewrite such a disjunctive program Q into a normal program Qn = Qn0 [ H [ G. It can be seen that Qn = sh(remove(Q↪HC(Q))). Here Qn0 is the program:

b reached(1)↪ not a▷ a reached(1)↪ not b▷ a reached(1)▷ b reached(1)▷

In Table 1, we compare the running times of computing an answer set of Q and Qn using solvers clasp and cmodels 2 . In the table, rand m k(t) stands for a class of randomly generated t graphs with m vertexes and k arcs. The numbers under "Q" refer to the average running times for computing an answer set of corresponding programs Q, using corresponding DLP solvers, i.e., clasp 3 (version 3.1.4) and cmodels 4 (version 3.8.5), and those under "Qn " refer to the average running times for computing an answer set of corresponding programs Qn , using corresponding NLP solvers, i.e., clasp and cmodels. As can be seen, for these programs, computing an answer set of Qn by NLP solvers is more efficient.

1 Our implementation is available on the web http://ss.sysu.edu.cn/%7ewh/dlp2nlp.html.

2 Our experiments were done on an Intel(R) Core(TM) i7-2600 3.40GHz CPU and 32GB RAM. The reported times are in CPU seconds as reported by Linux "/usr/bin/time" command.

3 The modern versions of clasp have built-in support for DLPs. http://www.cs.uni-potsdam.de/clasp/

4 http://www.cs.utexas.edu/users/tag/cmodels/

* When a solver could not compute an answer set of a program in 1800 seconds, we count the running time as 1800 seconds. We also report the number of such programs in the parentheses.

We also tested some benchmarks that were frequently used to evaluate performance of DLP solvers [Denecker et al., 2009; Gebser et al., 2013]. However, for most non-HCF DLPs P in these benchmarks, the size of P n is much larger than the size of P and as a result, our method failed to show advantage over direct use of DLP solvers.

7 Eliminating Disjunctions for First-order Programs on Finite Structures

In this section, we extend the new rewriting to non-ground programs with first-order answer set semantics on finite structures. We first review some basic notions.

In the following, we consider the first-order disjunctive logic programs [Ferraris et al., 2011], with similar syntactic forms as DLP programs. A distinction is made between predicates occurring only in rule bodies and the reminder predicates. A predicate P in a first-order DLP ⇧ is intensional (or IDB) if P occurs in head(r) for some r 2 ⇧, and extensional (or EDB) otherwise. We use P(⇧), PIDB(⇧), and PEDB(⇧) to denote sets of predicates, intensional predicates, extensional predicates occurring in ⇧ respectively. As with [Lee and Meng, 2008], we assume w.l.o.g. that ⇧ is in normal form without object constants occurring in rule heads.

We use first-order (ground) substitution, unifier, most general unifier (mgu) defined in the standard way. In contrast to grounded DLP, the answer sets of a first-order DLP is defined using first-order structures. In particular, a finite structureM is a tuple (D↪ cM1 ↪ ▷ ▷ ▷ ↪ cMm ↪ P M 1 ↪ ▷ ▷ ▷ ↪ P M n ), where D is a finite set called the domain of M, cMi 2 A (the interpretation of constant ci) (1  i  m), and P M j (the interpretation of a k-ary predicate symbol Pj) (1  j  n) a k-ary relation on D. We refer the readers to [Asuncion et al., 2012] for the definition of answer sets of first-order DLP on finite structures.

The answer set semantics of a first-order DLP on finite structures can be captured by first-order loop formulas [Chen et al., 2006; Lee and Meng, 2008] as well.

For a first-order DLP ⇧, the positive dependency graph of ⇧, written G⇧, is the infinite graph (V↪ E), where V is the set of atoms constructed from PIDB(⇧), (a↪ b) 2 E if there is a rule r 2 ⇧ and a substitution ✓ such that P(~t)✓ = a for some P (~t) 2 head(r) and Q(~t0 )✓ = b for some Q(~t0 ) 2 body+(r). A finite nonempty subset L of V is called a (first-order) loop of ⇧ if the subgraph of G⇧ induced by L is strongly connected. Specially, for each atom a 2 V , ¶a♦ is a loop of ⇧. We use Loop(⇧) to denote the set of loops of ⇧.

Given a loop L of a DLP ⇧ in normal form, we first rename variables in ⇧ so that no variables of ⇧ occur in L. Then the (first-order) external support formula of L for ⇧, denoted by ES(L↪⇧), is the following disjunction

The (first-order) loop formula of L in ⇧, denoted by LF(L↪⇧), is the universal closure of Va2L a ⊃ ES(L↪⇧)▷ We use LF(⇧) to denote the set of all loop formulas in ⇧.

Theorem 12 (Proposition 4 in [Lee and Meng, 2008]) Let ⇧ be a DLP and M a finite structure. M is an answer set of ⇧ if and only if M is a model of ¶tr(⇧)♦ [ LF (⇧).

Given a first-order DLP ⇧, the shifting result sh(⇧) is defined in the same way as in the propositional case. Every answer set of sh(⇧) is also an answer set of ⇧, but the converse is not true in general. Similarly, a first-order DLP ⇧ is called "Head-Cycle-Free" (HCF), if there is no loop L, rule r in ⇧, and substitution ✓ such that ♣L \ head(r)✓♣ > 1.

Based on the progression semantics of answer sets [Zhou and Zhang, 2011], Zhou [2015] provided the following proposition.

Proposition 1 Let P be an HCF first-order DLP. Then, AS(sh(⇧)) = AS(⇧).

Definition 5 (Elementary unfolding in first-order case)

Given two rules r1 and r2 (with suitable variable renaming), there are atoms a 2 head(r1) and b 2 body+(r2) such that a and b are unifiable with an mgu ✓. The rule obtained by elementary unfolding r2 at b using r1 at a, denoted by unfold(r1↪ r2↪ a↪ b), is the rule r such that head(r) = ((head(r1) ∩ ¶a♦) [ head(r2))✓ and body(r) = (body(r1) [ (body(r2) ∩ ¶b♦))✓.

Let ⇧ be a DLP, r a rule in ⇧, and b an atom in body+(r). We denote Uset(⇧↪ r↪ b) to be the set of rules constructed by the following procedure:

S0 := ¶(r0 ↪ a0 ) ♣ r0 2 ⇧↪ there is an atom a0 2 head(r0 ) such that a0 and b are unifiable ♦;

i := 0;

✓ := the mgu that a0 and b are unfiable with; Si+1 := Si+1[ ¶(r00 ↪ a⇤ ✓) ♣ (r0 ↪ a⇤ ) 2 Si↪ a⇤ 6= a0 ♦; i := i +1;

[Gergatsoulis, 1997] showed that the procedure would always terminate. We denote remove(⇧↪ r↪ b) = (⇧ ∩ ¶r♦) [ Uset(⇧↪ r↪ b). From Theorem 13 in [Gergatsoulis, 1997], we have the following proposition.

Proposition 2 Let P be a DLP, r a rule in ⇧, and b an atom in body+(r). Then AS(⇧) = AS(remove(⇧↪ r↪ b)).

Let ⇧ be a DLP and a an atom in head(r) for some r 2 ⇧. We denote remove(⇧↪ a) to be a set of rules constructed by the following procedure:

while there is a rule r 2 R and b 2 body+(r) such that a and b are unifiable

remove(⇧↪ a) := R.

Note that, by choosing different rules and corresponding atoms in the procedure, remove(⇧↪ a) would return different programs. However, they are equivalent in the sense of having the same sets of answer sets.

The above procedure may not terminate for some DLPs due to the unfolding process. Zhou [2015] identified a class of first-order DLPs called choice-bounded and showed that the process of applying the unfolding transformation when it is possible would always terminate for choice-bounded DLPs. Then for a choice-bounded DLP ⇧, the above procedure terminates and remove(⇧↪ a) always exists.

Theorem 13 Let ⇧ be a DLP, a an atom in head(r) for some r 2 ⇧, and remove(⇧↪ a) exists. Then AS(⇧) = AS(remove(⇧↪ a)).

Given a DLP ⇧, we denote head(⇧) = ¶a ♣ a 2 head(r) for some r 2 ⇧♦. Let ⇧ be a DLP and a set A ✓ head(⇧). We denote remove(⇧↪ A) to be a set of rules constructed by the following procedure:

for each a 2 A

Corollary 14 Let P be a DLP, A ✓ head(⇧), and remove(⇧↪ A) exists. Then AS(⇧) = AS(remove(⇧↪ A)).

Now we extend our rewriting to first-order DLPs. For a DLP ⇧, we denote

HC(⇧) = ¶a ♣ a 2 head(⇧)↪ there exists r 2 ⇧, a loop L of ⇧, and a substitution ✓ such that ♣L \ head(r)✓♣ > 1, a 2 head(r) and a✓ 2 L♦▷

We provide the following lemma to draw a sketch of the proof for the main result.

Lemma 6 Let ⇧ be a DLP, A ✓ head(⇧), and remove(⇧↪ A) exists. Then the following statements hold:

• ÷ A finite structure M satisfies LF(⇧) and tr(⇧) if and only if M satisfies LF(remove(⇧↪A)) and tr(remove(⇧↪A)), where LF(⇧) = ¶LF(¶a0 ♦↪⇧) ♣ a0 = a✓ for some a 2 A and substitution ✓♦.
• ÷ For each L 2 Loop(remove(⇧↪A)), if there does not exist a substitution ✓ such that L \ HC(⇧)✓ 6= ;, then LF(L↪ remove(⇧↪A)) ⌘ LF (L↪ sh(remove(⇧↪ A))).
• ÷ for each L 2 Loop(remove(⇧↪A)), either there does not exist a substitution ✓ with L \ A✓ 6= ; or L = ¶a♦ for some a0 2 A and substitution σ with a0σ = a.

Theorem 15 Let ⇧ be a DLP and remove(⇧↪ HC(⇧)) exists. Then AS(⇧) = AS(sh(remove(⇧↪ HC(⇧)))).

Asuncion et al. [2012] provided a solver of first-order NLPs by translating them to first-order sentences on finite structures. From Theorem 15, we can use the solver to compute answer sets of some first-order DLPs.

8 Conclusion

In this paper, we provide a new answer-set-preserving rewriting of a DLP to an NLP by first apply the unfolding transformation on "culprit" atoms, i.e., atoms that prevent the program from being HCF, then shift the resulting program. This result shows that the complexity penalty for extending NLPs by including disjunctive rules is closely tied to these "culprit" atoms. Hence, different from other transformations for eliminating disjunctions in literature, our rewriting is efficient for "almost" HCF programs, i.e., DLPs that have only a few "culprit" atoms. Later, we show that the computation of answer sets for a rewritten program can be improved by reducing the number of loops that need to be considered and the size of these loops is not larger than that of the original program. This result shows that although our transformation to NLP may result in an exponential blow-up, there is not necessarily a blow-up in loop formulas for the computation. Based on the new writing, we provide an anytime algorithm to compute answer sets of a DLP by calling NLP solvers. At last, we extend the rewriting to non-ground answer set programs on finite structures.

9 Acknowledgments

We thank Xiaoping Chen and his research group for their useful discussions. Jianmin Ji's research was partially supported by the National Natural Science Foundation of China under grant 61175057, the National Natural Science Foundation for the Youth of China under grant 61403359, as well as the USTC Key Direction Project and the USTC 985 Project. Hai Wan's research was in part supported by the National Natural Science Foundation of China under grant 61573386, Natural Science Foundation of Guangdong Province under grant 508257922126, Guangdong Province Science and Technology Plan projects under grant 509208496103, and Sun Yatsen University Young Teachers Cultivation Project under grant 16lgpy40. This work was also partially supported by ARC under grant DP130102302.