Conflict-Driven Answer Set Solving

1 Introduction

Answer set programming (ASP; [Baral, 2003]) has become an attractive tool for knowledge representation and reasoning. Although the corresponding solvers are highly optimized (cf. [Simons et al., 2002; Leone et al., 2006]), their performance does not match the one of state-of-the-art solvers for satisfiability checking (SAT; [Mitchell, 2005]). However, computational mechanisms of SAT and ASP solvers are not that far-off. This can, for instance, be seen on the success of SAT-based ASP solvers assat [Lin and Zhao, 2004] and cmodels [Giunchiglia et al., 2006]. But despite the close relationship to SAT and, more generally, constraint processing (CSP; [Dechter, 2003]), state-of-the-art look-back techniques from these areas, like backjumping, conflict-driven learning, and restarts, are not yet established in genuine ASP solvers. In fact, recent approaches to adopt such techniques [Ward and Schlipf, 2004; Ricca et al., 2006; Lin et al., 2006] are rather implementation-specific and lack generality.

We address this deficiency by introducing a new computational approach to ASP solving, centered around the CSP concept of a nogood. Apart from the fact that this allows us to easily integrate solving technology from the areas of CSP and SAT, e.g., conflict-driven learning, backjumping, watched literals, etc., it also provides us with a uniform representation of inferences from logic program rules, unfounded sets, as well as nogoods learned from conflicts.

∗Affiliated with the School of Computing Science at Simon Fraser University, Canada, and IIIS at Griffith University, Australia.

After establishing the formal background, we provide in Section 3 a constraint-based specification of ASP solving in terms of nogoods. Based on this uniform representation, we develop in Section 4 algorithms for ASP solving that rely on advanced CSP and SAT techniques. Notably, our solving procedure is centered around conflict-driven learning and backjumping. In Section 5, we describe our new ASP solver clasp, implementing our approach. We finally provide empirical results demonstrating the competitiveness of clasp.

2 Background

Given an alphabet P, a (normal) logic program is a finite set of rules of the form p0 ← p1, . . . , pm, not pm+1, . . . , not pn where 0 ≤ m ≤ n and pi ∈ P is an atom for 0 ≤ i ≤ n. A body literal is an atom p or its negation not p. For a rule r, let head(r) = p0 be the head of r and body(r) = {p1, . . . , pm, not pm+1, . . . , not pn} be the body of r. The set of atoms occurring in a logic program Π is denoted by atom(Π). The set of bodies in Π is body(Π) = {body(r) | r ∈ Π}. For regrouping rule bodies sharing the same head p, define body(p) = {body(r) | r ∈ Π, head(r) = p}. In ASP, the semantics of a programΠ is given by its answer sets, being total well-founded models of Π. For a formal introduction to ASP, we refer the reader to [Baral, 2003].

A Boolean assignment A over a domain, dom(A), is a sequence (σ1, . . . , σn) of signed literals σi of form Tp or Fp for p ∈ dom(A) and 1 ≤ i ≤ n; Tp expresses that p is true and Fp that it is false. (We omit the attribute signed for literals whenever clear from the context.) We denote the complement of a literal σ by σ, that is, Tp = Fp and Fp = Tp. We let A ◦ B denote the sequence obtained by concatenating assignments A and B. We sometimes abuse notation and identify an assignment with the set of its contained literals. Given this, we access true and false propositions in A via AT = {p ∈ dom(A) | Tp ∈ A} and AF = {p ∈ dom(A) | Fp ∈ A}.

For a canonical representation of constraints, we use the CSP concept of a nogood. In our setting, a nogood is a set {σ1, . . . , σn} of signed literals, expressing a constraint violated by any assignment containing σ1, . . . , σn. An assignment A such that AT ∪ AF = dom(A) and AT ∩ AF = ∅ is a solution for a set Δ of nogoods, if δ ̸⊆ A for all δ ∈ Δ.

