Experimenting with Heuristics for Answer Set Programming

1 Introduction

Answer set programming (ASP) is a declarative approach to programming, which has been recently proposed in the area of nonmonotonic reasoning and logic programming. The knowledge representation language of ASP is very expressive: function-free logic programs with classical negation where disjunction is allowed in the heads of the rules and nonmonotonic negation may occur in the bodies of the rules. The intended models of an ASP program (i.e., the semantics of the program) are subset-minimal models which are "grounded" in a precise sense, they are called answer sets [Gelfond and Lifschitz, 1991]. The idea of answer set programming is to represent a given computational problem by an ASP program whose answer sets correspond to solutions, and then use an answer set solver to find such a solution [Lifschitz, 1999].

✎ This work was supported by FWF (Austrian Science Funds) under the project Z29-INF and P14781.

As an example, consider the well-known problem of 3colorability, which is the assignment of three colors to the nodes of a graph in such a way that adjacent nodes have different colors. This problem is known to be NP-complete. Suppose that the nodes and the edges are represented by a set ✏ of facts with predicates ✑ ✒ ✔ ✖ (unary) and ✖ ✔ ✙ ✖ (binary), respectively. Then, the following ASP program allows us to determine the admissible ways of coloring the given graph.

✜ ✢ ✣ ✤ ✦ ★ ✦ ✜ ✬ ✮ ✰ ✜ ✳ ✵ ✤ ✦ ★ ✦ ✜ ✬ ✮ ✰ ✸ ✳ ✵ ✤ ✦ ★ ✦ ✜ ✬ ✮ ✰ ✾ ✳ ✣ ✿ ❀ ✦ ❂ ❃ ✬ ✮ ✳ ✜ ❅ ✣ ✣ ✿ ❃ ❂ ✾ ❃ ✬ ✮ ✰ ❈ ✳ ✰ ✤ ✦ ★ ✦ ✜ ✬ ✮ ✰ ❋ ✳ ✰ ✤ ✦ ★ ✦ ✜ ✬ ❈ ✰ ❋ ✳

Rule ❏ ❑ above states that every node of the graph is colored red or yellow or green, while ❏ ☎ forbids the assignment of the same color to any adjacent nodes. The minimality of answer sets guarantees that every node is assigned only one color. Thus, there is a one-to-one correspondence between the solutions of the 3-coloring problem and the answer sets of ✏ ▲ ◆ ❏ ❑ a80 ❏ ☎ ◗ . The graph is 3-colorable if and only if ✏ ▲ ◆ ❏ ❑ a80 ❏ ☎ ◗ has some answer set.

An advantage of answer set programming over SAT-based programming is that problems can be encoded more easily in the ASP language than in propositional CNF formulas, thanks to the nonmonotonic character of disjunction and negation as failure [Lifschitz, 1999]. Importantly, due to the support for variables, every problem in the complexity class ✁ ✂ ☎ (i.e., in ✞ ✠ ☛ ✌ ) can be directly encoded in an ASP program which can then be used to solve all problem instances in a uniform way [Eiter et al., 1997].

The high expressiveness of answer set programming comes at the price of a high computational cost in the worst case, which makes the implementation of efficient ASP systems a difficult task. Nevertheless, some efforts have been done in this direction, and a number of ASP systems are now available. The two best known ASP systems are DLV [Eiter et al., 2000], and Smodels [Niemel¨ a, 1999; Simons, 2000], but also other systems support ASP to some extent, including CCALC

[McCain and Turner, 1998], DCS [East and Truszczy´nski, 2000❚ ], QUIP [Egly et al., 2000], and XSB [Rao et al., 1997].

The core of an ASP system is model generation, where a model of the program is produced, which is then subjected to an answer set check. For the generation of models, ASP systems employ procedures which are similar to Davis-Putnam procedures used in SAT solvers. As for SAT solvers, the heuristic (branching rule) for the selection of the branching literal (i.e., the criterion determining the literal to be assumed true at a given stage of the computation) is fundamentally important for the efficiency of a model generation procedure, and dramatically affects the overall performance of an ASP system. While a lot of work has been done in AI developing new heuristics and comparing alternative heuristics for SAT (see, e.g., [Hooker and Vinay, 1995; Li and Anbulagan, 1997; Freeman, 1995]), only little work has been done so far for ASP systems. In particular, we are not aware of any previous comparison between heuristics for ASP.

