# completion_of_disjunctive_logic_programs__97cb4776.pdf

Completion of Disjunctive Logic Programs

Mario Alviano and Carmine Dodaro Department of Mathematics and Computer Science, University of Calabria, Italy

{alviano, dodaro}@mat.unical.it

Clark s completion plays an important role in ASP computation: it discards unsupported models via unit resolution; hence, it improves the performance of ASP solvers, and at the same time it simplifies their implementation. In the disjunctive case, however, Clark s completion is usually preceded by another transformation known as shift, whose size is quadratic in general. A different approach is proposed in this paper: Clark s completion is extended to disjunctive programs without the need of intermediate program rewritings such as the shift. As in the non-disjunctive case, the new completion is linear in size, and discards unsupported models via unit resolution. Moreover, an ad-hoc propagator for supported model search is presented.

1 Introduction Answer Set Programming (ASP) is a well established declarative language for knowledge representation and reasoning [Niemelä, 1999; Marek and Truszczy nski, 1999; Lifschitz, 2002; Baral, 2003; Gelfond and Kahl, 2014]. In fact, ASP programs are interpreted according to stable model semantics, where each stable model provides a plausible scenario or solution to the encoded problem. The original definition of stable model, applicable to programs with atomic heads, was soon extended to handle programs with disjunctive heads [Przymusinski, 1991]. In the subsequent years, relevant properties regarding stable model semantics for disjunctive programs were discovered, and discussed in the literature. In particular, broad classes of programs with good computational properties were identified: stable model existence belongs to the first level of the polynomial hierarchy for head cycle free [Ben-Eliyahu and Dechter, 1994], one level below than the general case. Even more relevant, the notion of tightness was extended to disjunctive programs [Fages, 1994; Erdem and Lifschitz, 2003; Lee and Lifschitz, 2003], proving that stable models actually coincide with supported models for a huge class of programs.

This work was partially supported by MIUR under PON project Ba2Know (Business Analytics to Know) Service Innovation - LAB , No. PON03PE_00001_1, and by Gruppo Nazionale per il Calcolo Scientifico (GNCS-INd AM).

The notion of support is intuitive, and expected to be satisfied by any stable model of the input program: a model is supported if for each true atom there is a rule whose body is true, and whose head is satisfied only by the atom itself. Such a notion can be enforced by a transformation known as Clark s completion [Clark, 1977] possibly preceded by another transformation known as shift [Ben-Eliyahu and Dechter, 1994], which provide a concrete strategy for computing stable models of tight programs by means of efficient SAT solvers. Moreover, since stable models are expected to be supported models as well, shift, completion and SAT solving are usually embedded in modern ASP solvers in combination with other techniques such as unfounded set inference via source pointers [Simons et al., 2002], and stability check via SAT oracle calls [Leone et al., 1997].

This paper highlights a source of inefficiency in current ASP solvers: the shift of a rule is quadratic in the number of atoms occurring in its head. Actually, this quadratic blow up was underestimated so far because the size of disjunctive heads is often bounded by the input program, which means that the data complexity is not affected. However, recent progresses in the formalization of the input language of GRINGO [Gebser et al., 2015a], a widely used ASP grounder, mentioned conditional literals, a construct that essentially allows to specify unbounded disjunctions. As a consequence, the quadratic blow up may occur for fixed non-ground programs.

Minimal Hitting Set computation is a prominent example of a problem that can be naturally encoded in ASP by means of unbounded disjunctions. Given a collection C of subsets of a set S, a hitting set for C is a subset S0 of S such that S0 contains at least one element from each subset in C. A hitting set S0 for C is minimal if there is no S00 S0 such that S00 is a hitting set for C. Hitting sets are widely used in artificial intelligence. For example, it is wellknown that minimal hitting sets provide a duality relationship between Minimal Unsatisfiable Subsets (MUSs) and Minimal Correction Subsets (MCSs) [Liffiton and Sakallah, 2008; Ignatiev et al., 2015]. A natural encoding for this problem in the input language of GRINGO is the following:

s0(X) : in(X, Y ) : c(Y ). (1) where the database contains c(y) if set y belongs to C, and in(x, y) if x 2 S belongs to y 2 C. The output of GRINGO is the propositional program comprising, for all y 2 C, a rule of the following form: W

x2y s0(x) .

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16)