For a nogood δ, a literal σ ∈ δ, and an assignment A, we say that σ is unit-resulting for δ wrt A, if (1) δ \ A = {σ}

and (2) σ ̸∈ A. By (1), σ is the single literal from δ that is not contained in A. This implies that a violated constraint does not have a unit-resulting literal. Condition (2) makes sure that no duplicates are introduced: If A already contains σ, then it is no longer unit-resulting. For instance, literal Fq is unit-resulting for nogood {Fp, Tq} wrt assignment (Fp), but neither wrt (Fp,Fq) nor wrt (Fp,Tq). Note that our notion of a unit-resulting literal is closely related to the unit clause rule of DPLL (cf. [Mitchell, 2005]). For a set Δ of nogoods and an assignment A, we call unit propagation the iterated process of extending A with unit-resulting literals until no further literal is unit-resulting for any nogood in Δ.

3 Nogoods of Logic Programs

Inferences in ASP rely on atoms and program rules, which can be expressed by using atoms and bodies. For a program Π, we thus fix the domain of assignments A to dom(A) = atom(Π) ∪ body(Π). Such a hybrid approach may result in exponentially smaller search spaces [Gebser and Schaub, 2006]; it moreover allows for an adequate representation of nogoods, as we show in the sequel.

Our approach is guided by the idea of Lin and Zhao [2004] and decomposes ASP solving into (local) inferences obtainable from the Clark completion of a program [Clark, 1978] and those obtainable from loop formulas. We begin with nogoods capturing inferences from the Clark completion.

The body of a rule is true if all its body literals are true. Conversely, some of its literals must be false if the body is false. For a body β = {p1, . . . , pm, not pm+1, . . . , not pn}, the following nogood captures this:

Intuitively, δ(β) is a constraint enforcing the truth of body β, or the falsity of a contained literal. E.g. for body {x, not y}, we obtain δ({x, not y}) = {F{x, not y}, Tx, Fy}.

Additionally, a body must be false if one of its literals is false. And conversely, all contained literals must be true if the body is true. For β = {p1, . . . , pm, not pm+1, . . . , not pn}, this is reflected by the following set of nogoods:

Taking again body {x, not y}, we obtain Δ({x, not y}) = { {T{x, not y}, Fx}, {T{x, not y}, Ty} }.

Nogoods induce a set of clauses, which can be used for investigating the logical contents of the underlying inferences. Given a program Π, we associate a nogood δ = {Tp1, . . . ,Tpm,Fpm+1, . . . ,Fpn} with the clause γ(δ) = {¬q1, . . . ,¬qm, qm+1, . . . , qn} where qi = pi, if pi ∈ atom(Π), and qi = pβ, if pi = β ∈ body(Π), for 1 ≤ i ≤ n; and define Γ(Δ) = {γ(δ) | δ ∈ Δ} for a set of nogoods Δ. For the bodies of Π, we obtain the following correspondence.

Proposition 3.1 Let Π be a logic program.

The set of clauses

{γ(δ(β)) | β ∈ body(Π)} ∪ {γ ∈ Γ(Δ(β)) | β ∈ body(Π)} is logically equivalent to the propositional theory

This result captures the intuition that a body should be equivalent to the conjunction of its body literals.

We now come to inferences primarily aiming at atoms. An atom p must be true if some body in body(p) is true. Conversely, all elements of body(p) must be false if p is false. For body(p) = {β1, . . . , βk}, we get the nogoods:

For example, for an atom x with body(x) = {{y}, {not z}}, we get Δ(x) = { {Fx, T{y}}, {Fx, T{not z}} }.

Finally, an atom p must be false if all elements of body(p) are false. And conversely, some body in body(p) must be true if p is true. For body(p) = {β1, . . . , βk}, this is reflected by the following nogood:

Taking once more atom x with body(x) = {{y}, {not z}}, we obtain δ(x) = {Tx, F{y}, F{not z}}.