In this paper, we evaluate different heuristics for ASP systems. To this end, we first consider a couple of heuristics which have been very successful in SAT solvers or in nondisjunctive ASP systems, and we extend them to the framework of (disjunctive) ASP. We then perform an experimentation activity to compare the different heuristics. In particular, we implement the heuristics in the ASP system DLV, and we compare their respective efficiency on a number of benchmark problems taken from various domains. The experiments show interesting results, and evidence a couple of promising heuristic criteria for ASP, which sensibly outperform the heuristic of DLV. Nevertheless, this paper is not at all a conclusive work on heuristics for ASP; rather, it is a first step in this field that will hopefully stimulate further works on the design and evaluation of heuristics for ASP, which are strongly needed to build efficient ASP solvers.

2 Answer Set Programming Language

In this section, we provide a formal definition of the syntax and semantics of the answer set programming language supported by DLV: disjunctive datalog extended with strong negation. For further background, see [Gelfond and Lifschitz, 1991; Eiter et al., 2000].

ASP Programs

A (disjunctive) rule ❏ is a formula

where ❯ ❑ a80 ❳ ❳ ❳ a80 ❯ ❬ a80 ❵ ❑ a80 ❳ ❳ ❳ a80 ❵ ✐ are classical literals (atoms possibly preceded by the symbol ❦ ) and ✑ ❧ ♠ a80 ♥ ❧ ♣ ❧ ♠ . The disjunction ❯ ❑ ❱ ❳ ❳ ❳ ❱ ❯ ❬ is the head of ❏ , while the conjunction ❵ ❑ a80 ❳ ❳ ❳ a80 ❵ ❜ a80 ❞ ❢ ❣ ❵ ❜ ❤ ❑ a80 ❳ ❳ ❳ a80 ❞ ❢ ❣ ❵ ✐ is the body, ❵ ❑ a80 ❳ ❳ ❳ a80 ❵ ❜ the positive body, and ❞ ❢ ❣ ❵ ❜ ❤ ❑ a80 ❳ ❳ ❳ a80 ❞ ❢ ❣ ❵ ✐ the negative body of ❏ . Comparison operators (like ✆ a80 a115 a80 ✉ a80 a115 ✉ ) are built-in predicates in ASP systems, and may appear in the bodies of rules.

A disjunctive datalog program (also called ASP program in this paper) ✈ is a finite set of rules.

As usual, an object (atom, rule, etc.) is called ground or propositional, if it contains no variables.

Answer Sets

We describe the semantics of consistent answer sets, which has originally been defined in [Gelfond and Lifschitz, 1991].

Given a program ✈ , let the Herbrand Universe ✇ ① be the set of all constants appearing in ✈ and theHerbrand Base ③ ① be the set of all possible combinations of predicate symbols appearing in ✈ with constants of ✇ ① , possibly preceded by ❦ . A set ④ of literals is said to be consistent if, for every literal ⑤ ⑥ ④ , its complementary literal is not contained in ④ .

Given a rule ❏ , ⑦ ❏ ✒ ⑧ ✑ ✔ ⑩ ❏ ❸ denotes the set of rules obtained by applying all possible substitutions ❹ from the variables in ❏ to elements of ✇ ① . Similarly, given a program ✈ , the ground instantiation ⑦ ❏ ✒ ⑧ ✑ ✔ ⑩ ✈ ❸ of ✈ is the set ❻ ❼ ❽ ① ⑦ ❏ ✒ ⑧ ✑ ✔ ⑩ ❏ ❸ .

For every program ✈ , we define its answer sets using its ground instantiation ⑦ ❏ ✒ ⑧ ✑ ✔ ⑩ ✈ ❸ in two steps, following [Lifschitz, 1996]: First we define the answer sets of positive programs, then we give a reduction of general programs to positive ones and use this reduction to define answer sets of general programs.

An interpretation ❾ is a set of ground literals. A consistent interpretation ❾ ❿ ③ ① is closed under ✈ (where ✈ is a positive program), if, for every ❏ ⑥ ⑦ ❏ ✒ ⑧ ✑ ✔ ⑩ ✈ ❸ , at least one literal in the head is true whenever all literals in the body are true. ➁ is an answer set for ✈ if it is minimal w.r.t. set inclusion and closed under ✈ .

