Introduction

Answer Set Programming (ASP) [1] is a declarative programming paradigm which has been proposed in the area of non-monotonic reasoning and logic programming. The idea of ASP is to represent a given computational problem by a logic program whose answer sets correspond to solutions, and then use a solver to find them [2].

The ASP language considered here allows disjunction in rule heads and nonmonotonic negation in rule bodies. These features make ASP very expressive; all problems in the second level of the polynomial hierarchy are indeed expressible in ASP [3]. Therefore, ASP is strictly more expressive than SAT (unless P = N P ). Despite the intrinsic complexity of the evaluation of ASP, after twenty years of research many efficient ASP systems have been developed (e.g. [4][5][6][7][8][9][10][11]). The availability of robust implementations made ASP a powerful tool for developing advanced applications in the areas of Artificial Intelligence, Information Integration, or Knowledge Management; for example, ASP has been used in applications for team-building [12], semantic-based information extraction [13], and e-tourism [14]. These applications of ASP have confirmed the viability of the use of ASP. Nonetheless, the interest in developing more effective and faster systems is still a crucial and challenging research topic, as witnessed by the results of the ASP Contests series [15][16][17].

This paper provides a contribution in the aforementioned context. In particular, we provide a preliminary report on the development of a new ASP solver for propositional programs called wasp. The new system is inspired by several techniques that were originally introduced for SAT solving, like the Davis-Putnam-Logemann-Loveland (DPLL) backtracking search algorithm [18], clause learning [19,20], backjumping [21,22], restarts [23], and conflict-driven heuristics [24] in the style of Berkmin [25]. The mentioned SAT-solving methods have been adapted and combined with state-of-the-art pruning techniques adopted by modern native disjunctive ASP systems [4]. In particular, the role of Boolean Constraint Propagation in SAT-solvers (based on the simple unit propagation inference rule) is taken by a procedure combining a set of inference rules. Those rules combine an extension of the well-founded operator for disjunctive programs with a number of techniques based on ASP program properties (see, e.g., [26]). Moreover, wasp uses a new branching heuristics tailored for ASP programs, which is based on a mixed approach between Berkmin-like heuristics and look-ahead, which takes into account minimality of answer sets (a requirement not present in SAT solving). Finally, stable model checking, which is a co-NP-complete problem for disjunctive logic programs, is efficiently implemented relying on the rewriting method of [27], by calling Minisat [28] as suggested by [29].

In the following, after briefly introducing ASP, we describe the new system wasp. We start from the solving strategy and present the design choices regarding propagation, constraint learning, restarts, and the new heuristics. Moreover, we present the results of some experiments conducted for assessing the impact of these techniques, on both random and structured instances; some of these instances had been used in the last ASP Competition [17]. In particular, we compared our system with both DLV and ClaspD. The obtained results are encouraging: the new prototype system is already competitive with state-of-the-art solvers, even if there is still room for improvements in both the implementation (e.g., through the optimization and tuning of data structures and heuristic parameters), and in the supported language features (notably aggregates and weak constraints).

Preliminaries

In this paper we consider propositional programs, so an atom p is a member of a countable set A. A literal is either an atom p (a positive literal), or an atom preceded by the negation as failure symbol not (a negative literal). A rule r is of the form

p 1 ∨ • • • ∨ p n :-q 1 , . . . , q j , not q j+1 , . . . , not q m (1)

where p 1 , . . . , p n , q 1 , . . . , q m are atoms and n ≥ 0, m ≥ j ≥ 0. The disjunction p 1 ∨ • • • ∨ p n is the head of r, while the conjunction q 1 , . . . , q j , not q j+1 , . . . , not q m is the body of r. Moreover, H(r) denotes the set of head atoms, while B(r) denotes the set of body literals. We also use B + (r) and B − (r) for denoting the set of atoms appearing in positive and negative body literals, respectively, and At(r) for the set