Dually to Proposition 3.1, we have the following for atoms.

Proposition 3.2 Let Π be a logic program.

The set of clauses

is logically equivalent to the propositional theory

Combining the last propositions yields the following result.

Theorem 3.3 Let Π be a tight logic program and

Then, X ⊆ atom(Π) is an answer set of Π iff X = AT ∩ atom(Π) for a (unique) solution A for ΔΠ.

The nogoods in ΔΠ capture the supported models of a program [Apt et al., 1987]. Any answer set is a supported model, but the converse only holds for tight programs [Fages, 1994]. The mismatch on non-tight programs is caused by loops [Lin and Zhao, 2004], responsible for cyclic support among true atoms. Such cyclic support can be prohibited by loop formulas. As shown in [Lee, 2005], the answer sets of a programΠ are precisely the models of Π that satisfy the loop formulas of all non-empty subsets of atom(Π). 1 Observe that the exponential number of loops in the worst case [Lifschitz and Razborov, 2006] makes an enumeration of all loop formulas infeasible. All loop formulas can however be checked in linear time, and propagation within genuine ASP solvers makes sure that they are satisfied by a solution.

For a program Π and some U ⊆ atom(Π), we define the external bodies of U for Π, EBΠ(U), as

The (disjunctive) loop formula of U for Π, LFΠ(U), is

1 Note that a loop formula can be constructed for any set of atoms, even if this set is not a loop in the sense of [Lin and Zhao, 2004].

where β+ = β ∩ atom(Π) and β= {p | not p ∈ β}. The loop formula of a set U of atoms enforces all elements of U to be false, if U is not externally supported [Lee, 2005].

To capture the effect of a loop formula induced by a set U ⊆ atom(Π), we define the loop nogood of an atom p ∈ U as

where EBΠ(U) = {β1, . . . , βk}. Overall, we get the following set of loop nogoods for a programΠ:

Observe that loop nogoods make direct use of the bodies in EBΠ(U) = {β1, . . . , βk}, unlike loop formulas LFΠ(U) relying on the literals in each βi. Using bodies in loop nogoods is reasonable because unit propagation on completion nogoods makes a body false if it contains a false literal. Notably, the usage of bodies avoids a combinatorial blow-up, faced when expressing these constraints in terms of body literals. In fact, representing λ(p, U) in terms of body literals yields about |β1 × · · · × βk| nogoods instead of a single one.

Dropping the tightness requirement, we can show that completion and loop nogoods characterize answer sets.

Theorem 3.4 Let Π be a logic program, let ΔΠ and ΛΠ as in Theorem 3.3 and (1).

Then, X⊆atom(Π) is an answer set of Π iff X =AT ∩ atom(Π) for a (unique) solution A for ΔΠ ∪ ΛΠ.

The nogoods in ΔΠ ∪ ΛΠ describe a set of constraints that must principally be checked for computing answer sets. While the size of ΔΠ is linear in atom(Π)×body(Π), the one of ΛΠ is exponential. These magnitudes apply to all existing ASP solvers, where ΔΠ is either encoded via dependency graphs (linking atoms and bodies/rules) or given through the Clark completion of Π. Loop nogoods in ΛΠ are determined only on demand by dedicated algorithms.

4 Conflict-Driven ASP Solving

Given the specification of ASP solving in terms of nogoods, we can now make use of advanced techniques from CSP and SAT for developing equally advanced ASP solving procedures. Different from SAT, where every (known) nogood is usually explicated as a clause, our algorithms work on logic programs, inducing several kinds of nogoods. In particular, the exponentially many nogoods resulting from loop formulas are implicitly given by a program, and determined only when used for propagation. The key role of the different kinds of (and partially implicit) constraints, expressed as nogoods, is to identify a reason responsible for deriving a literal by unit propagation. This makes the logical fundament of ASP solving the same as the one of CSP and SAT solving, so that we can directly apply similar reasoning strategies, without the need of a SAT conversion or proprietary designs.