The reduct or Gelfond-Lifschitz transform of a general ground program ✈ w.r.t. a set ➁ ❿ ③ ① is the positive ground program ✈ ➄ , obtained from ✈ by (i) deleting all rules ❏ ⑥ ✈ whose negative body is false w.r.t. X and (ii) deleting the negative body from the remaining rules.

An answer set of a general program ✈ is a set ➁ ❿ ③ ① such that ➁ is an answer set of ⑦ ❏ ✒ ⑧ ✑ ✔ ⑩ ✈ ❸ ➄ .

3 Answer Sets Computation

In this section, we describe the main steps of the computational process performed by ASP systems. We will refer particularly to the computational engine of the DLV system, which will be used for the experiments, but also other ASP systems, like Smodels, employ a very similar procedure.

An answer set program ✈ in general contains variables. The first step of a computation of an ASP system eliminates these variables, generating a ground instantiation ✙ ❏ ✒ ⑧ ✑ ✔ ⑩ ✈ ❸ of ✈ . 1 The hard part of the computation is then performed on this ground ASP program generated by the instantiator.

The heart of the computation is performed by the Model Generator, which is sketched in Figure 1. Roughly, the Model Generator produces some "candidate" answer sets. The stability of each of them is subsequently verified by the function IsAnswerSet(I), which verifies whether the given "candidate" ❾ is a minimal model of the program ⑦ ❏ ✒ ⑧ ✑ ✔ ⑩ ✈ ❸ ➇ obtained by applying the GL-transformation w.r.t. ❾ and outputs the model, if so. IsAnswerSet(I) returns True if the computation should be stopped and False otherwise.

1 Note that ✾ ✜ ✦ ➈ ❀ ❂ ✬ ➉ ✳ is not the full set of all syntactically constructible instances of the rules of ➉ ; rather, it is a subset (often much smaller) of it having precisely the same answer sets as ➉ [Faber et al., 1999a].

Function ModelGenerator(I: Interpretation): Boolean; var inconsistency: Boolean; begin I := DetCons(I); if I = ➊ then return False; (* inconsistency *) if no atom is undefined in I then return IsAnswerSet(I); Select an undefined ground atom ➋ according to a heuristic; if ModelGenerator(➌ ➍ ➎ ➋ ➐ ) then return True; else returnModelGenerator( ➌ ➍ ➎ ➑ ➒ ➓ ➋ ➐ ); end;

The ModelGenerator function is first called with parameter ❾ set to the empty interpretation. 2 If the program ✈ has an answer set, then the function returns True setting ❾ to the computed answer set; otherwise it returns False. The Model Generator is similar to the Davis-Putnam procedure employed by SAT solvers. It first calls a function DetCons(), which returns the extension of ❾ with the literals that can be deterministically inferred (or the set of all literals ➔ upon inconsistency). This function is similar to a unit propagation procedure employed by SAT solvers, but exploits the peculiarities of ASP for making further inferences (e.g., it exploits the knowledge that every answer set is a minimal model). If DetCons does not detect any inconsistency, an atom → is selected according to a heuristic criterion and ModelGenerator is called on ❾ ▲ ◆ → ◗ and on ❾ ▲ ◆ ❞ ❢ ❣ → ◗ . The atom → plays the role of a branching variable of a SAT solver. And indeed, like for SAT solvers, the selection of a "good" atom → is crucial for the performance of an ASP system. In the next section, we describe a number of heuristic criteria for the selection of such branching atoms.

4 Heuristics

Throughout this section, we assume that a ground ASP program ✈ and an interpretation ❾ have been fixed. Here, we describe the heuristic criteria that will be compared in Section 7. We consider "dynamic heuristics" (the ASP equivalent of UP heuristics for SAT), that is, branching rules where the heuristic value of a literal ↔ depends on the result of taking ↔ true and computing its consequences. Given a literal ↔ , ✖ ↕ ➙ ⑩ ↔ ❸ will denote the intepretation resulting from the application of DetCons (see previous section) on ❾ ▲ ◆ ↔ ◗ ; w.l.o.g., we assume that ✖ ↕ ➙ ⑩ ↔ ❸ is consistent, otherwise ↔ is automatically set to false and the heuristic is not evaluated on ↔ at all.