H(r)∪B + (r)∪ B − (r). A rule r is normal (or disjunction-free) if |H(r)| ≤ 1, positive (or negation- free) if B − (r) = ∅, a fact if both B(r) = ∅ and |H(r)| = 1, a constraint if |H(r)| = 0.

A program P is a finite set of rules; if all rules in it are positive (resp. normal), then P is a positive (resp. normal) program. Let L denote the complement of a literal L, i.e., a = not a and not a = a for an atom a. We extend this to sets of literals and will use S for denoting {L | L ∈ S}. An interpretation I is a subset of A ∪ A. An interpretation I is total if for each a ∈ A either a ∈ I or not a ∈ I; otherwise, I is partial. An interpretation I is inconsistent if there exists a ∈ A such that {a, not a} ⊆ I; otherwise, I is consistent. An interpretation thus associates each ASP structure (atom, literal, head or body) with a truth value in the set {T , F, U }, which extends to H(r) and B(r) in the standard way.

An interpretation I satisfies a rule r ∈ P if H(r) is true w.r.t. I whenever B(r) is true w.r.t. I, while I violates r if H(r) is false but B(r) is true. A total interpretation I is a model of a program P if I satisfies all the rules in P. Given an interpretation I for a program P, the reduct of P w.r.t. I, denoted by P I , is obtained by deleting from P all the rules r with B − (r) ∩ I = ∅, and then by removing all the negative literals from the remaining rules. The semantics of a program P is given by the set AS(P) of the answer sets (or stable models) of P, where a total interpretation M is an answer set (or stable model) for P if and only if M is a subset-minimal model of P M .

Model Generator

In this section we sketch the main model generator function MG (cf. Fig. 1), which is able to perform learning and restart techniques. MG is similar to the Davis-Putnam procedure in SAT solvers. For reasons of presentation, we have considerably simplified the procedure in order to focus on its main ideas. For example, the version described here computes only one answer set, but modifying it to compute all or n stable models is straightforward.

In the sequel, P will refer to the input program. Initially, the MG function is invoked with I = ∅, and bj level = −1 (but it will become 0 immediately), and the global variable numberOfConflicts is set to 0. MG returns true if the program P has an answer set, and sets I to the computed answer set; otherwise it returns false.

MG first calls a function Propagate, which extends I with those literals that can be deterministically inferred, and keeps track of the reason of each inference by building a representation of the so-called implication graph [24]. Propagate is similar to unit propagation as employed by SAT solvers, but exploits the peculiarities of ASP for making further inferences (e.g., it uses the knowledge that every answer set is a minimal model). Propagate, described in more detail in Section 3.1, returns false if an inconsistency (or conflict) is detected (i.e., the complement of a true literal is inferred to be true), true otherwise.

If Propagate returns true and no undefined atom is left in I, MG invokes CheckModel to verify that the current total interpretation is also an answer set; the CheckModel function implements the techniques described in [27]. If the stability check succeeds, MG returns true. 1 If Propagate returned true but I is still partial, an undefined literal L is selected according to a heuristic criterion and MG is recursively called. The atom L corresponds to a branching variable in SAT solvers.

If Propagate returns false, function ResolveConflict is called, which calculates the Unique Implication Point (UIP) of the implication graph (see Section 3.1), and exploits it to learn a constraint representing the inconsistency (see Section 3.2), which is added to the input program. As a by-product, ResolveConflict returns the recursion level to go back to (backjumping) in order to continue the search in the first branch of the search that is free of the just-detected conflict.