To begin, we give a specification of our nogood propagation procedure in Algorithm 1. Propagation works on a program Π, a set ∇ of recorded nogoods, and an assignment A. First, we invoke LOCALPROPAGATION on Π and accumulated nogoods in ∇. This function adds unit-resulting literals to A, derived via nogoods either in ΔΠ or in ∇; that is, a

Algorithm 1: NOGOODPROPAGATION

Input : A programΠ, a set ∇ of nogoods, and an assignment A.

Output : An extended assignment and set of nogoods.

U ← ∅ // set of unfounded atoms 1 loop 2 A ← LOCALPROPAGATION(Π, ∇, A) 3 if δ ⊆ A for some δ ∈ ΔΠ ∪ ∇ or TIGHT(Π) then 4 return (A, ∇) 5 else 6 U ← U \ AF 7 if U = ∅ then U ← UNFOUNDEDSET(Π, A) 8 if U = ∅ then return (A, ∇) 9 else let p ∈ U in 10 ∇ ← ∇ ∪ {λ(p, U )} 11 if Tp ∈ A then return (A, ∇) 12 else A ← A ◦ (Fp) 13

fixpoint of unit propagation is computed. If LOCALPROPAGATION yields a violated nogood δ (line 4), then A cannot be extended to a solution. Also if Π is tight, all unfounded atoms are already falsified. In both cases, we are done with nogood propagation. Only if Π is non-tight, we check whether an unfounded set [van Gelder et al., 1991] (accumulated in U) has to be falsified.

Initially, U is empty; so in line 8 we determine an unfounded set. Note that, if some non-false atom is unfounded, there always is an unfounded set not containing any false atoms. In Section 5, we describe our implementation of UNFOUNDEDSET; we here only require that an unfounded set U of non-false atoms is returned, if it exists. If so, we select in line 10 an atom p from U and add its loop nogood λ(p, U) to ∇ (line 11). 2 If p is true, then λ(p, U) is violated, and we return A and ∇ (line 12). Otherwise, Fp is unit-resulting for λ(p, U) wrt A, and we add Fp to A (line 13). Having falsified a single element of U, we re-invoke LOCALPROPAGATION before adding any further loop nogoods. In fact, completion nogoods in ΔΠ might suffice for falsifying the residual atoms in U. For example, consider U = {x, y, z} and rules x ← z, y ← x, z ← y: From Fx, we can derive Fy and Fz. But generally, falsifying a single element does not allow for falsifying the whole set U only via completion nogoods. If we add rule y ← z to the above example, then Fy and Fz are no longer derivable. This is reflected in line 7, where we remove false atoms from U. The shrunken set U is still unfounded, and if it is non-empty, we can immediately determine another loop nogood to falsify the next element of U. Observe that no further unfounded atoms are computed until the ones in U are expended. With changing set U, the atom p (selected in line 10) and the bodies in loop nogood λ(p, U) change in each iteration, aiming at a firmer representation of the respective unfounded set.

All in all, our nogood propagation procedure interleaves unit propagation on completion and accumulated nogoods

2 Given that p is unfounded, we have λ(p, U) \ {Tp} ⊆ A.

Algorithm2: CDNL-ASP

Input : A programΠ.

Output : An answer set of Π.

A ← ∅ // assignment over atom(Π) ∪ body(Π) 1 ∇ ← ∅ // set of (dynamic) nogoods 2 dl ← 0 // decision level 3 loop 4 (A, ∇) ← NOGOODPROPAGATION(Π, ∇, A) 5 if ε ⊆ A for some ε ∈ ΔΠ ∪ ∇ then 6 if dl = 0 then return no answer set 7 (δ, σUIP , k) ← CONFLICTANALYSIS(ε, Π, ∇, A) 8 ∇ ← ∇ ∪ {δ} 9 A ← A \ {σ ∈ A | k < dl (σ)} 10 dl ← k 11 A ← A ◦ (σUIP ) 12 else if AT ∪ AF = atom(Π) ∪ body(Π) then 13 return AT ∩ atom(Π) 14 else 15 σd ← SELECT(Π, ∇, A) 16 dl ← dl +1 17 A ← A ◦ (σd) 18