Heuristic ➜ ➝ . This is an extension of the branching rule adopted in the system SATZ [Li and Anbulagan, 1997] - one of the most efficient SAT solvers - to the framework of ASP.

The length of a rule ❏ (w.r.t. an interpretation ➟ ), is the number of undefined literals occurring in ❏ . Let ✇ ✑ ➡ ❯ ➙ ❜ ⑩ ↔ ❸ denote the number of unsatisfied rules 3 of length ♣ w.r.t. ✖ ↕ ➙ ⑩ ↔ ❸ , which have a greater length w.r.t. ❾ . In other words, ✇ ✑ ➡ ❯ ➙ ❜ ⑩ ↔ ❸ is the number of unsatisfied rules whose length shrinks to ♣ if the truth of ↔ is assumed and propagated in the interpretation ❾ . The weight ➥ ❑ ⑩ ↔ ❸ is

2 Observe that the interpretations built during the computation are 3-valued, that is a literal can be True, False or Undefined (if its value has not been set yet) w.r.t. to an interpretation ➌ .

3 Recall that a rule ✜ is satisfied w.r.t. ➤ if the body of ✜ is false w.r.t. ➤ or the head of ✜ is true w.r.t. ➤ .

Thus, the weight function ➥ ❑ prefers literals introducing a higher number of short unsatisfied rules. Intuitively, the introduction of a high number of short unsatisfied rules is preferred because it creates more and stronger constraints on the intepretation so that a contradiction can be found earlier [Li and Anbulagan, 1997]. We combine the weight of an atom ↔ with the weight of its complement ❞ ❢ ❣ ↔ to favour ↔ such that ➥ ❑ ⑩ ↔ ❸ and ➥ ❑ ⑩ ❞ ❢ ❣ ↔ ❸ are roughly equal, to avoid that a possible failure leads to a very bad state. To this end, as in SATZ, we define the combined weight comb-➥ ❑ ⑩ ↔ ❸ of an atom ↔ as follows:

Given two atoms → and ③ , heuristic ➲ ❑ prefers ③ over → ( → a115 ➵ ❑ ③ ) iff comb- ➥ ❑ ⑩ → ❸ a115 comb- ➥ ❑ ⑩ ③ ❸ . Once a a115 ➵ ❑ -maximum atom ↔ is selected, heuristic ➲ ❑ takes ↔ if ➥ ❑ ⑩ ↔ ❸ ✉ ➥ ❑ ⑩ ❞ ❢ ❣ ↔ ❸ , ❞ ❢ ❣ ↔ else.

Heuristic ➜ ➽ . The second heuristic we consider is inspired to the branching rule of Smodels - a well known ASP system [Simons, 2000]. Let ➾ ➟ ➾ denote the number of atoms which are either true or false in a (three-valued) intepretation ➟ . Then, define

Since ➥ ☎ maximizes the size of the resulting intepretation, it minimizes the atoms which are left undefined. Intuitively, this minimizes the size of the remaining search space (which is ➫ ➶ , where ⑧ is the number of undefined atoms in ✖ ↕ ➙ ⑩ ↔ ❸ ) [Simons, 2000]. Similar to Smodels, the heuristic ➲ ☎ cautiously maximizes the minimum of ➥ ☎ ⑩ ↔ ❸ and ➥ ☎ ⑩ ❞ ❢ ❣ ↔ ❸ . More precisely, the preference relationship a115 ➵ ☎ of ➲ ☎ is defined as follows. Given two atoms → and ③ , → a115 ➵ ☎ ③ if ♥ ➘ ✑ ⑩ ➲ ☎ ⑩ → ❸ a80 ➲ ☎ ⑩ ❞ ❢ ❣ → ❸ ❸ a115 ♥ ➘ ✑ ⑩ ➲ ☎ ⑩ ③ ❸ a80 ➲ ☎ ⑩ ❞ ❢ ❣ ③ ❸ ❸ ; otherwise, → a115 ➵ ☎ ③ if ♥ ➘ ✑ ⑩ ➲ ☎ ⑩ → ❸ a80 ➲ ☎ ⑩ ❞ ❢ ❣ → ❸ ❸ ✆ ♥ ➘ ✑ ⑩ ➲ ☎ ⑩ ③ ❸ a80 ➲ ☎ ⑩ ❞ ❢ ❣ ③ ❸ ❸ and ♥ ❯ ↕ ⑩ ➲ ☎ ⑩ → ❸ a80 ➲ ☎ ⑩ ❞ ❢ ❣ → ❸ ❸ a115 ♥ ❯ ↕ ⑩ ➲ ☎ ⑩ ③ ❸ a80 ➲ ☎ ⑩ ❞ ❢ ❣ ③ ❸ ❸ . Once a a115 ➵ ☎ -maximum atom ↔ is selected, heuristic ➲ ☎ takes either ↔ or ❞ ❢ ❣ ↔ , depending on the same selection principle.

