Technical Communications of ICLP 2015. Copyright with the Authors. 1 Abstract Answer Set Solvers for Cautious Reasoning REMI BROCHENIN and MARCO MARATEA University of Genova, Italy (email: {remi.brochenin,marco.maratea}@unige.it) submitted 29 April 2015; accepted 5 June 2015 Abstract Abstract solvers are a recently employed method to formally analyze algorithms that earns some advantages w.r.t. traditional ways such as pseudo-code-based description. Abstract solvers proved to be a useful tool for describing, comparing and composing solving techniques in various fields such as SAT, SMT, ASP, CASP. In ASP, abstract solvers have been so far employed for describing solvers for brave reasoning tasks. In this paper we apply, for the first time, this methodology to the analysis of ASP solvers for cautious reasoning tasks. We describe and compare the available approaches in the literature, which employ techniques for computing over- and under-approximations of the solution, the last including “coherence tests” for deciding the inclusion of a single atom in the solution, a technique borrowed from backbone computation of CNF formulas. Then, we show how to improve the current abstract solvers with new techniques, in order to design new solving algorithms. KEYWORDS: Answer Set Programming, Abstract solvers, Cautious reasoning 1 Introduction Abstract solvers are a relatively recently employed method to formally analyse algorithms that earns some advantages w.r.t. traditional ways such as pseudo-code-based description. In this methodology, the states of computation are represented as nodes of a graph, the solving techniques as edges between such nodes, the solving process as a path in the graph and formal properties of the algorithms are reduced to related graph properties. Abstract solvers proved to be a useful tool for describing, comparing and composing solver design techniques in various fields such as CNF satisfiability (SAT) and Satisfiability Modulo Theories (SMT) (Nieuwenhuis et al. 2006), Answer Set Programming (Lierler 2011; Lier- ler and Truszczynski 2011; Brochenin et al. 2014), and Constraint ASP (Lierler 2014). In ASP, such methodology led to the development of a new ASP solver, SUP (Lierler 2011); however, abstract solvers have been so far applied to ASP solvers for brave reasoning tasks where, given an input query and a knowledge base expressed in ASP, answers are witnessed by ASP solutions, i.e. stable models (Baral 2003; Eiter et al. 1997; Gelfond and Lifschitz 1988; Gelfond and Lifschitz 1991; Marek and Truszczyński 1998; Niemelä 1999). In cautious reasoning, instead, answers must be witnessed by all stable models. Two well-known ASP solvers, i.e. DLV (Leone et al. 2006) and CLASP (Gebser et al. 2012), 2 R. Brochenin and M. Maratea allow the computation of cautious consequences of ASP programs. They use devoted tech- niques, i.e. over- and under-approximations of the solution, which are built on top of their procedures for computing stable models. Very recently, Alviano et al. (2014) presented a unified, high-level view of such solving procedures, and designed several algorithms for cautious reasoning in ASP. The under-approximation technique relies on a “coherence test” for deciding the inclusion of a single atom in the solution, a technique borrowed from the backbone computation of CNF formulas (Janota et al. 2015): all these techniques are implemented (and tested) on top of the ASP solver WASP (Alviano et al. 2013). In this paper, starting from the algorithms description of Alviano et al. (2014), we apply, for the first time, abstract solvers to the analysis of ASP solvers for cautious reasoning tasks. We first describe and compare the mentioned available techniques, and show how they can be modeled by adding edges to the graphs describing ASP solvers in a modular way. Finally, we outline how to include in our picture further (optimization) techniques, like backjumping and learning, as well as other algorithms of Janota et al. (2015). To sum up, the main contributions of this paper are: • We employ abstract solvers for analyzing ASP solvers for cautious reasoning tasks. • We define a framework that can ease the import of other techniques originally devel- oped in solvers for computing backbones of CNF formulas in the abstract procedures for cautious reasoning. • We outline how to include further (optimization) techniques in our graphs. The paper is structured as follows. Section 2 introduces needed preliminaries, while Section 3 reviews abstract solvers for SAT and ASP, in a uniform way. Section 4 presents abstract solving algorithms for cautious reasoning in ASP. The paper ends by presenting how to add further techniques in our graphs, in Section 5, and with related work and con- clusions in Section 6. 2 Preliminaries Syntax. An atom is a Boolean variable over {⊤, ⊥}. A positive literal is an atom. A nega- tive literal is the negation of an atom ¬a. A literal is a positive literal or a negative literal. A rule is a pair (A, B), written A ← B, where B is a set of literals and A is a set of positive literals of size at most 1. A program is a finite set of rules. The complement l of a literal l is the literal a for l = ¬a and the literal ¬a for l = a. For a set of literals M , by M we denote the set of the complements of the literals of M , by M + is the set of positive literals of M and M − is the set of negative literals of M . A set of literals is consistent if it does not contain both l and l. In a rule A ← B, 1. A is called the head of the rule; 2. B is the body of the rule, of which elements are traditionally written separated by a comma as in a ← b, ¬c. We may also write a rule as A ← B + , B − , as an abbreviation for A ← B + ∪ B − , and A ← l, B as an abbreviation for A ← {l} ∪ B. Note that we focus on non-disjunctive programs in this article, hence A can only be empty or a singleton. Abstract Answer Set Solvers for Cautious Reasoning 3 Finally, for a program Π , by atoms(Π ) we denote the set of atoms occurring in Π ; we also use this notation for sets of literals and conjunctions. For a set of atoms X, a literal relative to X is a literal of which atom belongs to X, and lit (X) is the set of all literals relative to X. Semantics. An assignment to a set X of atoms is a total function from X to {⊥, ⊤}. We identify a consistent set M of literals with an assignment to atoms(M ): a ∈ M iff a is mapped to ⊤, and ¬a ∈ M iff a is mapped to ⊥. A classical model of a program Π is an assignment M to atoms(M ) such that for each rule R of Π , R ∩ M 6= ∅. The reduct Π X of a program Π w.r.t. a set of atoms X is obtained from Π by deleting each rule A ← B + , B − such that X ∩ atoms(B − ) 6= ∅ and replacing each remaining rule A ← B + , B − with A ← B + . A stable model of a program Π is an assignment M to atoms(M ) such that M + is minimal among the M0+ such that M0 is a classical model of + Π M . If a program Π has at least one stable model then cautious(Π ) is the intersection of all the stable models of Π . Following Leone et al. (1997), for a program Π and an assignment M over atoms(Π ), a subset X of atoms(Π ) is said to be unfounded on M w.r.t. Π when for each atom a in X and each rule a ← B in Π , one of the following condition holds: (i) M ∩ B 6= ∅, or (ii) X ∩ B + 6= ∅. 3 Abstract solvers The Davis-Putnam-Logemann-Loveland procedure (DPLL) (Davis et al. 1962) exhaus- tively explores assignments which are good candidates for classical models of CNF for- mulas. An abstract transition system for DPLL has been proposed by Nieuwenhuis et al. (2006), and then extended to procedures that exhaustively explore assignments which are good candidates for stable models of answer set programs (Lierler 2008). We present here these abstract transition systems, with slight modifications that will allow us to introduce abstract solvers for cautious reasoning with more clarity. States and Basic Rules. For a set of atoms X, an action relative to X is an element of the set {init , over } ∪ {under {l} |l ∈ lit (X)}. A decision literal relative to X is a literal relative to X annotated with d, as in ad . An annotated literal relative to X is a literal or a decision literal relative to X. For a set X of atoms, a record relative to X is a string L composed of annotated literals relative to X without repetitions. A record L is consistent if it does not contains both a literal and its negation, whether annotated or not. We may view a record as the set containing all its elements stripped from their annotations. For example, we may view bd ¬a as {¬a, b}, and hence as the assignment that maps a to ⊥ and b to ⊤. A record L is decision-free if it does not contains any annotated literal. The set of states relative to X, written VX , is the union of: • The set of core states relative to X, that are all LO,U,A , s.t. L is a record relative to X, O and U are sets of literals relative to X, and A is an action relative to X. • The set of control states relative to X, that are all the Cont (O, U ) where O and U are sets of literals relative to X. 4 R. Brochenin and M. Maratea Oracle rules Lld L′ is inconsistent and  Backtrack Lld L′ O,U,A =⇒ LlO,U,A if L′ contains no decision literal  L is consistent and Decide LO,U,A =⇒ Lld O,U,A if neither l nor l occur in L Return rule  Fail init LO,U,init =⇒ Failstate if L is inconsistent and decision-free Fig. 1. The basic transition rules of base. • The fail state Failstate; • The set of final states relative to X, that are all the Ok (W ) where W is a set of literals relative to X. The graphs we will define with these states represent algorithms that search for assign- ments with certain properties. In a core state, L represents what is known of the assignment currently studied. The fail state means that the computation failed, in other words there is no such mathematical object as the one we were searching for. The use of control and final states, as well as of the subscripts O, U, A in core states, does not influence our current graphs and will come in next section. Also, in this section the actions A will always be init . The basic rules are the rules from the set of transition rules base = {Backtrack , Decide, Fail init }, presented in Figure 1. The basic rules along with the states relative to X will be part of many transition graphs we will present in the article. The rule Decide means that we make an arbitrary decision to assign a value to an atom. The rules specific to a problem that we will add later will provide deterministic consequences to the choices already made, as literals that will not be decision literals. Since decisions with Decide are arbitrary, if we find a contradiction we should be able to backtrack to an earlier point, and the rule Backtrack means that the present state of computation is inconsistent and we reverse our latest arbitrary decision. The rule Fail means that we have found a contradiction and no backtracking is possible. Graphs. Intuitively, every reachable state of the graphs represents a possible state of a computation, and a path in the graph from the initial state is the description of possible search for a model. We now define the program ΠO,U,init to be Π . From the transition rules presented in Fig- ure 2, we define dp = {UnitPropagate}, cl = {UnitPropagate, Unfounded} and sm = {UnitPropagate, AllRulesCancelled , BackchainTrue, Unfounded } (i.e. rules employed in, e.g. SMODELS (Simons et al. 2002)). The rules in sm mean that we can add a literal that is a straightforward consequence of our previous decisions and the studied formula or program. Such deterministic consequences can be different, depending on whether we are searching for a classical model or a stable model. In case of a search for a classical model one may use dp, but since we search for a stable model we will use cl or sm. Abstract Answer Set Solvers for Cautious Reasoning 5 Oracle rules   in ΠO,U,A , there is : UnitPropagate LO,U,A =⇒ LlO,U,A if l ← B such that B ⊆ L or A ← l, B such that A ∪ B ⊆ L   AllRulesCancelled LO,U,A =⇒ L¬aO,U,A if for all a ← B in ΠO,U,A , B ∩ L 6= ∅  in ΠO,U,A , there is a ← l, B s. t. a ∈ L and BackchainTrue LO,U,A =⇒ LlO,U,A if for all other a ← B ′ holds B ′ ∩ L 6= ∅  there is X such that a ∈ X and Unfounded LO,U,A =⇒ L¬aO,U,A if X is unfounded on L w.r.t ΠO,U,A Fig. 2. The transition rules of sm. The family of graphs (VX , base ∪ sm) defines a general graph that include the transitions that characterise the behavior of backtracking-based SAT and (some) ASP solvers: To find a stable model of Π it is enough to find a path leading from a proper initial vertex to a terminal vertex in the graph employing the cl or sm set of transition rules. If the terminal vertex is Failstate, then no such model exists. Otherwise, L is a stable model of Π . The use of the sets of transition rules cl ∪ base and sm ∪ base respectively characterise the behavior of CLASP or WASP, and DLV, without backjumping and learning1 , i.e. the solvers on top of which approaches for cautious reasoning are implemented. Thus, in our graphs they will describe the search of an ASP oracle call. 4 Abstract Solvers for Computing Cautious Consequences In this section we abstract the algorithms from Alviano et al. (2014). After explaining some general properties about the graphs we will define, we first abstract the over-approximation strategy, and then we abstract the under-approximation strategy and show how these strate- gies can be mixed. General Structure. The basic architecture of all solutions, including the one implemented in WASP (Alviano et al. 2013), for determining the cautious consequences of a program is presented in Algorithm 1 of Alviano et al. (2014). Given a program, over-approximation is set to all atoms in the program, while the under-approximation is empty. A first stable model is searched (ASP oracle call at line 2), which is characterised by the action init in the base transition rules and, if found, serves as a first over-approximation of the cau- tious consequences of the program. Then, iteratively either under-approximation or over- approximation (as shown in Algorithms A1, . . . , A4 of Alviano et al. (2014)) are applied. When under- and over-approximations coincide, the set of cautious consequences O has been found and the computation terminates by going to the state Ok (O) in the graph. Hence, the full extent of states relative to X becomes useful. As previously, the fail state 1 CLASP and WASP are conflict-driven solvers relying heavily on learning, so it is not easy to describe such solvers as backtracking-based procedures without learning. For CLASP we refer to the considerations in Sec. 8.2 of Lierler (2011); WASP has a similar behavior to that of CLASP , which is confirmed by personal com- munications with the authors. For DLV we refer to Giunchiglia et al. (2008). More precise characterizations, including backjumping and learning techniques, will be presented in Section 5. 6 R. Brochenin and M. Maratea Return rules  Fail over LO,U,over =⇒ Ok (O) if  L is inconsistent and decision-free Find LO,U,A =⇒ Cont(O ∩ L, U ) if no other return or oracle rule applies Control rules Success Cont (O, O) =⇒ Ok (O)  OverApprox Cont (O, U ) =⇒ ∅O,U,over if O 6= U Fig. 3. The transition rules of ov . Failstate is reached when there is no model. The final states Ok (W ) are the only other type of terminal states, and W is what we want to compute in the graph – in this section the cautious consequences of the program. The initial state will always be ∅atoms(Π ),∅,init in this section. The core states LO,U,A and the control states Cont (O, U ) represent all the intermediate steps of the computation; they are such that: • L is the current state of the computation of a model; • O is the current over-approximation of the solution stored as a set; • U is the current under-approximation of the solution stored as a set; • A is the action currently carried out: init if we search for a first model, over (resp. under {l} ) action if over-approximation (resp. under-approximation on a literal l) is being applied. Intuitively, a core state represents the computation within a call to an (ASP) oracle, i.e. an ASP solver, while a control state controls the computation between different calls to ASP oracles, depending on over-approximation and under-approximation. We say that no cycle is reachable if there is no reachable state which is reachable from itself. Definition 1 We say that a graph G finds a statement M that defines a set of literals, or “finds M ”, if the following conditions hold: 1 G is finite, and no cycle is reachable in G, 2 the only reachable terminal state is Failstate if M does not define a set of literals, and 3 the only reachable terminal state is Ok (M ) otherwise. In the following we will define graphs that find the cautious consequences of a program. Over-approximation. We first abstract Algorithm A2 of Alviano et al. (2014). It corre- sponds to the strategy of CLASP and DLV to compute cautious consequences.2 We define ΠO,U,over as Π ∪ {← O}. We call ov the set containing all the rules pre- sented in Figure 3, that is ov = {Fail over , Find , Success, OverApprox }. These rules are organised into Return rules, that handle the result of an oracle call, and Control rules, that 2 The strategy of DLV slightly differs from that of CLASP as the studied program in DLV is Π to which is added one constraint per found stable model so as to avoid that precise stable model. CLASP , instead, add a constraint built on the over-approximation. Moreover, DLV does not forget the added constraints later, thus it may run in exponential space. Abstract Answer Set Solvers for Cautious Reasoning 7 Return rule  Fail under LO,U,under {l} =⇒ Cont (O \ {l}, U ∪ {l}) if L is inconsistent and decision-free Control rule  UnderApprox Cont (O, U ) =⇒ ∅O,U,under {l} if l∈O\U Fig. 4. The transition rules of un that are not in ov . direct the search given the actual values of O and U . Intuitively, Fail over means that a call to an oracle did not find a stable model, so O is the solution. If Find is triggered, instead, we go to a control state where the over-approximation O is updated according to the stable model found: then, if O = U a solution is found through Success, otherwise the search is restarted (L = ∅) in an oracle state with OverApprox . For any Π , the graph OS Π is (Vatoms(Π ) , base ∪ ov ∪ sm). In OS Π , first an oracle is called under the init action. If it fails there is no stable model at all and the computation ends on Failstate. If it succeeds, the obtained set is used as a first over-approximation of the cautious consequences of the studied program. Then, iteratively, the oracle is called to find other stable models that reduce the over-approximation O. The over action is used for this purpose. If a stable model M is found, since ΠO,U,over is Π ∪ {← O}, for sure M ∩O 6= ∅. Hence some progress has been made, the over-approximation can be updated to M ∩ O. Otherwise, if no stable model is found, there is no stable model that does not contain all the elements of O. Also, since at least one stable model has been found during the init action, all the elements of O belong to a stable model. Hence O is the set of cautious consequences of the studied program. Formally: Theorem 1 For any program Π , the graph OS Π finds cautious(Π ). Under-approximation. We now abstract the strategy A3 of Alviano et al. (2014). We define ΠO,U,under l as Π ∪ {← l}. We call un the set {Fail under , Find , Success, UnderApprox } containing the rules presented in Figure 4 plus Find and Success from Figure 3. Intuitively, Fail under updates over- and under-approximations in case a test on l failed, and leads to a control state, while UnderApprox restarts a new test if Find is not applicable. For any Π , the graph US Π is (Vatoms(Π ) , base ∪ un ∪ sm). In US Π , again, a first oracle call takes place with the action init . This provides a first over-approximation. Then, iteratively, for one element (i.e. the tested literal l) of the cur- rent over-approximation O the oracle is called to find a stable model of the program that does not contain this element. If such a stable model M is found then the element can be removed from the over-approximation, along with any other element of the over- approximation that would not belong to M , with O ∩ M in the rule Find kept identical from over-approximations. On the other hand, if no such stable model is found then this element can be added to the under-approximation with the rule Fail under . Finally, at some point the over-approximation and the under-approximation are equal. The computation can end with Success. Theorem 2 8 R. Brochenin and M. Maratea Π = Π{a,b,c},∅,init = { ∅{a,b,c},∅,init ← a, b UnitPropagate : c{a,b,c},∅,init a ← ¬a, ¬b Decide : cad {a,b,c},∅,init a ←b UnitPropagate : cad ¬b{a,b,c},∅,init b ← ¬a, ¬b Find : Cont({a, c}, ∅) b ←b c ←} OverApprox : ∅{a,c},∅,over UnitPropagate : c{a,c},∅,over Π{a,c},∅,over = Π ∪ { UnitPropagate : c¬a{a,c},∅,over ← a, c } UnitPropagate : c¬ab{a,c},∅,over Find : Cont({c}, ∅) Π{c},∅,under {c} = Π ∪ { UnderApprox : ∅{c},∅,under {c} ←c UnitPropagate : c{c},∅,under {c} ← ¬c } UnitPropagate : c¬c{c},∅,under {c} Fail under : Cont({c}, {c}) Success : Ok ({c}) Fig. 5. A path in MixS Π . For any program Π , the graph US Π finds cautious(Π ). The actual strategy of WASP mixes both over-approximations and under-approximations. We now abstract such a mixed strategy. We define MixS Π as (Vatoms(Π ) , base ∪ un ∪ ov ∪ sm), which summarises Algorithm 1 in Alviano et al. (2014). In Figure 5, we introduce an example of path through this mixed graph, where for each rule the destination state follows, while the source state is in the line above. Theorem 3 For any program Π , the graph MixS Π finds cautious(Π ). 5 Extensions and Discussion In this section we discuss further techniques that can be abstracted and added to the graphs described in the previous sections. After introducing backjumping and learning, it will be meaningful to add restarts. Finally, we discuss about the opportunity to apply other methods from backbone computation to the computation of cautious consequences. Backjumping and Learning. The techniques described above are actually often imple- mented on top of solvers employing two additional techniques: backjumping and learning. We now show how to add these techniques to the graphs defined above. For two programs Π and Π ′ , we say that Π is a logical consequence of Π ′ if any classical model of Π ′ is also classical model of Π . For a set of states V and a program Π , we define the set V BL(Π ) as the set of all the Λ x , where x ∈ V and Λ is a program of which rules have no nonempty head and of which atoms belong to atoms(Π ). Note that there is only a finite number of possible rules using a given finite set of atoms, hence there is only a finite number of possible such programs; so there is only a finite number of elements in V BL(Π ) . These elements are states that can Abstract Answer Set Solvers for Cautious Reasoning 9 Oracle rules Lld L′ is inconsistent and  Λ Λ Backjump Lld L′ O,U,A =⇒ LlO,U,A if ← l, L′ is a logical consequence of ΠO,U,A UnitLearn LΛ =⇒ LlΛ  O,U,A O,U,A if in Λ, there is ← l, B such that B ⊆ L Other rule   ← B is a logical consequence of ΠO,U,A and Λ∪{←B} Learn LΛ O,U,A =⇒ ∅O,U,A if ←B∈ / Λ and  ← B is a clause Fig. 6. The transition rules of bl. hold the learnt rules, and are hence suitable for backjumping and learning. We now define a trivial transformation of edges; for a set E of edges between elements of V we define E BL(Π ) as the set of edges between elements of V BL(Π ) such that (xΛ Λ2 1 , x2 ) ∈ E 1 BL(Π ) iff (x1 , x2 ) ∈ E and Λ1 = Λ2 . This transformation allows us to extend existing rules to the framework of backjumping and learning. We can now define the transition rules specific to backjumping and learning in Figure 6: Backjump restores an inconsistent state by flipping the last decision literal responsible for the conflict, UnitLearn applies unit propagation on the added rules, and Learn stores an implied rule. We define bl as the set containing these three transitions rules, where Backjump and UnitLearn are oracle rules, while Learn is neither an oracle rule nor a return rule. Abstractly, Learn is an oracle rule, but has been classified in a different way for a technical issue, i.e. in order to ensure correct interaction with (the conditions enabling) rule Find . Finally, for a graph G = (V, E), we define GBL(Π ) as (V BL(Π ) , E BL(Π ) ∪ bl). If G is finite and no cycle is reachable then it is possible to show that GBL(Π ) is also finite and no cycle is reachable. Note that the procedure obtained from such graphs may not run in polynomial space: hence, in general such algorithms also include a mechanism for forgetting learnt rules The following result extends the one in the previous section. For any program Π , and for any set S ⊆ {un, ov , ch} such that A 6= ∅, S BL(Π ) • the graph (Vatoms(Π ) , base ∪ x∈S x ∪ dp) finds backbone(Π ), and S BL(Π ) • for any set cl ⊆ S ′ ⊆ sm, the graph (Vatoms (Π ) , base ∪ x∈S x ∪ S ′ ) finds cautious(Π ). Adding restarts. In the previous graphs, it is meaningful to consider restart by adding the rule Restart. Note that Restart, like Learn, is neither an oracle rule nor a return rule. Other rule Restart LO,U,A =⇒ Cont(O, U ) This rule can be added to any of the graphs we have defined. We more particularly study the case of MixS Π . Extending the graph MixS Π with this rule and the ones in the previous paragraph provides a good abstraction of a mixed strategy in Algorithms A2*, A3* and A4*=A4 of Alviano et al. (2014). Stating a formal result on this graph involves using properties about the frequency of the use of Restart rule, which are not specified in the article. Without such assumptions, we can state the following result: The graph is finite, 10 R. Brochenin and M. Maratea the only reachable terminal state is Failstate if there is no stable model, and otherwise any reachable terminal state is of the form Ok (cautious(Π )). We are now also in the position to better characterise the behaviors of CLASP, WASP and DLV , i.e. the ASP solvers on top of which procedures for computing cautious consequences are built. In particular, CLASP and WASP also employ the techniques in bl and Restart, while DLV employs Backjump (Ricca et al. 2006). Methods from backbone computation. We believe that the framework we have defined can be also used, with simple adaptations, to abstract the computation of the backbone of CNF formulas. This could allow importing some solving technique into the algorithms for cautious reasoning in ASP, and also outlining relation between the computation of the backbone of CNF formulas and cautious reasoning in ASP. As an example, some algorithms from Janota et al. (2015) share numerous similari- ties with the ones described in this article; they contain over-approximation and under- approximation techniques as we have described. Other algorithms from Janota et al. (2015) include a more general version of under-approximation that allows to try to add several literals to the under-approximation at once. It is possible to include this “chunk” under- approximation in the framework we have defined in this article. Also, core-based methods presented in (Janota et al. 2015) use the unsatisfiable cores re- turned by SAT solvers in case a formula is unsatisfiable (see also Ası́n et al. (2008)). There is no published article describing such method for ASP, although there is no theoretical obstacle to its existence3 . In particular, in the case of ASP solvers based on SAT solvers, like CMODELS, one can easily imagine to use the core output by the underlying solver. Ab- stracting these core-based methods through graphs as we have defined in previous sections is possible, but properly defining and explaining such graphs would require substantially more space than allowed in this article. 6 Related Work and Conclusions Transition systems for describing solving procedures have been introduced by Nieuwen- huis et al. (2006) for the DPLL procedure of SAT solving and for certain extensions im- plemented in SMT solvers. In ASP, Lierler (2008) introduced and compared the transition systems for the answer set solvers SMODELS and CMODELS on non-disjunctive programs, then extended by Lierler (2011) by introducing transition rules that capture backjumping and learning techniques. Lierler and Truszczynski (2011) presented a unifying perspective based on completion of solvers for non-disjunctive answer set solving. Recently, Brochenin et al. (2014) presented transition systems for disjunctive answer set solvers CMODELS, GNT and DLV implementing plain backtracking. Lierler (2014) defined abstract frameworks for constraint answer set programming solvers, which solves problems that integrate ASP and constraint logic programming (Mellarkod et al. 2008). All these papers describe ASP procedures for brave reasoning. Our contribution focuses, 3 Our considerations about the feasibility of an ASP solver using core-based methods are corroborated by per- sonal conversations with people involved in the development of WASP . Additionally, at least one unpublished implementation of WASP is able to return a core, employing one method in (Ası́n et al. 2008). Abstract Answer Set Solvers for Cautious Reasoning 11 instead, on the description of ASP procedures for cautious reasoning. We show abstract procedures for the algorithms presented in Alviano et al. (2014), and outline how opti- mization techniques like backjumping, learning and restart, and techniques from backbone computation of CNF formulas, can be added to our graphs. Future work will be devoted to the precise characterization of these additions, and the inclusion in our framework. References A LVIANO , M., D ODARO , C., FABER , W., L EONE , N., AND R ICCA , F. 2013. WASP: A native ASP solver based on constraint learning. In Proceedings of the 12th International Conference of Logic Programming and Nonmonotonic Reasoning (LPNMR 2013), P. Cabalar and T. C. Son, Eds. Lecture Notes in Computer Science, vol. 8148. Springer, 54–66. A LVIANO , M., D ODARO , C., AND R ICCA , F. 2014. Anytime computation of cautious consequences in answer set programming. Theory and Practive of Logic Programming 14, 4-5, 755–770. A S ÍN , R., N IEUWENHUIS , R., O LIVERAS , A., AND RODR ÍGUEZ -C ARBONELL , E. 2008. Efficient generation of unsatisfiability proofs and cores in SAT. In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008). 16– 30. BARAL , C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cam- bridge University Press. B ROCHENIN , R., L IERLER , Y., AND M ARATEA , M. 2014. Abstract disjunctive answer set solvers. In Proceedings of the 21st European Conference on Artificial Intelligence (ECAI 2014). Frontiers in Artificial Intelligence and Applications, vol. 263. IOS Press, 165–170. DAVIS , M., L OGEMANN , G., AND L OVELAND , D. 1962. A machine program for theorem proving. Communications of the ACM 5(7), 394–397. E ITER , T., G OTTLOB , G., AND M ANNILA , H. 1997. Disjunctive Datalog. ACM Transactions on Database Systems 22, 3 (Sept.), 364–418. G EBSER , M., K AUFMANN , B., AND S CHAUB , T. 2012. Conflict-driven answer set solving: From theory to practice. Artificial Intellenge 187, 52–89. G ELFOND , M. AND L IFSCHITZ , V. 1988. The Stable Model Semantics for Logic Programming. In Proceedings of the 5th International Conference and Symposium on Logic Programming (ICLP/SLP 1988). MIT Press, Cambridge, Mass., 1070–1080. G ELFOND , M. AND L IFSCHITZ , V. 1991. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, 365–385. G IUNCHIGLIA , E., L EONE , N., AND M ARATEA , M. 2008. On the relation among answer set solvers. Annals of Mathematics and Artificial Intelligence 53, 1-4, 169–204. JANOTA , M., LYNCE , I., AND M ARQUES -S ILVA , J. 2015. Algorithms for computing backbones of propositional formulae. AI Communications 28, 2, 161–177. L EONE , N., P FEIFER , G., FABER , W., E ITER , T., G OTTLOB , G., P ERRI , S., AND S CARCELLO , F. 2006. The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic 7, 3, 499–562. L EONE , N., RULLO , P., AND S CARCELLO , F. 1997. Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation. Information and Computation 135(2), 69–112. L IERLER , Y. 2008. Abstract answer set solvers. In Proceedings of the 24th International Conference on Logic Programming (ICLP 2008), M. G. de la Banda and E. Pontelli, Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 377–391. L IERLER , Y. 2011. Abstract answer set solvers with backjumping and learning. Theory and Practice of Logic Programming 11, 135–169. 12 R. Brochenin and M. Maratea L IERLER , Y. 2014. Relating constraint answer set programming languages and algorithms. Artificial Intelligence 207, 1–22. L IERLER , Y. AND T RUSZCZYNSKI , M. 2011. Transition systems for model generators — a unifying approach. Theory and Practice of Logic Programming 11, 4-5, 629–646. M AREK , V. W. AND T RUSZCZY ŃSKI , M. 1998. Stable models and an alternative logic program- ming paradigm. CoRR cs.LO/9809032. M ELLARKOD , V. S., G ELFOND , M., AND Z HANG , Y. 2008. Integrating answer set programming and constraint logic programming. Annals of Mathematics and Artificial Intelligence 53, 1-4, 251–287. N IEMEL Ä , I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241–273. N IEUWENHUIS , R., O LIVERAS , A., AND T INELLI , C. 2006. Solving SAT and SAT modulo theo- ries: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937–977. R ICCA , F., FABER , W., AND L EONE , N. 2006. A backjumping technique for disjunctive logic programming. AI Communications 19, 2, 155–172. S IMONS , P., N IEMEL Ä , I., AND S OININEN , T. 2002. Extending and implementing the stable model semantics. Artificial Intelligence 138, 181–234.