with the recording and propagation of loop nogoods. The latter is only done if the underlying program is non-tight and the falsity of unfounded atoms cannot be determined via other nogoods. Our approach favors local propagation over unfounded set computations. This is motivated by the fact that local propagation does not add any nogoods to ∇, hence, it is more economical than unfounded set falsification. We further discuss the relation between our propagation strategy and other approaches in Section 7.

Conflict-Driven Nogood Learning. Our basic algorithm for deciding whether a program has an answer set is similar to Conflict-Driven Clause Learning (CDCL) with First-UIP scheme [Mitchell, 2005]. Given a program Π, Algorithm 2 starts from an empty assignment A and an empty set ∇ of learned nogoods. Via the decision level dl , we count decision literals, i.e., the literals in A not derived by nogood propagation. The initial value of dl is 0, it is incremented before a decision literal is added to A. For a literal σ ∈ A, we access via dl (σ) the decision level of σ, that is, the value dl had when σ was added to A. After encountering a conflict, the decision level is used to guide backjumping.

The loop of Algorithm 2 is similar to CDCL, so we here only sketch the principal steps. First, function NOGOODPROPAGATION deterministically extends A (and ∇) as described above. If this yields a conflict (line 6), function CONFLICTANALYSIS (see below) determines a conflict nogood δ to be recorded, a unique implication point (UIP) σUIP, and a decision level k to jump back to. Backjumping and nogood recording work as with CDCL, in particular, a conflict at decision level 0 indicates the non-existence of an answer set. If A is a solution (line 13), the atoms of Π that are true in A form an answer set of Π. Finally, if A is non-conflicting and partial, a decision literal σd is selected according to some heuristics (see Section 5 on further details) and added to A. Note that

Algorithm3: CONFLICTANALYSIS

Input : A violated nogood δ, a programΠ, a set ∇ of nogoods, and an assignment A. Output : A derived nogood, a UIP, and a decision level. let σ ∈ δ st B = C ◦ (σ) ◦ C′ and δ \ {σ} ⊆ C

let σ ∈ δ st A = B ◦ (σ) ◦ B′ and δ \ {σ} ⊆ B 1 while {ρ ∈ δ | dl (ρ) = dl (σ)} ̸= {σ} do 2 let ε ∈ ΔΠ ∪ ∇ st σ ∈ ε and ε \ {σ} ⊆ B 3 δ ← (δ \ {σ}) ∪ (ε \ {σ}) 4 5 B ← C 6 k ← max ({dl (ρ) | ρ ∈ δ \ {σ}} ∪ {0}) 7 return (δ, σ, k) 8

σd belongs to the new decision level dl + 1.

Our conflict analysis procedure determines an asserting nogood δ. That is, after backjumping, δ yields a unit-resulting literal, leading Algorithm 2 into a different part of the search space than traversed before. This is similar to an asserting clause, determined by conflict analysis in CDCL. In deriving δ, we follow the First-UIP scheme and stop conflict analysis at the first UIP that is found; no further UIPs are explored.