Remark. It is worthwhile noting that the heuristic of Smodels, while following the above intuition, is more advanced and sophisticated than ➲ ☎ . Unfortunately, it is defined for non-disjunctive programs, and centered around properties of unstratified negation. which is not so important in our framework. We do not see any immediate extension of Smodels' heuristic to the framework of disjunctive ASP programs.

Heuristic ➜ ➱ . Let us consider now the heuristic used in the DLV system. Even if this is more "naive" than the previous heuristics, we will benchmark it in order to evaluate the impact of changing the branching rule on the test system.

A peculiar property of answer sets is supportedness: For each true atom → of an answer set ❾ , there exists a rule ❏ of the program such that the body of ❏ is true w.r.t. ❾ and → is the only true atom in the head of ❏ . Since an ASP system must eventually converge to a supported interpretation, ASP

systems try to keep the interpretations "as much supported as possible" ❐ during the intermediate steps of the computation. To this end, the DLV system counts the number of UnsupportedTrue (UT) atoms, i.e., atoms which are true in the current interpretation but still miss a supporting rule (further details on UTs can be found in [Faber et al., 1999b] where they are called MBTs). For instance, the rule ❪ ❴ ✑ ✒ ➙ ↕ implies that ↕ must be true in every answer set of the program; but it does not give a "support" for ↕ . Thus, in the DLV system ↕ is taken true to satisfy the rule, and it is added to the set of UnsupportedTrue; it will be removed from this set once a supporting rule for ↕ will be found (e.g., ↕ ❱ ❵ ❪ ❴ ❒ is a supporting rule for ↕ in the interpretation ❾ ✆ ◆ ↕ a80 ❞ ❢ ❣ ❵ a80 ❒ ◗ ). Given a literal ↔ , let ✇ ❮ ⑩ ↔ ❸ be the number of UT atoms in ✖ ↕ ➙ ⑩ ↔ ❸ . Moreover, let ✇ ❮ ☎ ⑩ ↔ ❸ and ✇ ❮ ❰ ⑩ ↔ ❸ be the number of UT atoms occurring, respectively, in the heads of exactly 2 and 3 unsatisfied rules w.r.t. ✖ ↕ ➙ ⑩ ↔ ❸ . The heuristic ➲ ❰ of DLV considers ✇ ❮ ⑩ ↔ ❸ , ✇ ❮ ☎ ⑩ ↔ ❸ and ✇ ❮ ❰ ⑩ ↔ ❸ in a prioritized way, to favor atoms yielding interpretations with fewer ✇ ❮ a208 ✇ ❮ ☎ a208 ✇ ❮ ❰ atoms (which should more likely lead to a supported model). If all UT counters are equal, then the heuristic considers the total number a209 ❯ ➙ ⑩ ↔ ❸ of rules which are satisfied w.r.t. ✖ ↕ ➙ ⑩ ↔ ❸ . More precisely, given two atoms → and ③ :

1. → a115 ➵ ❰ ③ if ✇ ❮ ⑩ → ❸ ✉ ✇ ❮ ⑩ ③ ❸ ;
2. otherwise, → a115 ➵ ❰ ③ if ✇ ❮ ⑩ → ❸ ✆ ✇ ❮ ⑩ ③ ❸ and ✇ ❮ ☎ ⑩ → ❸ ✉ ✇ ❮ ☎ ⑩ ③ ❸ ;

