Completion of Disjunctive Logic Programs

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-INdAM).

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:

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: Wx2y s0 (x) .

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:

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

is a compact representation of the following clauses: ¶`0♦ [ ¶`i ♣ i 2 [1▷▷n]♦; ¶`0↪ `i♦, for all i 2 [1▷▷n]. Similarly,

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 SupMod(⇧) denote the set of supported models of ⇧.

Example 1. The models of the following program⇧1:

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:

Its only model is ¶c↪ c1 ↪ c3 ♦, and therefore Mod(Γ1) ⌘At(⇧) SupMod(⇧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 StMod(⇧) be the set of stable models of ⇧. It is well known that StMod(⇧) ✓ SupMod(⇧) for any program ⇧, while StMod(⇧) = SupMod(⇧) does not hold in general. Actually, the fact that StMod(⇧) ✓ SupMod(⇧) 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 StMod(⇧) = SupMod(⇧) 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 StMod(⇧) 6= ; is known to be ⌃P2 -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 I 0 := sinf ⇤ (⇧↪ I), and I 00 := unit ⇤ (Γ↪ I); (i) I 0 ✓ I 00 ; (ii) if (I 0 )+ [(I 0 )- = At(⇧), then (I 00 )+ [ (I 00 )- = 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♦, I 0 is ¶≻a↪ c↪ ≻b♦ (c is inferred by forward chain, and ≻b by lack of support). In this case, I 00 is ¶≻a↪ ≻a1 ↪ c3 ↪ c↪ ≻b1 ↪ ≻b2 ↪ ≻b↪ c1 ♦, and condition (i) is satisfied. Also note that I 0 and I 00 satisfy condition (ii): For I = ¶a♦, I 0 is inconsistent (b is inferred by forward chain, and then ≻a by lack of support); in this case, I 00 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

for all r 2 ⇧ of the form (2) with m = 1, where pr1 is a fresh atom (true if and only if r is a support of p1), together with 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(⇧) SupMod(⇧);
2. comp(⇧) winf ⇧;
3. ♣comp(⇧)♣ 2 O(♣⇧♣).

Example 4. Let ⇧2 be the following program:

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

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. SupMod(shift(⇧)) ⌘A SupMod(⇧), and therefore Mod(comp(shift(⇧))) ⌘At(⇧) SupMod(⇧);
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 tr1 ↪ ▷ ▷ ▷ ↪ trm 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:

for all r 2 ⇧ of the form (2), where tr1 ↪ ▷ ▷ ▷ ↪ trm are fresh atoms.

Theorem 1. If ⇧ is a program, then:

1. StMod(norm(⇧)) ⌘At(⇧) StMod(⇧);
2. ♣norm(⇧)♣ 2 O(♣⇧♣);
3. SupMod(norm(⇧)) 6⌘At(⇧) SupMod(⇧), 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↪ t11 ↪ t31 ↪ t21 ♦, and therefore StMod(norm(⇧1)) ⌘At(⇧1) StMod(⇧1). On the other hand, ¶t11 ↪ t12 ↪ 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↪ t12 ↪ t13 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 pri 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 mmay 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: sri , true if and only if rule r may support pi, for i 2 [1▷▷m]; dri , 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

prm $ srm

(19)

for all r 2 ⇧ of the form (2), together with (7) for all p 2 At (⇧). Note that (15) defines drm as an alias of pm. Similarly, (19) defines srm as an alias of prm. It turns out that drm and srm 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 sr1 is replaced by its alias pr1 .

Theorem 2. If ⇧ is a program, then:

1. Mod(comp _(⇧)) ⌘At(⇧) SupMod(⇧);
2. comp _(⇧) winf ⇧;
3. comp(⇧) = comp _(⇧) if ⇧ is disjunction-free.
4. ♣comp _(⇧)♣ 2 O(♣⇧♣);

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

Its only model is ¶c↪ s11 ↪ d13 ↪ d12 ↪ ≻a1 ↪ ≻b1 ↪ ≻a↪ s12 ↪ ≻b2 ↪ ≻b↪ s13 ↪ c1 ↪ c3 ♦, and therefore Mod(comp _(⇧1)) = SupMod(⇧1). As for inferences, for I = ¶≻a♦, sinf ⇤ (⇧1↪ I) is ¶≻a↪ c↪ ≻b♦, and unit ⇤ (comp _(⇧1)↪ I) is ¶≻a↪ ≻a1 ↪ d12 ↪ c3 ↪ c↪ d13 ↪ ≻b1 ↪ ≻b2 ↪ ≻b↪ s11 ↪ s12 ↪ s13 ↪ 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:

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 Pi2[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 Pj2[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:

if the current interpretation is ¶s11 ↪ ≻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 pseudoBoolean constraint. The general idea is to use auxiliary atoms sr1 , pr1 ↪ ▷ ▷ ▷ ↪ prm (as in comp _) for each rule r of the form (2), and to compactly represent the following clauses:

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↪ ≻sr1 ] and vr 1 := [pr1 ↪ ▷ ▷ ▷ ↪ prm]; when the i-th literal of vector vrk (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:

Indeed, since ¶pi↪ ≻pri ♦ belongs to (7), whenever ≻pi is added to the current interpretation, ≻pri is added as well. Thus, both (23) and (24) satisfy the following conditions: if p1↪ ▷ ▷ ▷ ↪ pm are false, then ≻sr1 is inferred; if p1↪ ▷ ▷ ▷ ↪ pi-1↪ pi+1↪ ▷ ▷ ▷ ↪ pm, for some i 2 [1▷▷m], and sr1 is true, then pi and pri 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:

by clause ¶s11 ♦, 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

i.e., the symbolic version of program¶Wx2[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.

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 RelatedWork

Supported model search is a significant part in the most frequent computational task of ASP solving, that is, computing 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

for each rule r 2 ⇧ of the form (2), and an implication

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 coNP-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.