Though our conflict analysis procedure is similar to its classical CDCL counterpart, we need subtle adjustments. The reason is that unfounded set inference works in a directed way: It only falsifies unfounded atoms, but does not "protect" true atoms from becoming unfounded. For illustration, consider Π = {x ← not y ; y ← not x ; u ← x ; u ← v ; v ← u, y} along with assignment A = (Tu). Note that Tu is a decision literal; its decision level is 1. Local propagation on ΔΠ and A yields no inferences (due to body(u) = {{x}, {v}}), and there is no unfounded set. When we extend A by decision literal Ty at level 2, local propagation sets atom x and body {x} to false (and v to true). But then, the set {u, v} becomes unfounded, which makes us record the loop nogood δ = λ(u, {u, v}) = {F{x},Tu}. Since A contains F{x} and Tu, nogood δ is violated. Also, δ contains only one literal added to A at decision level 2: F{x}. Hence, F{x} is a UIP. In this example, the violated nogood δ is immediately asserting. A situation like this cannot occur in classical CDCL, where the initial violated clause always contains more than one literal from the current decision level. The difference to CDCL is caused by the directedness of unfounded set inference in ASP, which is "partial", in the sense that not all logical consequences are derived. In terms of a loop nogood {Fβ1, . . . , Fβk, Tp}, unfounded set inference can only derive Fp, but not Tβi for a body βi (1 ≤ i ≤ k), at least as long as the loop nogood is not made explicit by recording it. For δ = {F{x},Tu} as above, unfounded set inference would have derived Fu at decision level 1, if we had selected F{x} as the decision literal. However, it does not derive T{x} from assignment (Tu), which is inferred by unit propagation once δ is available as an explicit constraint. (Undirected unfounded set inference is not yet algorithmically solved. Current algorithms only determine unfounded atoms, but not bodies that must be true according to an (implicit) loop nogood.)

Algorithm 3 shows our conflict analysis procedure. It works on an assignment A containing a violated nogood δ, either from the program Π and so in ΔΠ, or from the recorded nogoods in ∇. In line 1, we determine via σ the literal from δ added last to A. As mentioned above, σ might already be a UIP, that is, the single literal in δ from the current decision level. If σ is a UIP, we do not enter the while-loop in line 2. Otherwise, δ contains at least one literal other than σ from the current decision level. Note that, in this case, σ is not a decision literal. Hence, there is some nogood ε in ΔΠ or ∇ for which σ has been unit-resulting. Such an ε is determined in line 3, and in line 4 we resolve δ and ε into a new nogood δ. In line 5, we determine as new σ the literal from the new δ added last to A. In each iteration, σ moves closer to the front of A. Hence, we finally derive a nogood δ that contains exactly one literal σ from the current decision level; in the worst case, it is the decision literal. In line 7, we determine the decision level to jump back to as the maximum level of any literal in δ other than σ. Algorithm CONFLICTANALYSIS is very similar to the First-UIP scheme for CDCL. The difference is that conflict resolution might start from an asserting nogood.

5 The clasp System

Our new system clasp [2006] implements our approach to ASP solving. It combines the high-level modeling capacities of ASP with state-of-the-art techniques from the area of Boolean constraint solving. Unlike existing ASP solvers, clasp is originally designed and optimized for conflictdriven ASP solving. Rather than applying a SAT solver to a CNF conversion, clasp directly incorporates suitable data structures, particularly fitting backjumping and learning. This includes dedicated treatment of binary and ternary nogoods [Ryan, 2004], and watched literals for unit propagation on "long" nogoods [Moskewicz et al., 2001]. Unlike smodelscc [Ward and Schlipf, 2004], which builds a material implication graph for keeping track of the multitude of inference rules found in ASP solving, clasp uses the more economical approach of SAT solvers: For a derived literal, it only stores a pointer to the responsible constraint in ΔΠ ∪∇.

Unfounded set detection within clasp combines smodels' source pointer technique [Simons, 2000] with the unfounded set computation algorithm described in [Anger et al., 2006]. It aims at small and "loop-encompassing", rather than greatest unfounded sets, as determined by smodels [Simons et al., 2002] and dlv [Leone et al., 2006]. Notably, clasp recognizes violated loop nogoods that are immediately asserting (cf. Section 4), so that the same nogood is not recorded twice.