1. otherwise, → a115 ❰ ③ if ✇ ❮ ❰ ⑩ → ❸ ✆ ✇ ❮ ❰ ⑩ ③ ❸ and a209 ❯ ➙ ⑩ → ❸ a115 a209 ❯ ➙ ⑩ ③ ❸ .

A a115 ➵ ❰ -maximum atom is selected by the heuristic ➲ ❰ of DLV. Unlike the previous heuristics, ➲ ❰ considers only atoms (instead of literals), and it does not take into account what happens when the selected atom ↔ leads to a failure (i.e., ✖ ↕ ➙ ⑩ ❞ ❢ ❣ ↔ ❸ is not considered in the heuristic).

Heuristic ➜ a211 . Finally, we have considered a simple "balanced version" ➲ a212 of the heuristic ➲ ❰ of DLV, where also the complement of an atom is evaluated for the heuristic. Given an atom → , let ✇ ❮ a213 ⑩ → ❸ ✆ ✇ ❮ ⑩ → ❸ ➯ ✇ ❮ ⑩ ❞ ❢ ❣ → ❸ , ✇ ❮ a213 ☎ ⑩ → ❸ ✆ ✇ ❮ ☎ ⑩ → ❸ ➯ ✇ ❮ ☎ ⑩ ❞ ❢ ❣ → ❸ , ✇ ❮ a213 ❰ ⑩ → ❸ ✆ ✇ ❮ ❰ ⑩ → ❸ ➯ ✇ ❮ ❰ ⑩ ❞ ❢ ❣ → ❸ , and a209 ❯ ➙ a213 ⑩ → ❸ ✆ a209 ❯ ➙ ⑩ → ❸ ➯ a209 ❯ ➙ ⑩ ❞ ❢ ❣ → ❸ . The heuristic ➲ a212 works precisely as ➲ ❰ , but considers the primed counters. Once the best atom has been selected, it is taken positive or negative, depending on ➲ ❰ .

5 Benchmark Programs

To evaluate the different heuristics presented in the previous section, we chose a couple of benchmark problems: 3SAT, Blocksworld Planning, Hamiltonian path, and Strategic Companies.

3SAT is one of the best researched problems in AI and generally used for solving many other problems by translating them to 3SAT, solving the 3SAT problem and transforming the solution back to the original domain:

Let a214 be a propositional formula in conjunctive normal form (CNF) a214 ✆ a215 ❬ a216 a217 ❑ ⑩ ✔ a216 a218 ❑ ❱ ❥ ❥ ❥ ❱ ✔ a216 a218 ❰ ❸ where the ✔ a216 a218 a219 are literals over the propositional variables ↕ ❑ a80 ❥ ❥ ❥ a80 ↕ ✐ . a214 is satisfiable, iff there exists a consistent conjunction ❾ of literals such that ❾ ➾ ✆ a214 (see e.g. [Papadimitriou, 1994] for a complete definition).

3SAT is a classical NP-complete problem and can be easily represented in our formalism as follows:

For every propositional variable ↕ a216 ( ➩ a220 ➘ a220 ♥ ), we add the following rule which ensures that we either assume that variable ↕ a216 or its complement ✑ ↕ a216 true:

And for every clause ✔ ❑ ❱ ❥ ❥ ❥ ❱ ✔ ❰ in a214 we add the constraint

where a227 ✔ a216 ( ➩ a220 ➘ a220 a228 ) is ↕ a219 if ✔ a216 is a positive literal ↕ a219 , and ✑ ↕ a219 if ✔ a216 is a negative literal ❞ ❢ ❣ ↕ a219 .

Hamiltonian Path (HAMPATH) is another classical NPcomplete problem from the area of graph theory:

Given an undirected graph ⑦ ✆ ⑩ a229 a80 a230 ❸ , where a229 is the set of vertices of ⑦ and a230 is the set of edges, and a node ❯ ⑥ a229 of this graph, does there exist a path of ⑦ starting at ❯ and passing through each node in a229 exactly once?

Suppose that the graph ⑦ is specified by using two predicates ✑ ✒ ✔ ✖ ⑩ ➁ ❸ and ❯ ❏ ❒ ⑩ ➁ a80 a231 ❸ 4 , and the starting node is specified by the predicate ➡ ➙ ❯ ❏ ➙ (unary) which contains only a single tuple. Then, the following program solves the problem HAMPATH.

