We present a new ASP solver for ground ASP programs that builds upon related techniques, originally introduced for SAT solving, which have been extended to cope with disjunctive logic programs under the stable model semantics. We describe the key components of this solving strategy, namely: learning, restarts, heuristics based on look-back concepts, and backjumping. At the same time, we introduce a new heuristics based on a mixed approach between lookback and look-ahead techniques. Moreover, we present the results of preliminary experiments that we conducted in order to assess the impact of these techniques on both random and structured instances (used also in the last ASP Competition 2011). In particular, we compared our system with both DLV and ClaspD.
Answer Set Programming (ASP) [
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 [
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 [
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 [
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 p1 ∨ · · · ∨ pn :- q1, . . . , qj , not qj+1, . . . , not qm (1) where p1, . . . , pn, q1, . . . , qm are atoms and n ≥ 0, m ≥ j ≥ 0. The disjunction p1 ∨ · · · ∨ pn is the head of r, while the conjunction q1, . . . , qj , not qj+1, . . . , not qm 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 negationfree) 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 6= ∅, 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 . 3
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 [
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 [
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, 64, 128, . . . ) introduced in [
If the recursive call returned true, MG just returns true as well. If it returned false, the corresponding branch is inconsistent, bj level is set to the recursion level to backtrack or backjump to. Now, if bj level is less than the current level, this indicates a backjump, and we return. If not, then we have reached the level to go to, and the search continues.
bool MG (Interpretation& I, int& bj level ) int curr level = ++ bj level; if ( ! Propagate( I ) ) bj level = ResolveConflict(); return false; if ( “no atom is undefined in I” ) if ( CheckModel( I ) ) return true; else bj level = ResolveConflict(); return false; Select an undefined atom A using a heuristic; if ( MG( I ∪ {A}, bj level ) ) return true; if (bj level < curr level) return false; if ( MG( I ∪ {not A}, bj level ) ) return true; if (bj level < curr level) return false; return false; int ResolveConflict() int level = calculateFirstUIP(); learning(); if(inRestartSequence(numberOfConflict)) return 0; return level;
Fig. 1. Computation of answer sets 3.1
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 ha, ti 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 ha, ti to a node ha′ , t′ i whenever ha, ti 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 pi be the undefined atom in H(r). The following elements are added to G: a node hpi, T i; arcs (hqk, T i, hpi, T i) (k = 1, . . . , j); arcs (hqk, F i, hpi, T i) (k = j + 1, . . . , m); arcs (hpk, F i, hpi, T i) (k = 1, . . . , n and k 6= 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 ha, F i 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 (hL, F i, ha, F i) is added to G; otherwise, if L ∈ H(r), an arc (hL, T i, ha, F i) is added to G; otherwise, L ∈ B−(r) and thus an arc (hL, T i, ha, F i) 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: hb, T i (for each b ∈ B+(r)); hb, F i (for each b ∈ B−(r) ∪ H(r) \ {a}); for each new node hb, vi an arc (ha, T i, hb, vi). 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 (hL, F i, hb, vi) is added to G, otherwise, if L ∈ B−(r′ ) ∪ H(r′ ) \ {a}, an arc (hL, T i, hb, vi) is added to G; this is done for each new node hb, vi 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 ha, vi 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: (hb, F i, ha, vi) (for each b ∈ H(r) ∪ B−(r) \ {a}; (hb, T i, ha, vi) (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 ha, F i 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 (ha, F i, hc, F i) 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 (hL, F i, hc, F i) is added to G; otherwise, if L ∈ H(r), an arc (hL, T i, hc, F i) is added to G; otherwise, L ∈ B−(r) and thus an arc (hL, T i, hc, F i) is added to G. 3.2
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) [
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 [
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 [
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 selected2. 2 An atom removes a supporting rule if it makes the body of r false or the head of r true 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 r1–r4 and learned constraints c1–c2 (listed in chronological order): r1 : r2 :
a :- c. a ∨ b :- d.
r3 : r4 : a ∨ c :- e. e ∨ b :- c.
c1 : c2 : :- a, b. :- a, not c, d.
Moreover, let us assume a partial interpretation I1 = {a, not b} and the following counter values: cl(a) = 2, cl(not a) = 2, cl(b) = 1, cl(not b) = 0, cl(c) = 1, cl(not c) = 2, cl(d) = 3 and cl(not d) = 0.
Note that constraint c1 is satisfied because b is false. Thus, the first learned constraint (according to the chronological order) which is not satisfied is c2. Indeed, two undefined literals occur in the body of c2, 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 (r1 and r4) by setting c false, and one supporting rule (r3) would be removed by setting c true, for a total of 3 supporting rules removed. Concerning d, one supporting rule (r2) 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. 5
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. 5.1
In our experiments, we considered problems from the most recent ASP Competition
[
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 [
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 [
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 [
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. 5.2
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 [
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 [
Concerning other ASP solvers, we differ from non-native solvers like Cmodels3 [
Comparing our system with ClaspD (a disjunction-supporting version built upon
Clasp) more similarities can be found, as it includes similar techniques, e.g.
backjumping, 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 [
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 [