The primary operation mode of clasp is conflict-driven nogood learning. Beyond backjumping and learning, clasp features a number of related techniques, typically found in CDCL-based SAT solvers. clasp incorporates restarts, deletion of recorded conflict and loop nogoods, and decision heuristics favoring literals from conflict nogoods. All these features are configurable via command line options. The default restart and nogood deletion policies are adopted from MiniSat [E´en and S¨orensson, 2003]; the standard heuristics is an adjustment of BerkMin [Goldberg and Novikov, 2002]. Although Algorithm 2 details the search for one answer set, clasp also allows for enumerating answer sets. This is accomplished by interleaving backjumping with (systematic) backtracking: After a solution has been found, its decision literals can only be backtracked chronologically; backjumping is restricted for not repeating already enumerated solutions. This strategy avoids the generation of nogoods excluding entire solutions, as done for instance by smodelscc and mchaff 3 .

clasp's second major operation mode runs (systematic) backtracking without learning. This is similar to the strategy of standard ASP solvers like smodels, using lookahead. Both operation modes are implemented in a uniform framework, which also allows us to evaluate the efficiency of advanced SAT implementation techniques, such as watched literals, in a standard ASP solver.

6 Experiments

We conducted experiments on a variety of problem classes. Our comparison considers clasp (RC2) in its two major modes: (a) the standard one using backjumping and learning, and (b) the systematic backtracking mode using lookahead but no learning. We refer to these variants as claspa and claspb. As "traditional" ASP solver, we include smodels (2.31). Beyond some variations, smodels' strategy is similar to claspb. We also incorporate assat (2.02) and cmodels (2.12), both using mchaff (spelt3), and smodelscc (1.08). Among all compared solvers, smodelscc is closest to claspa. SAT-based solvers assat and cmodels convert a logic program into CNF and delegate the search for a supported model to mchaff. For tight programs, this approach amounts to clasp in mode (a). In the non-tight case, assat and cmodels delay checking loop nogoods until an assignment is total, while all other solvers integrate it into their propagation.

All experiments were run on a 2.2GHz PC on Linux. We report results in seconds, taking the average of 3 runs, each restricted to 900s time and 1GB RAM. A timeout is indicated by "-". All solvers were run with their default settings except for smodelscc, for which we used option "nolookahead" as recommended by the developers. The instances used in our experiments as well as extended results (e.g. for dlv and nomore++, being excluded here due to lack of space) are available at [clasp, 2006]. In brief, the instances in Table 1 and 2 are from the areas of bounded model checking (1-5;31-35), DES cryptanalysis (6-10), blocksworld planning (11-12;42-45), Hamiltonian cycles in clumpy graphs (13-20), Hamiltonian paths for the Gryzzles game (21-25), Sokoban (26-30;46-55), and machine code superoptimization (36-41). The instances numbered 1-10 and 31-41 are tight, all others are non-tight.

Table 1 gives results for computing one answer set. On the tight instances 1-10, claspa performs comparable to assat and cmodels. Sometimes it is even slightly faster, showing that the low-level implementation of clasp is competitive with stateof-the-art SAT solvers, doing most of the work for assat and cmodels. Regarding smodels, we see that its systematic backtracking approach does not scale very well; the same applies to clasp in mode (b). Instances 11 and 12 are tight on their supported models, that is, every supported model is also an answer set. As unfounded set checks produce unnecessary overhead here, assat and cmodels are a bit faster than claspa. Looking at the Hamiltonian problems in 13-25, we see that smodelscc and claspa scale best. They outperform assat and cmodels by some orders of magnitude; on two clumpy graphs, assat and cmodels even time out (viz. 19 and 20). Both smodels and claspb are ineffective on Hamiltonian problems and time out on most of the instances. On Sokoban problems in 26-30, claspa outperforms the other solvers. Only cmodels and smodelscc never time out, but they are much slower.