% Each node has to be reached. ✣ ✿ ❀ ✦ ❂ ❃ ✬ ✮ ✳ ✰ ➑ ➒ ➓ ✜ ❃ a232 ✤ a233 ❃ ❂ ✬ ✮ ✳ a223 ✜ ❃ a232 ✤ a233 ❃ ❂ ✬ ✮ ✳ ✣ ✿ a234 a235 a232 ✜ a235 ✬ ✮ ✳ a223 ✜ ❃ a232 ✤ a233 ❃ ❂ ✬ ✮ ✳ ✣ ✿ a236 ❀ a238 a232 a235 a233 ✬ ❈ ✰ ✮ ✳ a223 % Guess whether to take a path or not. a236 ❀ a238 a232 a235 a233 ✬ ✮ ✰ ❈ ✳ ✵ ✦ ➈ a235 a238 a232 a235 a233 ✬ ✮ ✰ ❈ ✳ ✣ ✿ ✜ ❃ a232 ✤ a233 ❃ ❂ ✬ ✮ ✳ ✰ a232 ✜ ✤ ✬ ✮ ✰ ❈ ✳ a223 % At most one incoming/outgoing arc! ✣ ✿ a236 ❀ a238 a232 a235 a233 ✬ ✮ ✰ ❈ ✳ ✰ a236 ❀ a238 a232 a235 a233 ✬ ✮ ✰ ❈ a240 ✳ ✰ ❈ a241 a242 ❈ a240 a223 ✣ ✿ a236 ❀ a238 a232 a235 a233 ✬ ✮ ✰ ❈ ✳ ✰ a236 ❀ a238 a232 a235 a233 ✬ ✮ a240 ✰ ❈ ✳ ✰ ✮ a241 a242 ✮ a240 a223

Blocksworld (BW) is a classic problem from the planning domain, and one of the oldest problems in AI:

Given a table and a number of blocks in a (known) initial state and a desired goal state, try to reach that goal state by moving one block at a time such that each block is either on top of another block or the table at any given time step.

Figure 2 shows a simple example that can be solved in three time steps: First we move block c to the table, then block b on top of a, and finally c on top of b.

4 Predicate a232 ✜ ✤ is symmetric, since undirected arcs are bidirectional.

Due to space restrictions we refer to [Erdem, 1999; Faber et al., 1999a] for a complete encoding.

Strategic Companies (STRATCOMP) finally, is a ✁ ✂ ☎ - complete problem, which has been first described in [Cadoli et al., 1997]:

A holding owns ❒ companies, each of which produces some goods. Some of these companies may jointly control others. This is modelled by means of predicates a243 ❏ ✒ ✔ ⑩ a244 a80 a245 ➩ a80 a245 ➫ ❸ (a244 is produced by a245 ➩ and a245 ➫ ) and ❒ ✒ ✑ ➙ ⑩ a245 a80 a245 ➩ a80 a245 ➫ a80 a245 a228 ❸ (company a245 is jointly controlled by a245 ➩ , a245 ➫ and a245 a228 ).

Now, some companies should be sold, under the constraint that all goods can be still produced, and that no company is sold which would still be controlled by the holding afterwards. A company is strategic, if it belongs to a strategic set, which is a minimal set of companies satisfying these constraints.

The answer sets of the following natural program correspond one to one to the strategic sets. Checking whether any given company a245 is strategic is done by brave reasoning: "Is there any answer set containing a245 ?"

a234 ✤ ✬ ❋ a240 ✳ ✵ a234 ✤ ✬ ❋ a246 ✳ ✣ ✿ a247 ✜ ✦ ❂ ✬ a238 ✰ ❋ a240 ✰ ❋ a246 ✳ a223 a234 ✤ ✬ ❋ ✳ ✣ ✿ ✤ ✦ ❀ a235 ✬ ❋ ✰ ❋ a240 ✰ ❋ a246 ✰ ❋ a248 ✳ ✰ a234 ✤ ✬ ❋ a240 ✳ ✰ a234 ✤ ✬ ❋ a246 ✳ ✰ a234 ✤ ✬ ❋ a248 ✳ a223

As in [Cadoli et al., 1997] we assume that each product is produced by at most two companies and each company is jointly controlled by at most three companies to allow for an easier representation.

6 Benchmark Data