Empirical evidence of the inefficiency of currently implemented algorithms for processing the above program, and any other program containing at least one rule whose head size is not negligible, motivates a more in depth analysis of the problem. In particular, new techniques to handle rules with unbounded heads are required in order to overcome the limits of the shift. As proved in Section 3, simple arguments such as bounding head sizes by means of auxiliary atoms would solve the quadratic blow up of the shift, but would also destroy the link between stable models of the original program and supported models of the rewritten program. Even worse, a single rule with three or more atoms in its head would be sufficient to destroy other desirable computational properties such as tightness and head cycle freeness.

The proposed solution is thus to rethink the completion in the disjunctive case. As in the original completion, the new technique consists in building a CNF whose models are one-to-one with the supported models of the input program. Moreover, and even more important from the computational point of view, all inferences commonly implemented by ASP solvers for supported model search are preserved by the proposed transformation. As an additional contribution, a specific propagator for handling support inferences in disjunctive rules is described and implemented. In the tested instances, the new completion and the propagator provide a sensible performance gain to the solver WASP [Alviano et al., 2014].

2 Background Let A be a fixed, countable set of (propositional) atoms, including ?. A literal is either an atom p, or its negation p. Let denote the complement of , i.e., p := p, and p := p, for all p 2 A. For a set S of literals, S := { | 2 S}, S+ := S \ A, and S := S \ A.

A (disjunctive) rule r has the following form:

p1 _ _ pm 1 n (2)

where m 1, n 0, p1, . . . , pm are distinct atoms, and 1, . . . , n are distinct literals. Define B(r) := { 1, . . . , n}, and H(r) := {p1, . . . , pm}, referred to as the body and the head of r, respectively. A program is a set of rules. Let At( ) denote the set of atoms occurring in , and heads( , p) be the set of rules in whose head contains p.

A CNF Γ is a set of clauses, where each clause ' is a set of literals. For n 0, and 0, . . . , n being literals, formula

0 $ 1 n (3)