3 http://www.princeton.edu/∼chaff/

Table 2 shows results for computing all answer sets, or for determining that no answer sets exist (0 #sol). Given that assat cannot enumerate answer sets, we only include it on unsatisfiable programs. On satisfiable instances 31-35, we see that claspa is relatively fast enumerating all answer sets. The superoptimization instances in 36-41 are easily determined unsatisfiable by assat, cmodels, and claspa. Both smodels and claspb show a clear exponential behavior and finally time out. Surprisingly, smodelscc scales worst, that is, several orders of magnitude behind other learning solvers and timing out even before non-learning ones. We conjecture that this is because smodelscc does, differently from other learning solvers, not include rule bodies in conflict nogoods. Looking at the satisfiable instances among 42-55, we see that claspa is faster enumerating all answer sets than any other solver we tested. Unsatisfiable blocksworld problems 42 and 45 are most effectively solved by assat and cmodels. (Note that instances 42-45 are tight on their supported models.) Like with computing one answer set on (satisfiable) Sokoban problems in 26-30, claspa is fastest on both satisfiable and unsatisfiable problems in 46-55.

Overall, we notice a huge gap between learning and nonlearning solvers: The latter frequently time out, while the best among the former solve the same instances within seconds (cf. Table 1). The short run-times of learning solvers do sometimes not permit a reliable comparison between them. We however see a clear distinction between different concepts: Problems that are intractable for systematic backtracking methods are often easily dealt with using backjumping and learning. Note that all our benchmarks are structured to some extent. This is useful for learning solvers, as structure can be explicated via learned constraints. The picture might be different on unstructured random problems as, e.g., reported in the SAT literature.

7 Discussion

We have provided a uniform approach to ASP solving, allowing for a transparent technology transfer from CSP and SAT. The idea is to view ASP inferences as unit propagation on nogoods, reflecting constraints from program rules, unfounded sets, and conflicts. We have seen that SAT translations are unnecessary for applying techniques found in SAT solvers.

In contrast to SAT, ASP induces further implicit constraints given by loop nogoods. Though inherently present, these nogoods need only be explicated when used for propagation and conflict analysis. Thus, sophisticated unfounded set checks still work on the logical fundament of CSP and SAT. Based on this perception, we have provided a conflict-driven algorithm for ASP solving, using state-of-the-art SAT solving techniques. Notably, our approach favors local propagation on explicit nogoods over unfounded set checks, which explicate inherent loop nogoods that give rise to unit propagation. In fact, many of the combinatorially constructable loop nogoods might be redundant, that is, entailed by completion and other loop nogoods. (For tight programs, the loop nogoods of all non-singletons are redundant.) In this respect, our approach guarantees that only non-redundant loop nogoods are used for propagation and, particularly, for conflict analysis.

We have implemented our approach in the clasp system. Our empirical results show that clasp is competitive with existing ASP solvers. The clasp system directly incorporates state-of-the-art techniques from Boolean constraint solving, avoiding a SAT translation as it is done by assat, cmodels, and sag [Lin et al., 2006]. Also, clasp records loop nogoods only when ultimately needed for unit propagation; this is different from assat and sag, which determine loop formulas for all "terminating" loops. Unlike genuine ASP solvers smodels and dlv, clasp does not determine greatest unfounded sets. Rather, it applies local propagation directly after an unfounded set has been found. Different from dlv with backjumping [Ricca et al., 2006] and smodelscc, the inclusion of rule bodies in nogoods allows for a straightforward extension of unit propagation to ASP, abolishing the need for multiple inference rules. Notably, clasp can enumerate answer sets of a program without explicitly prohibiting already computed solutions by nogoods, as done by cmodels and smodelscc.

Acknowledgments

The authors are grateful to Wolfgang Faber, Yuliya Lierler, and Ilkka Niemel¨a for helpful comments on previous drafts of this paper.