For 3SAT, we have randomly generated 3CNF formulas over ✑ variables using a tool by Selman and Kautz [Selman and Kautz, 1997]. For each size we generated 8 such instances, where we kept the ratio between the number of clauses and the number of variables at 4.3, which is near the cross-over point for random 3SAT [Crawford and Auton, 1996].

The instances for HAMPATH were generated using a tool by Patrik Simons which has been used to compare Smodels against SAT solvers (cf. [Simons, 2000]), and is available at http://tcs.hut.fi/Software/smodels/misc/ hamilton.tar.gz. For each problem size ✑ we generated 8 instances, always assuming node 1 as the starting node.

The blocksworld problems P3 and P4 have been employed in [Erdem, 1999] to compare ASP systems, and can be solved in 8 and 9 steps, respectively. We augmented these by problems P5 and P6 which require 11 and 12 steps, respectively. For each of these problems, we generated 8 random permutations of the input.

For STRATCOMP, finally, we randomly generated 8 instances for each problem size ✑ , with ✑ companies and ✑ products. Each company a249 is controlled by one to five companies, where the actual number of companies is uniform randomly chosen. On average there are 1.5 ❒ ✒ ✑ ➙ relations per company.

The benchmark data are available at http://www.dbai. tuwien.ac.at/proj/dlv/. All experiments were performed on an Athlon/750 FreeBSD 4.2 machine with 256MB of main memory. The binaries were produced with GCC 2.95.2.

7 Experimental Results and Conclusion

The results of our experiments are displayed in the graphs of Figures 3-6. In each graph, the horizontal axis reports a parameter representing the size of the instance. On the vertical axis, we report the average running time (expressed in seconds) over the 8 instances of the same size we have run (see previous section).

Remark. All heuristics have been implemented in a straightforward way, without optimizations, so the running times reported in the graph are meaningful only for comparing the relative efficiencies of the heuristics.

We have allowed a running time of 600 seconds for each problem instance. In the graphs, the line of an heuristic stops whenever some problem instance was not solved in the maximum allowed time. The following table displays, for each heuristic, the maximum instance-size where the heuristic could solve all problem instances in the maximum allowed time.

As expected, heuristic ➲ ❰ , the "native" heuristic of theDLV system, which does not combine the heuristic values of complementary atoms, is the worst in most cases. It does not terminate on the instance P6 of BW, it could not solve any of the benchmark instances of STRATCOMP (it does not appear at all in Figure 5), and stopped earlier than the others on 3SAT.

Heuristic ➲ ❑ , the extension of SATZ heuristic to ASP, behaves very well on average. On 3SAT, BW, and STRATCOMP, ➲ ❑ could solve all benchmark instances we have run. It is the fastest on BW and one of the two fastest on 3SAT. It shows a negative behaviour only on HAMPATH. In this problem, considering UnsupportedTrue literals seems to be crucial for the efficiency.

Heuristic ➲ a212 is surprisingly good compared to ➲ ❰ . It is a simple "balanced version" of heuristic ➲ ❰ (the heuristic values of the positive and of the negative literal are combined by sum). This simple extension to ➲ ❰ dramatically improves the performance. Indeed, heuristic ➲ a212 solves nearly all instances we ran (only on 3SAT it stopped a bit earlier than other heuristics). It is the best heuristic on STRATCOMP and, importantly, on HAMPATH, where it beats all other heuristics of a relevant factor.

The behaviour of heuristic ➲ ☎ , based on the minimization of the undefined atoms, is rather controversial. It behaves very well on 3SAT and BW, but it is extremely bad on HAMPATH, where it stops at 40 nodes already and is beaten even by the "naive" heuristic ➲ ❰ . This confirms that further studies are needed to find a proper extension of the heuristic of Smodels to the framework of disjunctive ASP.

Concluding, we observe that both heuristic ➲ ❑ and heuristic ➲ a212 , significantly improve the efficiency of the native heuristic ➲ ❰ of the DLV system. The dramatic improvement obtained by the simple change from ➲ ❰ to ➲ a212 , confirms even more the importance of a careful study of branching rules in ASP systems. This paper is only a first step in this field, we hope that further works will follow, for proposing new heuristics for ASP a251 and for better understanding the existing ones, in order to improve the efficiency of ASP systems.