is a compact representation of the following clauses: { 0} [ { i | i 2 [1..n]}; { 0, i}, for all i 2 [1..n]. Similarly,

0 $ 1 _ _ n (4)

is a compact representation of the following clauses: { 0, i}, for all i 2 [1..n]; { 0} [ { i | i 2 [1..n]}. (For n = 0, the connective or _ on the right of $ will be specified in order to avoid ambiguities.)

For being a set, a rule, a program, or a CNF, let | | denote the size of , i.e., the number of atoms occurring in , where each occurrence count 1. Note that formula (3) has size (n + 1) + 2 n = 3 n + 1; the same for (4).

A (partial) interpretation is a set I of literals containing ?; I is consistent if I+ \ I = ;, and total for a program or CNF if I+ [ I = At( ). Let V be a set of atoms. The restriction of I to V is I|V := I \ (V [ V ). Two sets I, J of interpretations are equivalent wrt a set V of (visible) atoms, denoted I V J, if both |I| = |J|, and {I|V | I 2 I} = {J|V | J 2 J} (where the first condition is important for counting and enumeration of models [Janhunen, 2006]).

Relation |= is defined as follows: for r of the form (2), I |= r if H(r) \ I 6= ; whenever B(r) I; for a program , I |= if I |= r for all r 2 ; for a CNF Γ, I |= Γ if ' \ I 6= ; for all ' 2 Γ. For being a program or a CNF, a model of is a total, consistent interpretation I such that I |= . A model I is possibly referred to by the set I+ of its positive literals. Let Mod( ) denote the set of models of . For a program , I is supported in if for all p 2 I there is a rule r such that B(r) I, and H(r) \ I = {p}. A supported model of is a model of that is supported in . Let Sup Mod( ) denote the set of supported models of . Example 1. The models of the following program 1:

a _ b _ c b a c a

are {c}, {a, b}, {c, b}, and {a, b, c}. The first is the only supported model of 1. Consider now the following CNF Γ1:

a1 $ b c b2 $ a a $ a1

b1 $ a c c3 $ a b $ b1 _ b2

c1 $ a b c $ c1 _ c3

Its only model is {c, c1, c3}, and therefore Mod(Γ1) At( ) Sup Mod( 1). A model I of a program is stable if it satisfies the following stability condition: there is no J+ I+ such that J |= I, where I is the reduct obtained from by first removing each rule r such that B(r) \ I 6= ;, and then removing all negative literals [Przymusinski, 1991]. Let St Mod( ) be the set of stable models of . It is well known that St Mod( ) Sup Mod( ) for any program , while St Mod( ) = Sup Mod( ) does not hold in general. Actually, the fact that St Mod( ) Sup Mod( ) can be used in practice by ASP solvers: the stability condition has to be checked only on supported models; moreover, there is a relevant class of program, known as tight [Lee and Lifschitz, 2003] and defined below, for which St Mod( ) = Sup Mod( ) holds.

The (positive) dependency graph of , denoted G , has vertices At( ), and arcs from any p 2 H(r) to any q 2 B(r)+, for all r 2 . is tight if all (strongly connected) components of G are singleton. A broader class is referred in the literature as head cycle free (HCF) programs [Ben-Eliyahu and Dechter, 1994], defined next, and particularly relevant for computational complexity: checking St Mod( ) 6= ; is known to be P

2 -complete, but only NPcomplete if is HCF. is HCF if there is no rule r 2 of the form (2) such that pi, pj, for some 1 i < j m, belong to the same component of G . Example 2. Program 1 from Example 1 is tight, and therefore {c} is its only stable model. Indeed, ; is not a model of {c}

1 = {a _ b _ c , c }.

Model search usually takes advantage of inference rules that iteratively add inferred literals to an interpretation I. Given a CNF Γ, if there is a clause ' 2 Γ such that ' \ I = { }, then is inferred by unit resolution. Given a program , if there is a rule r 2 such that both B(r) I, and H(r) \ I = {p}, then p is inferred by forward chain; if there is a rule r 2 such that both H(r) I , and B(r) \ I = { }, then is inferred by backward chain.

Supported model search for a program can use more inference rules. Let psup( , p, I) denote the set of possible supports for p, i.e.,

{r 2 heads( , p) | H(r) \ I {p}, B(r) \ I = ;}. (5) If there is an atom p 2 At( ) such that psup( , p, I) = ;, then p is inferred by lack of support. If there is an atom p 2 I+ such that psup( , p, I) = {r}, then literals in B(r)[ H(r) \ {p} are inferred by last support.

Let unit(Γ, I) be the set of literals inferred by unit resolution on Γ and I; let unit (Γ, I) be the limit of I0 := I, Ii+1 := Ii [ unit(Γ, Ii), for all i 0. Let sinf ( , I) be the set of literals inferred by all inference rules on and I, i.e., forward and backward inference, and last and lack of support; let sinf ( , I) be the limit of I0 := I, Ii+1 := Ii [ sinf ( , Ii), for all i 0. A CNF Γ is inference preserving wrt a program , denoted Γ winf , if for all consistent interpretations I such that I At( )[At( ) the following conditions are satisfied: Let I0 := sinf ( , I), and I00 := unit (Γ, I); (i) I0 I00; (ii) if (I0)+[(I0) = At( ), then (I00)+ [ (I00) = At(Γ). Intuitively, (i) guarantees that all inferences on are covered by unit resolution on Γ, and (ii) ensures that truth values of atoms in Γ are implied by truth values of atoms in . Example 3. Γ1 and 1 from Example 1 satisfy Γ1 winf 1. For example, for I = { a}, I0 is { a, c, b} (c is inferred by forward chain, and b by lack of support). In this case, I00 is { a, a1, c3, c, b1, b2, b, c1}, and condition (i) is satisfied. Also note that I0 and I00 satisfy condition (ii): For I = {a}, I0 is inconsistent (b is inferred by forward chain, and then a by lack of support); in this case, I00 is inconsistent as well (and contains b, and a). Stable model search is usually implemented by combining (supported) model search with other techniques widely acknowledged in ASP computation, i.e., unfounded set inference via source pointers [Simons et al., 2002], and stability check via SAT oracle calls [Leone et al., 1997]. These techniques are out of the scope of the paper. The next section is thus mainly focused on the computation of supported models.

3 Computation Supported models of programs without disjunction can be computed by means of the so-called Clark s completion [Clark, 1977]. Let be a program without disjunction. The completion of , denoted comp( ), is the set of clauses

1 $ 1 n (6) for all r 2 of the form (2) with m = 1, where pr

1 is a fresh atom (true if and only if r is a support of p1), together with

r2heads( ,p)

for all p 2 A. Moreover, two other strengths of completion are that inferences are preserved, and the construction is linear in size. Proposition 1. If is a program without disjunction, then:

1. Mod(comp( )) At( ) Sup Mod( );

2. comp( ) winf ; 3. |comp( )| 2 O(| |). Example 4. Let 2 be the following program:

a b c b a b a c c a c a b

Its only supported model is {c}, and its completion comp( 2) is Γ1 from Example 1, whose only model is {c, c1, c3}. As observed in Example 3, Γ1 winf 2. In order to apply completion to programs in general, a transformation known as shift is first applied to the input program , so to obtain a program shift( ) with the same supported models. Formally, let shift( ) be the program comprising rules

j2[1..n],j6=i

pj 8i 2 [1..m] (8)

for all r 2 of the form (2). The strength of the shift is to preserve both supported models and inferences. On the other hand, the construction is not linear, but quadratic in size. Proposition 2. If is a program, then:

1. Sup Mod(shift( )) A Sup Mod( ), and therefore Mod(comp(shift( ))) At( ) Sup Mod( );

2. comp(shift( )) winf ; 3. |shift( )| 2 O(| |2), so |comp(shift( ))| 2 O(| |2); 4. comp( ) = comp(shift( )) if is disjunction-free. Example 5. Program 2 from Example 4 is shift( 1). Point 3 of Proposition 2 highlights a weakness of shift. Hence, an interesting question is whether a different strategy to avoid the quadratic blow up of the shift can be obtained when the computational task is to compute stable models, not just supported models. Actually, it is sufficient to add auxiliary atoms in order to rewrite the input program into a new program 0 whose head size is bound to 2. However, since such auxiliary atoms are essentially Tseitin s variables, implications in both directions have to be added to the program, thus introducing dependencies that are likely to deteriorate the performance of a solver. In more detail, auxiliary atoms tr

1, . . . , tr

m will be used to compactly represent subformulas in rules of the form (2). The normalization of , denoted norm( ), is the program comprising the following rules:

1 1 n (9) tr

i pi 8i 2 [2..m] (10) tr

i+1 8i 2 [2..m 1] (11) pi _ tr

i 8i 2 [1..m 1] (12) pm tr

m (13) for all r 2 of the form (2), where tr

1, . . . , tr

m are fresh atoms.

Theorem 1. If is a program, then:

1. St Mod(norm( )) At( ) St Mod( );

2. |norm( )| 2 O(| |); 3. Sup Mod(norm( )) 6 At( ) Sup Mod( ), and comp(shift(norm( ))) 6winf are possible; 4. if contains some rule r such that |H(r)| 3, then

norm( ) is not HCF. Example 6. The normalization norm( 1) of program 1 from Example 1 is the following program:

Its only stable model is {c, t1

1}, and therefore St Mod(norm( 1)) At( 1) St Mod( 1). On the other hand, {t1

2, b} is a supported model of norm( 1), while {b} is not a supported model of 1. Also note that norm( 1) is not HCF, as b, t1

3 belong to the same component of Gnorm( 1). Points 3 4 of Theorem 1 suggest that the weakness highlighted by point 3 of Proposition 2 may be better circumvented by directly extending completion to the disjunctive case. Hence, auxiliary atoms pr

i will be used with the same meaning of the disjunction-free case, i.e., rule r of the form (2) supports atom pi, for i 2 [1..m]. However, since m may be greater than 1, other atoms occurring in the head of r have to be taken into account. Additional auxiliary atoms will be thus used, and in particular: sr

i , true if and only if rule r may support pi, for i 2 [1..m]; dr

i , true if and only if the disjunction pi _ _ pm is true, for i 2 [2..m].

The completion of a (disjunctive) program , denoted comp_( ), is the set of clauses

i $ pi _ dr

i+1 8i 2 [2..m 1] (14) dr

m $ pm if m 2 (15) sr

1 $ 1 n (16) sr

i 1 pi 1 8i 2 [2..m] (17) pr

i+1 8i 2 [1..m 1] (18) pr

for all r 2 of the form (2), together with (7) for all p 2 At( ). Note that (15) defines dr

m as an alias of pm. Similarly, (19) defines sr

m as an alias of pr

m. It turns out that dr

m could be simplified in the above construction, but they are left to ease the reading. Even more important, note that for m = 1 the above equations essentially give (6): only (16) and (19) are used in this case, and (16) is precisely (6) if sr

1 is replaced by its alias pr

1. Theorem 2. If is a program, then:

1. Mod(comp_( )) At( ) Sup Mod( );

2. comp_( ) winf ; 3. |comp_( )| 2 O(| |); 4. comp( ) = comp_( ) if is disjunction-free.

Example 7. The completion of program 1 from Example 1 is the following CNF comp_( 1):

2 b a1 $ s1

2 b2 $ a a $ a1

3 c3 $ a b $ b1 _ b2

3 c $ c1 _ c3

Its only model is {c, s1

2, a1, b1, a, s1

2, b2, b, s1

3, c1, c3}, and therefore Mod(comp_( 1)) = Sup Mod( 1). As for inferences, for I = { a}, sinf ( 1, I) is { a, c, b}, and unit (comp_( 1), I) is { a, a1, d1

2, c3, c, d1

3, b1, b2, b, s1

3, c1}. Conditions (i) (ii) of inference preserving are satisfied. Moreover, for I = {a}, sinf ( 1, I) and unit (comp_( 1), I) are inconsistent.

4 Implementation The completion for disjunctive programs has been implemented in WASP, an open source ASP solver previously applying completion after shifting the input program. In the new version, the input program is possibly simplified after its parsing, and its completion comp_( ) is computed. If necessary, other data structures are computed as it was done before. This is the case, for example, of non-tight components, for which source pointers are used, and of non-HCF components, for which stability checks are obtained via SAT oracle calls.

ASP solvers may also take advantage of other propagators, i.e., efficient data structures that essentially provide a compact representation of a set of clauses. In particular, in WASP, aggregates are handled by pseudo-Boolean constraints of the following form:

w1 1 + + wn n k (20) where n, w1, . . . , wn, k are positive integers, and 1, . . . , n are literals. Intuitively, the above constraint compactly represents all clauses of the form C { 1, . . . , n} such that P

i2[1..n], i /2C wi < k. Efficient data structures are thus employed to extend unit resolution: for all i 2 [1..n], i is inferred from (20) if P

j2[1..n],j6=i, j /2I wj < k, i.e., if the sum of the integers associated with true and undefined literals different from i is smaller than k. Note that the propagator has to receive notifications only for literals j (j 2 [1..n]) whose complement is added to the current interpretation. Example 8. Literal c1 is inferred by the following constraint:

1 + a + b + c + a1 + b1 + c1 2 if the current interpretation is {s1

1, a, a1, c, b, b1}. A new propagator implementing all the inference rules for supported model search described in Section 2 has been implemented in WASP. The propagator actually combines ad-hoc data structures with a few clauses, and one pseudo Boolean constraint. The general idea is to use auxiliary atoms sr

1, . . . , pr

m (as in comp_) for each rule r of the form (2), and to compactly represent the following clauses:

j} 8j 2 [1..m] (21)

j} 8i 2 [1..m], 8j 2 [1..m], i 6= j (22)

i } [ {pj | j 2 [1..m], j 6= i} 8i 2 [1..m] (23)

together with (16). Moreover, clauses of the form (7) are added for each p 2 At( ). In more detail, (21) (22) are handled by storing two vectors, vr

0 := [p1, . . . , pm, sr

1, . . . , pr

m]; when the i-th literal of vector vr

k (k 2 [0..1]) is added to the current interpretation, the complement of each literal in position different from i of vr

1 k is inferred. Clauses from (23), instead, are handled by adding the following pseudo-Boolean constraint:

1 + p1 + + pm + pr

Indeed, since {pi, pr

i } belongs to (7), whenever pi is added to the current interpretation, pr

i is added as well. Thus, both (23) and (24) satisfy the following conditions: if p1, . . . , pm are false, then sr

1 is inferred; if p1, . . . , pi 1, pi+1, . . . , pm, for some i 2 [1..m], and sr

1 is true, then pi and pr

i are inferred; no inference is done in the remaining cases. Example 9. The disjunctive rule of program 1 from Example 1 (i.e., a _ b _ c ) is handled by the following vectors:

0 = [a, b, c, s1

1 = [a1, b1, c1]

by clause {s1

1}, and by the pseudo-Boolean constraint reported in Example 8. The remaining rules are handled as in comp( 1). Hence, the clauses defining a, b, c, b2, and c3 from Example 1 are also added. Transformation comp_ has been also implemented in an external tool producing DIMACS output in the style of LP2SAT [Janhunen and Niemelä, 2011]. Finally, the normalization norm introduced in Section 3 has been implemented in an external tool whose input and output conform to the numeric format of GRINGO.

5 Experiment The impact of the new techniques proposed in this paper was assessed empirically on three benchmarks: (i) instances from ASP Competitions containing choice rules easily replaceable by unbounded disjunctions; (ii) instances of Minimal Hitting Set downloaded from http://research.nii.ac.jp/~uno/ dualization.html; (iii) single rule

p(X) : X = 1..n.

i.e., the symbolic version of program {W

x2[1..n] p(xi) } for increasing values of constant n 1. The experiment was run on an Intel Xeon CPU 2.4 GHz with 16 GB of RAM. Time and memory were limited to 600 seconds and 15 GB. The tested solvers are WASP, CLASP 3.1.3 [Gebser et al., 2015b], and GLUCOSE 4.0 [Audemard and Simon, 2009].

Concerning the first benchmark, the tested encodings are Sokoban, Solitaire, Visit All and Weighted Sequence Problem. The number of instances solved by WASP rises from 74 to 79 when shift +comp is replaced by comp_. The performance achieved by using the propagator is similar, with 78 solved instances. These are good results if compared with CLASP: 80 instances are solved in the allotted time when the original encodings based on choice rules are used (74 when choice rules are replaced by disjunctions). On the other hand, on the tested instances already norm provides a sensible performance gain to shift +comp, even not reaching the same performance of comp_: WASP solves 77 instances, and CLASP 78.

80 90 100 110 120 130 140 150

Execution time (s)

Number of instances

wasp (shift+comp) lp2sat+glucose (shift+comp)

clasp (shift+comp) normalization+wasp (shift+comp) normalization+clasp (shift+comp)

wasp (compv) compv+glucose compv+clasp wasp (propagator)

0 200 400 600

wasp (compv)

wasp (shift+comp)

0 200 400 600

compv+glucose

lp2sat+glucose

0 200 400 600

wasp (propagator)

wasp (shift+comp)

Figure 1: Performance on Minimal Hitting Set.

As for the second benchmark, the tested encoding is program (1). The execution time is plotted in Figure 1(a). It can be observed that the performance of both WASP and CLASP is affected negatively by the transformation norm. On the other hand, replacing shift +comp by the new transformation comp_ provides a sensible performance gain to WASP, which can be also observed for CLASP on hard instances; for WASP, an instance by instance comparison of shift +comp and comp_ is plotted in Figure 1(b), where the majority of the points are below the diagonal, indicating that comp_ is faster than shift+comp in the majority of the tested instances. The benefit of adopting comp_ is also confirmed by the performance of GLUCOSE, which improves considerably when comp_ replaces the shift +comp transformation applied by LP2SAT; an instance by instance comparison is plotted in Figure 1(c), where almost all points are below the diagonal. Finally, the best performance is achieved by WASP with the propagator; Figure 1(d) highlights that the propagator has an advantage over shift +comp in all tested instances.

The last benchmark in the experiment highlights how the quadratic blow up due to shift may kill the computation of ASP solvers already before starting the actual stable model search procedure. Indeed, as it can be observed in Figure 2, the tested solvers cannot process disjunctions of size 30K in the allotted memory when shift +comp is used. On the other hand, the amount of memory required by the other techniques discussed in this paper is linear, as expected.

6 Related Work Supported model search is a significant part in the most frequent computational task of ASP solving, that is, computing

0 100 200 300 400 500 600 700 800 900 1000

Memory consumption (MB)

Size of disjunction (thousands)

wasp (shift+comp) lp2sat+glucose (shift+comp)

clasp (shift+comp) normalization+wasp (shift+comp) normalization+clasp (shift+comp)

wasp (compv) compv+glucose compv+clasp wasp (propagator)

Figure 2: Memory consumption to handle long disjunctions.

stable models of an input program. When the input program contains disjunctive heads, many efficient ASP solvers implement all inference rules of supported model search via unit resolution on the CNF obtained by applying shift+comp. For example, CLASP 3 [Gebser et al., 2015b], CMODELS 3 [Lierler, 2005], and WASP 2 [Alviano et al., 2015a] implement this strategy. As a consequence, and since unbounded disjunctions were already used in the literature (for example in Encoding 3 of [Abseher et al., 2015]), these excellent ASP solvers are affected by the quadratic blow up highlighted by the experiment reported in Section 5, and can be easily improved by replacing shift +comp with the translation comp_ introduced in this paper.

Technically, CMODELS 3 implements support inferences by means of an extension of Clark s completion that can be directly applied to disjunctive logic programs, and whose output is a set of propositional formulas [Lee and Lifschitz, 2003]. In more detail, given a program , CMODELS 3 builds an implication

1 n ! p1 _ _ pm (25) for each rule r 2 of the form (2), and an implication

r2heads( ,p)

for each atom p 2 At( ). As a first observation, the above construction is quadratic in size because of (26). Moreover, note that replacing the implication with an equivalence in (26), and rewriting it into an equi-satisfiable CNF by the Tseitin s transformation, would result into comp(shift( )). In the above transformation, instead, the implication is sufficient because of (25), which however has the side effect of introducing more Tseitin s variables during the computation of an equi-satisfiable CNF.

It is an interesting fact that the quadratic blow up in the implementation of support inferences for disjunctive logic programs does not affect DLV [Alviano et al., 2010], and WASP 1 [Alviano et al., 2013], which essentially take advantages of a propagator for this task. However, their propagators have fundamental differences with the propagator presented in Section 4. First of all, DLV does not implement conflict learning,

which is instead supported by WASP and by its propagators: in case of conflict, clauses compactly represented by propagators are possibly provided to the learning procedure, which is therefore the same of CDCL-based SAT solvers [Silva and Sakallah, 1996]. Conflict learning is implemented by WASP 1 as well, but with a completely different approach: the learning procedure is properly adapted to handle all inference rules of stable model search, and is therefore difficult to maintain and optimize.

For non-tight programs, support inferences are not sufficient to compute stable models. For these programs, unfounded set inference is often implemented by means of source pointers [Simons et al., 2002], which essentially enforce acyclicity in supporting rules. The implementation of source pointers requires notifications for variations of the possible supports of atoms in non-tight components, which are easy to obtain by observing the truth values of atoms of the form pr. Moreover, for non-HCF programs, stability of models is checked by means of calls to co NP-oracles [Leone et al., 1997]. In particular, CLASP 3 builds a CNF for checking the absence of unfounded sets in the model [Gebser et al., 2013], which was observed to be quadratic in size and motivated the introduction in WASP 2 of a CNF of linear size for checking minimality of the model for the program reduct [Alviano et al., 2015b]. The completion for disjunctive programs can be combined with these two techniques.

Finally, CLASP 3 implements the so-called componentwise shift in case of non-HCF programs [Drescher et al., 2008]: head atoms belonging to the same component are not shifted, and the completion of the resulting program is computed by introducing additional Tseitin s variables for non-atomic heads. When all disjunctive rules contain atoms from the same component, the component-wise shift is not affected by the quadratic blow up of the shift. On the other hand, support inferences are not preserved in general, which is a weakness in comparison to the completion for disjunctive programs proposed in this paper.

7 Conclusion Support inferences play an important role in stable model search. ASP solvers take advantage of SAT solving to handle this computational task. The CNF built for this purpose is thus a key component to achieve efficiency. Despite that, a quadratic CNF is currently adopted by many ASP solvers. The problem cannot be further underestimated because of a recently formalized construct of GRINGO [Gebser et al., 2015a] that was already used in the literature [Abseher et al., 2015]. Actually, two solutions to this problem are proposed in this paper, one using a CNF of linear size, and another using propagators for an even more efficient memory management.

References [Abseher et al., 2015] Michael Abseher, Bernhard Bliem,

Günther Charwat, Frederico Dusberger, and Stefan Woltran. Computing secure sets in graphs using answer set programming. Journal of Logic and Computation, 2015. [Alviano et al., 2010] Mario Alviano, Wolfgang Faber, Nicola Leone, Simona Perri, Gerald Pfeifer, and Giorgio

Terracina. The disjunctive datalog system DLV. In Datalog Reloaded, volume 6702 of Lecture Notes in Computer Science, pages 282 301. Springer, 2010. [Alviano et al., 2013] Mario Alviano, Carmine Dodaro, Wolfgang Faber, Nicola Leone, and Francesco Ricca. WASP: A native ASP solver based on constraint learning. In LPNMR 2013, volume 8148 of Lecture Notes in Computer Science, pages 54 66. Springer, 2013. [Alviano et al., 2014] Mario Alviano, Carmine Dodaro, and

Francesco Ricca. Anytime computation of cautious consequences in answer set programming. TPLP, 14(4-5):755 770, 2014. [Alviano et al., 2015a] Mario Alviano, Carmine Dodaro, Nicola Leone, and Francesco Ricca. Advances in WASP. In LPNMR 2015, volume 9345 of Lecture Notes in Computer Science, pages 40 54. Springer, 2015. [Alviano et al., 2015b] Mario Alviano, Carmine Dodaro,

and Francesco Ricca. Reduct-based stability check using literal assumptions. In ASPOCP 2015, 2015. [Audemard and Simon, 2009] Gilles Audemard and Laurent

Simon. Predicting learnt clauses quality in modern SAT solvers. In IJCAI 2009, pages 399 404, 2009. [Baral, 2003] Chitta Baral. Knowledge Representation, Rea-

soning and Declarative Problem Solving. Cambridge University Press, 2003. [Ben-Eliyahu and Dechter, 1994] Rachel Ben-Eliyahu and

Rina Dechter. Propositional semantics for disjunctive logic programs. Ann. Math. Artif. Intell., 12(1-2):53 87, 1994. [Clark, 1977] Keith L. Clark. Negation as failure. In Logic

and Data Bases, pages 293 322, 1977. [Drescher et al., 2008] Christian Drescher, Martin Gebser,

Torsten Grote, Benjamin Kaufmann, Arne König, Max Ostrowski, and Torsten Schaub. Conflict-driven disjunctive answer set solving. In KR 2008, pages 422 432. AAAI Press, 2008. [Erdem and Lifschitz, 2003] Esra Erdem and Vladimir Lifs-

chitz. Tight logic programs. TPLP, 3(4-5):499 518, 2003. [Fages, 1994] François Fages. Consistency of clark s com-

pletion and existence of stable models. Meth. of Logic in CS, 1(1):51 60, 1994. [Gebser et al., 2013] Martin Gebser, Benjamin Kaufmann,

and Torsten Schaub. Advanced conflict-driven disjunctive answer set solving. In IJCAI. IJCAI/AAAI, 2013. [Gebser et al., 2015a] Martin Gebser, Amelia Harrison, Roland Kaminski, Vladimir Lifschitz, and Torsten Schaub. Abstract gringo. TPLP, 15(4-5):449 463, 2015. [Gebser et al., 2015b] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Javier Romero, and Torsten Schaub. Progress in clasp series 3. In LPNMR 2015, volume 9345 of Lecture Notes in Computer Science, pages 368 383. Springer, 2015. [Gelfond and Kahl, 2014] Michael Gelfond and Yulia Kahl.

Knowledge Representation, Reasoning, and the Design

of Intelligent Agents: The Answer-Set Programming Approach. Cambridge University Press, 2014. [Ignatiev et al., 2015] Alexey Ignatiev, Alessandro Previti,

Mark H. Liffiton, and Joao Marques-Silva. Smallest MUS extraction with minimal hitting set dualization. In CP 2015, volume 9255 of Lecture Notes in Computer Science, pages 173 182. Springer, 2015. [Janhunen and Niemelä, 2011] Tomi Janhunen and Ilkka

Niemelä. Compact translations of non-disjunctive answer set programs to propositional clauses. In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning, volume 6565 of Lecture Notes in Computer Science, pages 111 130. Springer, 2011. [Janhunen, 2006] Tomi Janhunen. Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics, 16(12):35 86, 2006. [Lee and Lifschitz, 2003] Joohyung Lee and Vladimir Lifs-

chitz. Loop formulas for disjunctive logic programs. In ICLP 2003, volume 2916 of Lecture Notes in Computer Science, pages 451 465. Springer, 2003. [Leone et al., 1997] Nicola Leone, Pasquale Rullo, and Francesco Scarcello. Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation. Inf. Comput., 135(2):69 112, 1997. [Lierler, 2005] Yuliya Lierler. Cmodels - SAT-based disjunc-

tive answer set solver. In LPNMR 2005, volume 3662 of Lecture Notes in Computer Science, pages 447 451. Springer, 2005. [Liffiton and Sakallah, 2008] Mark H. Liffiton and Karem A.

Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning, 40(1):1 33, 2008. [Lifschitz, 2002] Vladimir Lifschitz. Answer set program-

ming and plan generation. Artif. Intell., 138(1-2):39 54, 2002. [Marek and Truszczy nski, 1999] Victor W. Marek and Mirosław Truszczy nski. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm A 25-Year Perspective, pages 375 398. Springer Verlag, 1999. [Niemelä, 1999] Ilkka Niemelä. Logic programs with stable

model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell., 25(3-4):241 273, 1999. [Przymusinski, 1991] Teodor C. Przymusinski. Stable semantics for disjunctive programs. New Generation Comput., 9(3/4):401 424, 1991. [Silva and Sakallah, 1996] João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In ICCAD, pages 220 227, 1996. [Simons et al., 2002] Patrik Simons, Ilkka Niemelä, and

Timo Soininen. Extending and implementing the stable model semantics. Artif. Intell., 138(1-2):181 234, 2002.