After a certain number of conflicts, ResolveConflict may decide to restart the entire search, if the total number of conflicts found during the search reached a certain threshold. It is important to note that after each restart MG works on a program composed of the original input program and the learned constraints. Our restart policy is based on the sequence of thresholds (32, 32, 64, 32, 32,

Propagation

WASP implements a number of deterministic inference rules for pruning the search space during the computation of stable models. These inference rules are named forward inference, Kripke-Kleene negation, contraposition for true heads, contraposition for false heads and well-founded negation. All of these inference rules are briefly described in this section.

During the propagation of deterministic inferences, implication relationships among atoms are stored in a graph G named Implication Graph. This graph has a node a, t for each atom a and truth value t such that a has been assigned t. Each node of the graph is associated with a decision level, which is set to the level of the backtracking tree when t is assigned to a. Moreover, G has a directed arc connecting a node a, t to a node a ′ , t ′ whenever a, t is one of the reasons that lead to the derivation of the truth value t ′ for the atom a ′ . Note that G will contain at most one node for each atom of the program, unless a conflict is derived. The way of building G is described below.

Forward Inference. This is essentially modus ponens. When the body of a rule r is true w.r.t. the current partial interpretation, and all but one of the head atoms of r are false and the remaining one is undefined, then there is only one way to satisfy r, by deriving the remaining head atom as true.

Concerning the Implication Graph G, it is updated as follows. Let r be of the form (1) and let p i be the undefined atom in H(r). The following elements are added to G: a node p i , T ; arcs

( q k , T , p i , T ) (k = 1, . . . , j); arcs ( q k , F , p i , T ) (k = j + 1, . . . , m); arcs ( p k , F , p i , T ) (k = 1, . . . , n and k = i).

Kripke-Kleene Negation. This derives negative information by using supportedness, the fact that each atom a which is true in a stable model M must occur in at least one rule r such that B(r) is true w.r.t. M and a is the only atom in H(r) which is true w.r.t. M . Hence, atoms with no candidate supporting rules can be derived to be false. So, if all of the rules r such that a ∈ H(r) are satisfied because of a false body literal or because of a true head atom different from a, atom a is inferred as false.

Concerning G, a node a, F is introduced. Moreover, for each rule r with a ∈ H(r), let L be the first literal (in chronological order of derivation) that satisfied r.

If L ∈ B + (r), an arc ( L, F , a, F ) is added to G; otherwise, if L ∈ H(r), an arc ( L, T , a, F ) is added to G; otherwise, L ∈ B − (r) and thus an arc ( L, T , a, F ) is added to G.

Contraposition for True Heads. Supportedness is also used by this inference rule: If an atom a that has been derived as true has only one candidate supporting rule r, the truth of all literals in B(r) and the falsity of all atoms in H(r) different from a are inferred.

Concerning G, the following new nodes and arcs are introduced: b,

T (for each b ∈ B + (r)); b, F (for each b ∈ B − (r) ∪ H(r) \ {a}); for each new node b, v an arc ( a, T , b, v ). Moreover, for each rule r ′ such that a ∈ H(r ′ ), let L be the first literal (in chronological order of derivation) that satisfied r ′ . If L ∈ B + (r ′ ), an arc ( L, F , b, v ) is added to G, otherwise, if L ∈ B − (r ′ ) ∪ H(r ′ ) \ {a}, an arc ( L, T , b, v

) is added to G; this is done for each new node b, v introduced by the application of the inference rule for r.

Contraposition for False Heads. This inference rule is essentially modus tollens. When for a rule r all head atoms are false, the only way to satisfy r is by having a false body. In case all but one body literals of r are true, falsity of the remaining L is inferred.

Concerning G, a node a, v is added, where a is the atom in L and v = F if L = a or v = T if L = not a. Moreover, the following arcs are added to G:

( b, F , a, v ) (for each b ∈ H(r) ∪ B − (r) \ {a}; ( b, T , a, v ) (for each b ∈ B + (r) \ {a}).

Well-founded Negation. Unfounded sets are sets of unsupported or self-supporting atoms, that is, atoms that can have supporting rules only if their own truth is assumed. It is well-known that unfounded sets are disjoint from stable models, which allows for assuming the falsity of all the atoms that belong to some unfounded set. Hence, after the propagation process has been carried out, wasp determines the set X of all the atoms belonging to some unfounded set and derives the falsity of these atoms; if this set is empty, the rule does not apply.

In order to model such a lack of external supporting rules, a number of nodes and arcs is added to G. For each a ∈ X, a node a, F is added. Arcs are introduced according to the following schema: Let C be the set of atoms in X that were previously derived as true, and let c be a randomly selected atom in C. For each a ∈ X \ C, an arc ( a, F , c, F ) is added to G. Moreover, for each b ∈ C \ {c} and for each rule r such that b ∈ H(r), let L be the first literal (in chronological order of derivation) that satisfied r.

If L ∈ B + (r), an arc ( L, F , c, F ) is added to G; otherwise, if L ∈ H(r), an arc ( L, T , c, F ) is added to G; otherwise, L ∈ B − (r) and thus an arc ( L, T , c, F ) is added to G.

Constraint Learning

Constraint learning means acquiring information that avoids arriving again at a conflict that was already encountered during the search. Our learning schema is based on the concept of the first Unique Implication Point (UIP) [24]. A node n in the Implication Graph is a UIP for a decision level d iff all paths from the literal chosen at the level d to a conflict atom pass through n. Intuitively, a UIP is the most concise reason for the conflict of a certain decision level. We calculate the first UIP only for the decision level of the conflict. By definition the chosen literal is always a UIP, but since several UIPs may exist, we calculate the UIP closest to the conflict, the first UIP. After each conflict at the decision level d, a constraint is learned that contains the first UIP and all atoms of lower levels that are connected to a node between the first UIP and the conflict.

Since the number of learned constraints may become exponential in the size of the program, we adopt the standard technique of expiring learned constraints. Our policy is similar to Minisat's [28]: Each learned constraint has an activity value, measuring how much it is involved in conflicts. If a learned constraint has recently been used for propagation, we do not delete it. If the number of learned constraints is greater than one third of the input program, then we delete half of the learned constraints. Moreover, we also delete all learned constraints with an activity value lower than a threshold value.

Clearly, a crucial issue in the Model Generator function in Fig. 1 is the selection of a literal when all inferences have been made and there are still undefined atoms. It is clear that the correctness of the algorithm reported in Fig. 1 does not depend on the strategy in which this selection is made, but making a "good" choice is very important for practical efficiency. However, strategies which perform very well on some domains may perform very bad for other domains, and of course an optimal strategy seems unlikely to be found. For this reason, some heuristic must be adopted; the quality of the adopted heuristic can often only be assessed empirically.

Heuristics can be classified in two main classes, look-ahead based and look-back based. Look-ahead heuristics estimate the effects of assigning a specific truth value to a given undefined atom, for any truth value and for a set of undefined atoms (which might also be the set of all undefined atoms). Once the effects of all candidate assumptions have been estimated, a look-ahead heuristic selects the most promising undefined atom and truth value according to some function. Look-back heuristics, instead, rely on the information on conflicts derived in the computation so far.

The heuristic implemented in wasp is based on a mixed approach. In fact, a lookback approach is used for selecting an undefined atom and, in some cases, a look-ahead step is performed for choosing the truth value for the selected atom. More specifically, statistics on previously detected conflicts are analyzed and atoms that have caused most conflicts are preferred. Also the "age" of conflicts is taken into account in the selection process, and more recent conflicts are given greater importance. This approach has already been adopted in the context of SAT, for example in the BerkMin solver [31]. In this sense, our heuristic could be seen as an extension of the heuristic implemented in BerkMin to the framework of ASP.

In the remainder of this section, we will provide a few additional details on the strategy adopted by wasp for selecting undefined atoms and truth values to be assumed during the computation of stable models.

A counter cl(L) is associated with each literal L. Initially, all of these counters are set to zero. When a new constraint is learned, counters for all literals occurring in the constraint are increased by one. In this way, wasp keeps track of those literals occurring more frequently in learned constraints. Moreover, counters are also updated during the computation of the First UIP: If a literal L is traversed in the implication graph, the associated counter cl(L) is increased by one. In this way, those literals that mainly caused the derivation of a conflict are identified. Finally, every 100 conflicts, all these counters are divided by 4 (this is an experimentally determined parameter), which gives more importance to recently active literals. Our heuristic will first select an atom and then a truthvalue for this atom. To this end, we will use cv(a) := cl(a) + cl(not a), for each propositional atom a.

Learned constraints are stored in chronological order. The atom selection is first restricted to those undefined atoms that occur in the first (if any) learned constraint r with undefined body. Among those, the atom with the highest cv(•) value is chosen. In case of ties, the atom removing the highest number of supporting rules is selected 2 .

If two or more atoms remove the same number of supporting rules, the first processed atom is chosen. In this way, the chances of achieving a conflict increases, and this may help the learning process. If no learned constraints with undefined body exist, the undefined atom with the highest cv(•) value is selected. In case of ties, the first processed atom is selected. If there are no learned constraints, e.g. in the beginning of the solving process, the atom occurring in most rules is picked.

After selecting an atom a according to the strategy described above, wasp chooses a truth value for a. For this purpose, we only distinguish two cases, namely whether a learned constraint r with undefined body exists or not. If a learned constraint r with undefined body exists, additional counters are considered for choosing a truth value for a. In particular, a counter gcl(L) is associated with each literal L for estimating the global contribution of L to all of the conflicts derived during the computation. For each literal L, gcl(L) is initially set to zero and increased whenever cl(L) is increased. The difference to cl(L) is that gcl(L) is never decreased, that is, gcl(L) is unchanged when cl(L) is divided by 4. Thus, in this case wasp assumes the truth of a if gcl(a) > gcl(not a); otherwise, if gcl(a) ≤ gcl(not a), the falsity of a is assumed. It is important to emphasize that this counter is not used when the atom removing the highest number of supporting rules was chosen. In fact, in this case the literal removing the highest number of supporting rules is picked. In the other case, that is, if all learned constraints have false bodies, a look-ahead step is performed and both a and not a are propagated (i.e., the function Propagate is invoked). The literal appearing in more rules is propagated before the other one. During these propagations, wasp estimates the impact of the two assumptions on the computation of answer sets. In particular, wasp counts the number of inferred atoms and the number of rules that have been satisfied by the two propagations. The truth of a is then assumed if the impact of the propagation of a is greater than the impact of the propagation of not a, while a is assumed to be false in other case, that is, if the impact of the propagation of not a is greater than the impact of the propagation of a. If the impact is equal then a is assumed to be false. It is important to note that when a conflict is derived in one of the two propagations, a deterministic inference is determined. That is, if a conflict is derived during the propagation of a, the falsity of a is determined, while the truth of a is determined whenever a conflict is derived during the propagation of not a.

Example 1. We will now provide an example of the way our heuristic works. In the example, we will consider the following rules r 1 -r 4 and learned constraints c 1 -c 2 (listed in chronological order): Note that constraint c 1 is satisfied because b is false. Thus, the first learned constraint (according to the chronological order) which is not satisfied is c 2 . Indeed, two undefined literals occur in the body of c 2 , namely not c and d. We then consider the counters cv(c) = cl(c) + cl(not c) and cv(d) = cl(d) + cl(not d), which are both equal to 3. The heuristics then examines the removal of supporting rules:

Two supporting rules would be removed (r 1 and r 4 ) by setting c false, and one supporting rule (r 3 ) would be removed by setting c true, for a total of 3 supporting rules removed. Concerning d, one supporting rule (r 2 ) would be removed by setting d false, and no rules would be removed by setting d true, for a total of 1 supporting rule removed. Therefore c removes more supporting rules than d, and therefore our heuristic will choose c and it first will be set to false.

Experiments

In this section we report the results of an experimental analysis we carried out in order to assess the performance of wasp. As a comparison, we also ran the suite of our benchmarks on two state-of-the-art ASP solvers, namely DLV and ClaspD;3 a discussion on the difference between wasp and these two systems is provided in Section 6.

The machine used for the experiments is a two-processor Intel Xeon "Woodcrest" (quad core) 3GHz machine with 4MB of L2 Cache and 4GB of RAM, running Debian GNU Linux 4.0. As our ASP system focuses on the Model Generation phase, only the time for evaluating ground programs (previously produced by the DLV instantiator from the original non-ground instances) have been considered. In the following, we briefly describe both benchmark problems and data.

Benchmark Problems and Data

In our experiments, we considered problems from the most recent ASP Competition [17] and other problems which have already been employed for assessing performance of the ASP solver DLV [4]. Our experiments consist of 36 instances in 15 different domains. The instances and encodings are those that were used in the competitions or in the other publicly available suites. In the following we describe the benchmark problems.

Labyrinth. Ravensburger's Labyrinth game deals with guiding an avatar through a dynamically changing labyrinth to certain fields. A solution is represented by pushes of the labyrinth's rows and columns such that the avatar can reach the goal field (which changes its location when pushed) from its starting field (which also changes its location when pushed) by a move along some path after each push. Knight-tour. Given a chessboard, the problem is to find a tour for a knight piece that starts at any square, travels all squares, and comes back to the origin, following the knight move rules of chess.

Graph coloring. Given an undirected graph and a set of n colors, we are interested in checking whether there is an assignment of colors to nodes such that no adjacent nodes share the same color.

Maze-Generation.

A maze is an m × n grid, in which each cell is empty or a wall and two distinct cells on the edges are indicated as entrance and exit, satisfying the following conditions: (1) each cell on the edge of the grid is a wall, except entrance and exit that are empty; (2) there is no 2 × 2 square of empty cells or walls; (3) if two walls are on a diagonal of a 2 × 2 square, then not both of their common neighbors are empty; (4) no wall is completely surrounded by empty cells; (5) there is a path from the entrance to every empty cell. The problem has been proved to be NP-complete in [32].

Strategic Companies. Strategic companies is a well-known N P N P -complete problem that has often been used for system comparisons, also in the previous ASP Competitions. In the Strategic Companies problem, a collection C = c 1 , . . . , c m of companies is given, for some m ≥ 1. Each company produces some goods in a set G, and each company c i in C is possibly controlled by a set of owner companies O i (where O i is a subset of C, for each i = 1, . . . , m). In this context, a set C ′ of companies (i.e., a subset of C) is a strategic set if it is minimal among all the sets satisfying the following conditions: (i) Companies in C' produce all goods in G; (ii) if O i is a subset of C ′ , the associated company c i must belong to C ′ (for each i = 1, . . . , m). We considered a random instance having 7500 companies and 22500 products.

2-QBF.

The problem consists of checking the validity of a quantified boolean formula Φ = ∃X∀Y φ, where X and Y are disjoint sets of propositional variables and φ = C 1 ∨ . . . ∨ C k is a DNF on variables X and Y . In our benchmark, we used the transformation from 2-QBF to ASP presented in [4], which is based on a reduction presented in [33]. The instance considered has 1000 universal variables, 20 existential variables, 10000 clauses, and is a 5-DNF.

Prime Implicants. In Boolean logic, an implicant is a "covering" (sum term or product term) of one or more minterms (a product term in which each of the n variables appears once) in a sum of products, or, maxterms (a sum term in which each of the n variables appears once) in a product of sums, of a boolean function. Formally, a product term P in a sum of products is an implicant of the Boolean function F if P implies F . A prime implicant of a function is an implicant that cannot be covered by a more general (more reduced -meaning with fewer literals) implicant. The instance we considered consists of 180 variables and 774 clauses.

3-Colorability.

This well-known problem asks for an assignment of three colors to the nodes of a graph, in such a way that adjacent nodes always have different colors. One simplex graph was generated with the Stanford GraphBase library [34], by using the function simplex(600, 600, −2, 0, 0, 0, 0). Another ladder graph was generated having 11998 edges, and 8000 nodes.

Hamiltonian Cycle. A classical NP-complete problem in graph theory, which can be expressed as follows: given a directed graph G = (V, E) and a node a ∈ V of this graph, does there exist a path in G starting at a and passing through each node in V exactly once? One random graph was generated with the Stanford GraphBase library [34], by using the function random graph(85, 700, 0, 0, 0, 0, 0, 1, 1, 33), having 700 edges and 85 nodes; the other instances has been generating using the function random graph(80, 456, 0, 0, 0, 0, 0, 1, 1, 33), having 456 edges and 80 nodes.

Blocks World. Blocks world is one of the most famous planning domains in artificial intelligence. We have a set of cubes (blocks) sitting on a table. The goal is to build one or more vertical stacks of blocks. The catch is that only one block may be moved at a time: it may either be placed on the table or placed atop another block. Because of this, any blocks that are, at a given time, under another block cannot be moved. The four instances considered are by Esra Erdem and taken from the ccalc homepage (http://www.cs.utexas.edu/users/tag/cc/).

3SAT. The satisfiability problem (SAT) is a decision problem, whose instance is a propositional formula. The question is: given the formula, is there some assignment of T and F values to the variables that will make the entire expression true? SAT is the best-known NP-complete problem. 3-satisfiability is a special case of SAT, where each formula is a CNF in which each clause contains exactly three literals. We considered two random instances with 280 variables and 1204 clauses.

Towers of Hanoi. The Towers of Hanoi (ToH) problem has three pegs and n disks. Initially, all n disks are on the left-most peg. The goal is to move all n disks to the rightmost peg with the help of the middle peg. The rules are: (1) move one disk at a time;

(2) only the top disk on a peg can be moved; (3) a larger disk cannot be placed on top of a smaller one. The instance we considered has 6 disks, and we check whether a plan of length 64 exists.

Ramsey Numbers. The Ramsey number ramsey(k, m) is the least integer n such that, no matter how the edges of the complete undirected graph (clique) with n nodes are colored using two colors, say red and blue, there is a red clique with k nodes (a red k-clique) or a blue clique with m nodes (a blue m-clique).The encoding of this problem consists of one rule and two constraints. For the experiments, the problem was considered of deciding whether, for k = 3, m = 7, n = 21, and for k = 4, m = 6, n = 26, n is the Ramsey number ramsey(k, m). n-Queens. The 8-queens puzzle is the problem of putting eight chess queens on an 8x8 chessboard such that none of them is able to capture any other using the standard chess queen's moves. The n-queens puzzle is the more general problem of placing n queens on an nxn chessboard (n ≥ 4). The instance considered is for n = 23.

Timetabling. The problem is determining a timetable for some university lectures that have to be given in one week to some groups of students. The timetable must respect a number of given constraints concerning availability of rooms, teachers, and other issues related to the overall organization of the lectures.

Experimental Results

The results of our experiment are summarized in Table 1, reporting, for each considered instance the execution times in seconds elapsed by each considered system. For each instance of the benchmark problems, we allowed a maximum of 600 seconds of execution time. Timeouts are indicated by means of the word TIME in Table 1. In the last rows we report, for each system, the total number of solved instances, the average execution time for solving all the 36 considered instances (timeouts are counted 600s each), and the number of instances in which each solver resulted to be the fastest. Overall, the results of the preliminary experimental analysis are encouraging: the performance of wasp is comparable to ClaspD (same number of wins and cumulative average time), and it is often faster than DLV (only 9 wins vs 15 of wasp and ClaspD). In more detail, for the Labyrinth problem wasp was able to solve four instances out of five in the allowed time, while the other systems solved all five instances; the system is always outperformed by the competitors, except for one instance in which it is the best performer. Regarding the Knight Tour problem, wasp always outperforms the competitor systems, solving the hardest instance (on which DLV timed out) in only 7, 44 seconds compared to 179, 48 seconds for ClaspD. Concerning the Graph Coloring problem, wasp was slower than ClaspD, but solved one instance more than DLV. Also for the Maze Generation benchmarks, wasp was slightly slower than ClaspD, but always outperformed DLV. Considering the other benchmarks, wasp outperformed the other two ASP solvers on 2QBF, Ramsey Numbers, N-Queens, School Timetabling, 3Colorability, and Towers of Hanoi. In the remaining benchmarks, the system remains competitive, with the single exception of Strategic Companies. For this, we hypothesize that a reason might be that wasp does not implement yet a model-checking-driven backjumping technique, which proved to be very effective on this particular benchmark [35].

Related Work and Conclusion

In this paper we provided a preliminary report on a new ASP solver for propositional programs called wasp. The new system is inspired by several techniques that were originally introduced for SAT solving, like the Davis-Putnam-Logemann-Loveland (DPLL) backtracking search algorithm [18], clause learning [19,20], backjumping [21,22], restarts [23], and conflict-driven heuristics [24] in the style of Berkmin [25]. Actually, some of the techniques adopted in wasp, including backjumping and look back heuristics were first introduced for Constraint Satisfaction [21,22,36] and successively successfully applied in SAT [37,38,25,24] and QBF solving [39][40][41][42]. Some of these tech-niques were already adapted in modern non-disjunctive ASP solvers like Smodels cc [43,44], Clasp [8], and solvers supporting disjunction like CModels3 [10], GnT [45], and DLV [46,47].

Concerning other ASP solvers, we differ from non-native solvers like Cmodels3 [10], in the sense that we do not rely on a rewriting into a propositional formula and an external SAT solver, but use native ASP techniques. Among native solvers, similarities with DLV [4] can be found in the propagation rules, in the computation of the greatest unfounded set, and in the model checking technique. However, we clearly differ from DLV as it does not implement many of the look-back techniques borrowed from CP and SAT. The prototypical version of DLV presented in [46] and extended in [47], implements backjumping and some forms of look back heuristics, but it does not include clause learning, restarts, and does not use an implication graph for determining the reasons of the conflicts. Similar considerations hold for GnT [45], which, as DLV, implements a systematic backtracking without learning and look-ahead heuristics.

Comparing our system with ClaspD (a disjunction-supporting version built upon Clasp) more similarities can be found, as it includes similar techniques, e.g. ing, clause learning, restarts, and look-back heuristics. There are nonetheless several differences with wasp. First of all, wasp performs the unfounded set checking by means of the well-founded operator, while ClaspD relies on the computation of loop formulas. Moreover, ClaspD implements an alternative version of the implication graph that is more similar to SAT solvers, since it relies on unit propagation of nogoods (minimality is handled via loop formula learning). Furthermore, ClaspD, as wasp, adopts a branching heuristics based on Berkmin [25]; however, wasp extends the original Berkmin heuristics by exploiting a lookahaed technique in place of the "two" function calculating the number of binary clauses in the neighborhood of literal L, together with an additional criterion based on minimality of answer sets. In particular, to deal with the case of two atoms with the same heuristic value, wasp chooses the atom that introduces the maximum number of unsatisfied supporting rules.

It is worth pointing out that the implementation of wasp is still in a preliminary phase, yet the results obtained up to now are encouraging. Our system is able to compete with the state-of-the-art solvers, and even outperform them in some of the considered benchmarks.

Concerning future work, we plan to extend the prototypical system by introducing new language constructs such as aggregates [48,49] and weak constraints [50], which are currently missing from wasp. Moreover, the current implementation can be improved in several respects: parameter tuning of the heuristics, fine tuning of the source code, a model-checking-driven backjumping [35] as well as support for multi-threading are also planned.