Implementing the p-stable semantics Angel Marı́n George, Claudia Zepeda Cortés Benemérita Universidad Autónoma de Puebla, Facultad de Ciencias de la Computación misterilei@hotmail.com, czepedac@gmail.com Abstract. In this paper we review some theoretical results about the p-stable semantics, and based on that, we design some algorithms that search for the p-stable models of a normal program. An important point is that some of these algorithms can also be used to compute the stratified minimal models of a normal program. Key words: non-monotonic reasoning, p-stable, stratified minimal model 1 Introduction Currently, is a promising approach to model features of commonsense reasoning. In order to formalize NMR the research community has applied monotonic logics. In [7], Gelfond and Lifschitz defined the stable model semantics by means of an easy transformation. The stable semantics has been successfully used in the modeling of non-monotonic reasoning (NMR). Additionally, Pearce presented a characterization of the stable model semantics in terms of a collection of logics in [20]. He proved that a formula is “entailed by a disjunctive program in the stable model semantics if and only if it belongs to every intuitionistically complete and consistent extension of the program formed by adding only negated atoms”. He also showed that in place of intuitionistic logic, any proper intermediate logic can be used. The construction used by Pearce is called a weak completion. In [14], a new semantics for normal programs based on weak completions is defined with a three valued logic called G03 logic. The authors call it the P- stable semantics. In [12], the authors define the p-stable semantics for disjunctive programs by means of a transformation similar to the one used by Gelfond and Lifschitz in their definition of the stable semantics. The authors also prove that the p-stable semantics for disjunctive programs can be characterized by means of a concept called weak completions and the G03 logic, with the same two conditions used by Pearce to characterize the stable semantics of disjunctive programs, that is to say, for normal programs it coincides with the semantics defined in [14]. In fact, a family of paraconsistent logics studied in [12] can be used in this characterization of the p-stable semantics. In [13], the authors offer an axiomatization of the G03 logic along with a soundness and completeness theorem, i.e., every theorem is a tautology and vice-versa. We also remark that the authors of [12] present some results that 90 2 Angel Marı́n George, Claudia Zepeda Cortés give conditions under which the concepts of stable and p-stable models agree. They present a translation of a disjunctive program D into a normal program N , such that the p-stable model semantics of N corresponds to the stable semantics of D when restricted to the common language of the theories. Besides, they show that if the size of the program D is n then the size of the program N is bounded by An2 for a constant A. The relevance of this last result is that it shows that the p-stable model semantics for normal programs is powerful enough to express any problem that can be expressed with the stable model semantics for disjunctive programs. One major recent result of the p-stable semantics is in the context of argu- mentation theory [6], which explores ways to carry out into the theory of compu- tation the mechanisms humans use in argumentation. The three major semantics of argumentation theory (grounded, stable, and preferred) can be characterized in terms of three logic programming semantics: the well founded semantics [22], the stable semantics [7] and the p-stable semantics, respectively in terms of a unique normal logic program P , that is constructed only in terms of the ar- gumentation framework AF [3]. Argumentation theory does not depend on a particular semantics. Then, if we want to obtain the stable semantics of AF , we compute the stable semantics of logic programming over PAF . If, on the other hand, we want to obtain the preferred semantics of AF , we compute the p-stable semantics over PAF . Moreover, if we want to obtain the grounded semantics of AF , we compute the well founded semantics over PAF . There are also initial work about other two approaches for knowledge rep- resentation based on the p-stable semantics: updates, and preferences. In case intelligent agents get new knowledge and this knowledge must be added or up- dated to their knowledge base, it is important to avoid inconsistencies. An up- date semantics for update sequences of programs based on p-stable semantics is proposed in [15]. The concept of preferences is considered a vital component of reasoning with real-world knowledge. In [16], the authors introduce preference rules which allow us to specify preferences as an ordering among the possible solutions of a problem. Their approach allow us to express preferences for arbi- trary programs. They also define a semantics for those programs. The formalism used to develop their work is p-stable semantics. It is important to mention that the p-stable semantics, which can be de- fined in terms of paraconsistent logics, shares several properties with the stable semantics, but is closer to classical logic. For example, the following program P = {a ← ¬b, a ← b, b ← a} does not have stable models. However, the set {a, b} could be considered the intended model for P in classical logic. In fact, it is the only p-stable model of P . In [18], a schema for the implementation of the p-stable semantic using two well known open source tools: Lparse and Minisat is described. In [18], a pro- totype1 written in Java of a tool based on that schema is also presented. In this paper we present an implementation of the p-stable semantics implemen- tation with aim to improve the implementation presented in [18], considerable 1 http://cxjepa.googlepages.com/home 91 Implementing the p-stable semantics 3 effort has been made in the optimization the code and in the design of the al- gorithms used, which are theoretically more efficient than those used in [18]. As this implementation started recently, we have not yet made definitive tests to warrantee that the solver is error-free, nor we can give conclusive comparative tests between our implementation and that on [18]. In the section 2 the basic concepts about the p-stable semantics are intro- duced, specially the transformations. In the section 3 are presented the algo- rithms used to apply the transformations. In the section 4 and 5 is explained how to construct the graph of dependencies of the program and how this graph is used to reduce the search space when looking for the p-stable models. 2 Background In this section, we define some basic concepts in terms of logic programming semantics, including the definitions of the transformations, which are used to simplify a program. 2.1 Syntax A signature L is a finite set of elements that we call atoms. A literal is either an atom a, called positive literal, or the negation of an atom ¬a, called negative literal. Given a set of atoms {a1 , ..., an }, we write ¬{a1 , ..., an } to denote the set of atoms {¬a1 , ..., ¬an }. A normal clause or normal rule, r, is a clause of the form a ← b1 , . . . , bn , ¬bn+1 , . . . , ¬bn+m . where a and each of the bi are atoms for 1 ≤ i ≤ n + m, and the commas mean logical conjunction. In a slight abuse of notation we will denote such a clause by the formula a ← B + (r) ∪ ¬B − (r) where the set {b1 , . . . , bn } will be denoted by B + (r), the set {bn+1 , . . . , bn+m } will be denoted by B − (r), and B + (r) ∪ B − (r) denoted by B(r). We use H(r) to denote a, called the head of r. We define a normal program P , as a finite set of normal clauses. If for a normal clause r, B(r) = ∅, H(r) is known as a fact . We write LP , to denote the set of atoms that appear in the clauses of P . 2.2 Semantics From now on, we assume that the reader is familiar with the single notion of minimal model [8]. In order to illustrate this basic notion, let P be the normal program {a ← ¬b., b ← ¬a., a ← ¬c., c ← ¬a.}. As we can see, P has five models: {a}, {b, c}, {a, c}, {a, b}, {a, b, c}; however, P has just two minimal models: {b, c}, {a}. We will denote by M M (P ) the set of all the minimal models of a given logic program P . Usually M M is called minimal model semantics. Now we give the definition of p-stable model semantics for normal programs. 92 4 Angel Marı́n George, Claudia Zepeda Cortés Definition 1. [19] Let P be a normal program and M be a set of atoms. We define the reduction of P with respect to M as RED(P, M ) = {a ← B + ∪¬(B − ∩ M )|a ← B + ∪ ¬B − ∈ P }. Definition 2. [19] A set of atoms M is a p-stable model of a normal program P iff RED(P, M ) |= M , where the symbol |= means logical consequence under classical logic semantics. The set of p-stable models of P is denoted by P S(P ). We say that two normal programs P and P 0 are equivalent if and only if they have the same set of p-stable models, this relation is denoted by P ≡ P 0 . An important theorem relating the p-stable and minimal models is the following. Theorem 1. [14] Let P be a normal program. If M ∈ P S(P ) then M ∈ MM(P ). 2.3 Transformations preserving equivalence The main purpose of the transformations presented in this section is to simplify the input normal program, reducing its size. What allows the use of those trans- formations under the p-stable semantics are the propositions proved in [17, 4] about equivalence of normal programs under these transformations. Let P be a normal program, the definition of the transformations SUB, TAUT, RED− , RED+ , SUCC, LOOP, NAF and EQUIV when applied to P is as follows 1. SUB(P ) = P \ {r0 } ⇐⇒ r0 ∈ P , ∃r00 ∈ P : r0 6= r00 , B − (r00 ) ⊆ B − (r0 ), B + (r00 ) ⊆ B + (r0 ), H(r) = H(r0 ). 2. TAUT(P ) = P \ {r0 } ⇐⇒ r0 ∈ P , H(r0 ) ∈ B + (r0 ). 3. EQUIV(P ) = (P \ {r0 }) ∪ {r} ⇐⇒ r0 ∈ P, H(r0 ) ∈ B − (r0 ), B − (r) = B − (r0 ) \ {H(r0 )}, B + (r) = B + (r0 ), H(r) = H(r0 ). 4. SUCC(P ) = (P \ {r0 }) ∪ {r} ⇐⇒ r0 ∈ P, B − (r) = B − (r0 ), H(r) = H(r0 ), ∃r00 ∈ P : B(r00 ) = ∅, H(r00 ) ∈ B + (r0 ), B + (r) = B + (r0 ) \ {H(r00 )}. 5. RED+ (P ) = (P \ {r0 }) ∪ {r} ⇐⇒ r0 ∈ P, B + (r) = B + (r0 ), H(r) = H(r0 ), ∃a ∈ LP : a ∈ B − (r0 ), B − (r) = B − (r0 ) \ {a}, 6 ∃r00 ∈ P : H(r00 ) = a. 6. RED− (P ) = P \ {r0 } ⇐⇒ r0 ∈ P, ∃r00 ∈ P : B(r00 ) = ∅, H(r00 ) ∈ B − (r0 ). 7. NAF(P ) = P \ {r0 } ⇐⇒ r0 ∈ P, ∃a ∈ LP : a ∈ B + (r0 ), 6 ∃r00 ∈ P : H(r00 ) = a. 8. LOOP(P ) = {r0 : r0 ∈ P, B + (r0 ) ⊆ M }, where M is the unique minimal model of MM(POS(P )). The definition of POS(P ) is given by POS(P ) = {r0 : B − (r0 ) = ∅, ∃r ∈ P : B + (r) = B + (r0 ), H(r) = H(r0 )}. Proposition 1. [17, 4] Let P be a normal program, and let P 0 be the resulting program from the application to P of any of the transformations SUB, TAUT, EQUIV, SUCC, RED+ , RED− , NAF or LOOP. Then P ≡ P 0 . 3 Computing the p-stable models Now we present the implementation of a p-stable model solver. To find the p-stable models of a program P we can first apply the transformations to P , however the application of the transformations is not absolutely necessary nor sufficient to find the p-stable models of P . In this section we start presenting the implementation of the application of the transformations, and then we give three approaches to find the p-stable models of P , one that follows from the theorem 1, and the others from the theorem 2 which is also presented in this section. 93 Implementing the p-stable semantics 5 3.1 Implementing the transformations Given a program P as input to the p-stable solver, we associate to each atom a ∈ LP three sets that are used for the application of the transformations, those sets are initialized as follows, 1. H(a) = {r : r ∈ P, H(r) = a}. 2. P (a) = {r : a ∈ P, B + (r)}. 3. N (a) = {r : a ∈ P, B − (r)}. With the information in those sets it is efficient the application of some trans- formations, because it is avoided the use of a search algorithm, for example, it will not be necessary to search through all the program P when we require all the rules whose head is a particular atom a. Each atom a ∈ LP also has asso- ciated a variable state(a), which can hold one of the following values (we refer to this variable as the state of a): if state(a) = state f act then a is a fact, if state(a) = state no f act then a can not be a fact, if state undef ined then we can not tell yet if a is or can not be a fact. The application of the transformations TAUT and EQUIV is easily im- plemented, and in this paper we do not write the algorithms that apply those transformations. The transformations SUCC, RED+ , RED− , NAF and a par- ticular case of SUB are applied iteratively by the algorithm transf ormations iterated(...). This particular version of SUB consists in delet- ing the rules whose head is a fact. For the general case of SUB it is necessary to check for set inclusion between the bodies of all pairs of rules with the same head, some of our experimental implementations showed that it was very in- efficient and in most cases only a few rules were deleted. The LOOP trans- form was implemented using the Dowling-Gallier algorithm [5] (which finds the unique minimal model of a positive program in linear time) it is presented in the LOOP (...) algorithm. Also a watched variables scheme[9] might be used, this technique is effective in some cases when the deletion of atoms from rules needs to be continuously undone, but at this stage we do not need undo any changes. For the algorithm transf ormations iterated(...) we need two lists (see the algorithm at the end of the paper), they are Lp and Lf , which have to be initial- ized before calling to transf ormations iterated(...). Lp is initialized with the atoms that are facts, then for all a ∈ Lp it is assigned state(a) = state f act. Lf initialized with the atoms a such that there is no rule with head a, then for all a ∈ Lf it is assigned state(a) = state no f act. In transf ormations iterated(...) the auxiliary algorithms remove rule(r) and remove atom f rom rule(a, r, B) are used. remove rule(r) removes the rule r and if all the rules with head H(r) have been removed, set state(H(r)) = state no f act and add a to Lf . remove atom f rom rule(a, r, B) removes the atom a from B, where B = B + (r) or B = B − (r), if after removing a from B, |B| = 0, then set state(H(r)) = state f act and add a to Lp In the next example we illustrate how the algorithm transf ormations iterated(...) behaves with the program P as input 94 6 Angel Marı́n George, Claudia Zepeda Cortés Example 1. Example of the execution of transf ormations iterated P ={ Π1 ={ Π2 ={ r1 : u ← not v. r1 : u ← not v. r1 : u ← not v. r2 : v ← not u. r2 : v ← not u. r2 : v ← not u. r3 : u ← not r, not x, b. r3 : u ← not r, not x, b. r3 : u ← not r, not x, b. r4 : x ← y, r, not c. r4 : x ← y, r, not c. r4 : x ← y, r, not c. r5 : y ← not x, z, not v. r5 : y ← not x, z, not v. r5 : y ← not x, z, not v. r6 : x ← not z, t, not d. r6 : x ← not z, t, not d. r6 : x ← not z, t. r7 : z ← t, v. r7 : z ← t, v. r7 : z ← t, v. r8 : z ← r, not u, not x. r8 : z ← r, not u, not x. r8 : z ← r, not u, not x. r9 : r ← not t, not a. r9 : r ← not t, not a. r9 : r ← not t, not a. r10 : t ← not r, b. r10 : t ← not r, b. r10 : t ← not r, b. r11 : a ← not a, c. r11 : a ← c. r11 : a ← c. r12 : b ← not d. r12 : b ← not d. r12 : b ← . r13 : d ← c, d. r14 : c ← not a, b, d, z. r15 : c ← not b, a, x. r14 : c ← not a, b, d, z. r15 : c ← not b, a, x. r16 : b ← not a, not u.} r15 : c ← not b, a, x. r16 : b ← not a, not u.} Lp = {b}, Lf = {}. r16 : b ← not a, not u.} Lp = {}, Lf = {d}. Π3 ={ Π4 ={ Π5 ={ r1 : u ← not v. r1 : u ← not v. r1 : u ← not v. r2 : v ← not u. r2 : v ← not u. r2 : v ← not u. r3 : u ← not r, not x. r3 : u ← not r, not x. r3 : u ← not r, not x. r4 : x ← y, r, not c. r4 : x ← y, r. r4 : x ← y, r. r5 : y ← not x, z, not v. r5 : y ← not x, z, not v. r5 : y ← not x, z, not v. r6 : x ← not z, t. r6 : x ← not z, t. r6 : x ← not z, t. r7 : z ← t, v. r7 : z ← t, v. r7 : z ← t, v. r8 : z ← r, not u, not x. r8 : z ← r, not u, not x. r8 : z ← r, not u, not x. r9 : r ← not t, not a. r9 : r ← not t, not a. r9 : r ← not t. r10 : t ← not r. r10 : t ← not r.} r10 : t ← not r.} r11 : a ← c.} Lp = {}, Lf = {a}. Lp = {}, Lf = {}. Lp = {}, Lf = {c}. Before starting the transf ormations iterated(...) algorithm, the EQUIV and TAUT transformations are applied obtaining Π1 (this is an optional step), also Lp and Lf have to be initialized. Then we call transf ormations iterated(Π1 ). In the first iteration d is removed from Lf , we apply NAF and RED+ until d do not appear in the program, obtaining Π2 . In the second iteration remove b from Lp then apply SUB by removing all the rules whose head is b, then SUCC and RED− are applied until b do not appear in the program, obtaining Π3 . In the third iteration remove c from Lf , and apply NAF and RED+ until c do not appear in the program obtaining Π4 . In the fourth iteration remove a from Lf , and apply NAF and RED+ until a do not appear in the program obtaining Π5 . At this point Lp and Lf are empty making the algorithm stop. During the execution of transf ormations iterated(P ) have been removed all the rules whose head is a fact, including the rules r for which B(r) = ∅, which are precisely the rules that indicate that H(r) is a fact, it does not represent any problem because we can recover the atoms that are facts just by gathering the atoms whose state is state f act. As the transformations applied preserve equivalence, P ≡ Π5 ∪ {b ←}, we added the rule b ← to Π5 because state(b) = 95 Implementing the p-stable semantics 7 state f act. The state of all the atoms that were added to Lp was set to state f act (in this case {b}), and the state of the atoms that were added to Lf was set to state no f act ({d, a, c}), it means that b must be in all the p-stable models of P and {d, a, c} can not be in any. It is not hard to see that after the application of this algorithm we can no longer apply SUCC, RED− , RED+ or NAF. 3.2 The graph of dependencies In most cases the application of the transformations is not enough to find a p-stable model of a normal program, and other techniques are required. One of those techniques is to partition the program into sets of rules called modules. Those modules are created based on its graph of dependencies. Before explaining this technique in detail we give the next definition Definition 3. A strongly connected component C of a graph G is a subset of nodes of G. C is a maximal set of nodes(maximal respect to inclusion) such that there is a directed cycle in G that contains all the nodes in C. When we have the rule ah ← a1 , a2 , ..., am , not am+1 , not am+2 , ..., not an ., ah is dependent of all the a0i s, i = 1...n, in a graph this dependencies can be rep- resented with the directed edges (ai , ah ), i = 1, ..., n. The graph of dependencies of a program P represents all the dependencies between the atoms in LP , given by all the rules of P . The following definition states the definition of stratification and module of a program P . Definition 4. Let P be a normal program which can be partitioned into the disjoint sets of rules {P1 , ..., Pn }. Let Pi , Pj ∈ {P1 , ..., Pn }, Pi 6= Pj , we say that Pi < Pj if ∃r ∈ Pj : ∃r0 ∈ Pi : H(r0 ) ∈ B(r), if from this condition we do not conclude that Pi < Pj or Pj < Pi then we can choose to hold whether Pi < Pj or Pj < Pi as long as the following properties hold. For every X, Y, Z ∈ {P1 , ..., Pn }, the strict partial order relation properties and the totality property hold: 1. X < X is false (this property holds trivially). 2. If X < Y then (Y < X is false). 3. If (X < Y and Y < Z) then X < Z. 4. P1 < ... < Pn then we refer to this partition as the stratification of P , sometimes we will write it as P = P0 ∪ ... ∪ Pn . And we will refer to Pi , 1 ≤ i ≤ n as a module of P . Fortunately we do not have to worry about how to construct this order be- cause there exists a well known algorithm [21](that we implemented in the algo- rithm getM odules(P )) which obtains a sequence C1 , ..., Cn of strongly connected components of the graph of dependencies of P , from which we can construct a stratification of P , P = P1 ∪...∪Pn , where Pi = {r : r ∈ P, H(r) ∈ Ci }, 1 ≤ i ≤ n. Now we define h(Pi , P ) 96 8 Angel Marı́n George, Claudia Zepeda Cortés Definition 5. Let P be a normal program, Ci a strongly connected component of the graph of dependencies of P , and Pi the module constructed from Ci . We define h(Pi , P ) as the atoms which are represented as nodes in Ci . 3.3 Computing the p-stable models The purpose of this section is to show how to compute the p-stable models of a program, three approaches to find the p-stable models of a program P are presented. One way is a direct application of the theorem 1, it consist in com- puting the minimal models of P and choosing those which satisfy the definition of p-stable model. By theorem 2 the p-stable models of P can be computed by computing the p-stable models of the modules of P after the application of certain transformations. Theorem 2. [19] Let P be a normal logic program, and M a model of P with stratification P = P1 ∪ P2 , then RED(P, M ) |= M iff RED(P1 , M1 ) |= M1 and RED(P20 , M2 ) |= M2 with P20 , M1 , and M2 defined as follows: M = M1 ∪ M2 , M1 = h(P1 , P ) ∩ M , M2 = h(P2 , P ) ∩ M , and P20 is obtained by transforming P2 as follows: 1. Removing from P2 the rules r0 such that B − (r0 ) ∩ M1 6= ∅ or B + (r0 ) ∩ (h(P1 , P ) \ M1 ) 6= ∅, obtaining a new program P200 . 2. For every r ∈ P200 , removing from B(r) the occurrences of the atoms in h(P1 , P ), obtaining P20 . In other words M is a p-stable model of P iff M1 is a p-stable model of P1 and M2 is a p-stable model of P20 , where P20 is obtained by removing from P2 the occurrences of the atoms in h(P1 , P ) according to the theorem 2. If P can be stratified as P = P1 ∪ ... ∪ Pn , n > 2, then P = P1 ∪ Q with Q = P2 ∪ ... ∪ Pn is also an stratification of P that has only two modules, and then we can apply the theorem 2. From theorems 1 and 2, three different approaches to compute the p-stable models of a program P are known. The first approach has been implemented in [18]. We propose the other two approaches that reduce the search space respecto to the first approach in many practical examples. 1. From theorem 1, it follows that in order to find the p-stable models of P , we can generate minimal models M ∈ MM(P ) and accept as p-stable models those for which the consequence test RED(P, M ) |= M is true. To implement the consequence test we take advantage of the fact that RED(P, M ) |= M ⇐⇒ RED(P, M ) ∪ {¬M } is unsatisfiable, to test if RED(P, M ) ∪ {¬M } is unsatisfiable it is used a SAT solver, in this case we used MINISAT[1], the consequence test is implemented in the algorithm consequence test(...)(not presented here for lack of space). Using this approach the search space to find the p-stable models of P is M M (P ). The computation of the p-stable models following this approach is implemented in new P S(...). 97 Implementing the p-stable semantics 9 2. As we have said, if P can be stratified into n modules P = P1 ∪ ... ∪ Pn , then P can also be stratified into two modules P = P1 ∪ Q, where Q = P2 ∪ ... ∪ Pn , n > 2, and now we can apply the theorem 2 to find the p- stable models of P , this approach is based on the fact that Q0 (obtained from Q according to theorem 2) can be stratified as Q0 = Q2 0 ∪ ... ∪ Qn 0 where Qi 0 , 2 ≤ i ≤ n is obtained by removing from Pi the occurrences of LP1 according to theorem 2. If n > 3, to compute the p-stable models of Q0 , we argument the same way but now instead of P , we have Q0 with stratification Q0 = Q2 0 ∪ ... ∪ Qn 0 . We can proceed this way whenever we want to compute the p-stable models of a program stratified into more than two modules, when it only has two modules, we just apply the theorem 2. The search space to find all the p-stable models of a program P using this approach is in the worst case M M (P ), but sometime this search space is bigger than in the third approach. The advantage of this approach over the third approach is that it is not necessary to compute the stratification of a module before computing its p-stable models, we compute only once the stratification of P . 3. Again following the theorem 2, to compute a p-stable model of P with strat- ification P = P1 ∪ P2 (as we have said a program with n modules can also be stratified into two modules), we can compute a p-stable model of P1 and one p-stable model of P20 , and if P20 can be stratified into P20 = Q1 ∪ Q2 , we can apply again the theorem and compute the p-stable models of Q1 and Q02 . The difference with the second approach is that in the second approach the stratification is computed only once, and in this approach we compute the stratification with getM odules(...) each time we want to compute a p-stable model of a module. Using this approach the search space is in many cases considerably smaller than M M (P ), this is because the problem of finding the p-stable models of a program is translated into the problem of finding the p-stable models of many small subprograms, the smaller these subprogram, more chances are to reduce the search space. We distinguish between finding the first and the subsequent p-stable models, to find the first p-stable model use the f irst P S recursive(...) algorithm and to find the another p-stable model use next P S recursive(...). We illustrate the second approach by finding the p-stable models of the pro- gram Π5 that resulted from the application of the transformations in the example 1. In the graph 1 we see the graph of dependencies of Π5 , the dotted edges trace maximal cycles, and determine the strongly connected components of Π5 . 98 10 Angel Marı́n George, Claudia Zepeda Cortés Based on the graph of dependencies of Π5 (graph 1), we see that Π5 can be stratified into two modules Π5 = P1 ∪ P2 . To compute a p-stable model of Π5 we start by finding a p-stable model of P1 , in this case we found {r} to be a p-stable model of P1 . Then compute P20 by removing the occurrences of the atoms r and t from P2 according to the theorem 2, in the next figure you can see P1 , P2 and P20 P2 ={ P1 ={ r1 : u ← not v. r9 : r ← not t. r2 : v ← not u. r10 : t ← not r.} r3 : u ← not r, not x. P20 = { r4 : x ← y, r. r1 : u ← not v. r5 : y ← not x, z, not v. r2 : v ← not u. r6 : x ← not z, t. r4 : x ← y. r7 : z ← t, v. r5 : y ← not x, z, not v. r8 : z ← r, not u, not x.} r8 : z ← not u, not x.} Then find a minimal model of P20 and do the consequence test, a mini- mal model of P20 is {v, x}, but when doing the consequence test we find that RED(P20 , {v, x}) ∪ {¬{v, x}} = RED(P20 , {v, x}) ∪ {¬v ∨ ¬x} is satisfiable, thus {v, x} is not a p-stable model of P20 . We generate another minimal model of P20 , {v, z}, this time RED(P20 , {v, z}) ∪ {¬v ∨ ¬z} is unsatisfiable and {v, z} is accepted as a p-stable model of P20 . Merging the p-stable model of P1 and the p-stable model of P20 we obtain a p-stable of Π5 , {r, v, z}. To look for another p-stable model of Π5 , we start by looking for another p-stable model of P20 , we find that {u} is a p-stable model of P20 , for instance another p-stable model of Π5 is {r, u}. Again we try to generate another p-stable model of P20 , but we note that all the p-stable models of P20 have been generated (all M ∈ M M (P20 ) have been computed), then we go to the anterior module(P1 ) and try to generate another p-stable model of P1 , we find that {t} is another p-stable model of P1 , then compute P20 again : P20 ={ r1 : u ← not v. r2 : v ← not u. r3 : u ← not x. r5 : y ← not x, z, not v. r6 : x ← not z. r7 : z ← v.} 99 Implementing the p-stable semantics 11 We encounter the two p-stable models of P20 , {{x, u}, {x, v}}, from which we find another two p-stable models of Π5 , {{t, x, u}, {t, x, v}}. When trying to generate another p-stable model of P20 we can not find any so we go to P1 , and can not find another p-stable model of P1 so we stop. We end up with the four p- stable models of Π5 , PS(Π5 ) = {{t, x, u}, {t, x, v}, {r, v, z}, {r, u}}. Recall form the example 1 that b was found to be a fact after the application of the transfor- mations to P , for instance PS(P ) = {{b, t, x, u}, {b, t, x, v}, {b, r, v, z}, {b, r, u}}. When using the third approach, we stratify Π5 into Π5 = P1 ∪ P2 as in the second approach, but after obtaining P20 , try to stratify P20 , we can see in the graph of dependencies of P20 (graph 2), that P20 can be stratified into two modules, so P20 is stratified into P20 = Q1 ∪Q2 which can be seen in the next figure Q1 ={ r1 : u ← not v. R1 ={} r2 : v ← not u.} Q02 ={ R2 ={x ← y.} Q2 = { r4 : x ← y. R3 ={z ← not x.} r4 : x ← y. r8 : z ← not x.} R20 ={} r5 : y ← not x, z, not v. R30 ={z ←.} r8 : z ← not u, not x.} Applying again the theorem 2, first choose a minimal model of Q1 , {v} and when doing the consequence test we find that {v} is a p-stable model of Q1 . Now obtain Q02 (see the anterior figure) which is further partitioned into Q02 = R1 ∪ R2 ∪ R3 which are respectively the sets of rules with head y, x and z. Then compute a p-stable model of R1 , the only p-stable model of R1 is the empty set, R20 is also empty and also has an empty p-stable model. R30 (obtained by removing from R3 the occurrences of LR1 and LR2 ) only has an empty rule z ← and its unique p-stable model is {z}. Merging the p-stable model of the modules P1 , Q1 , R1 , R20 and R30 we get a p-stable model of Π5 , it is {r} ∪ {v} ∪ {} ∪ {} ∪ {z} = {r, v, z}. When trying to generate another p-stable model, first we try to generate another p-stable model of R30 , it does not have more p-stable models, thus we go back and try on R20 but it has neither, then try on R1 that has no more p-stable models, finally we find that Q1 has another p-stable model, {u}, from this point, to find the other p-stable models of Π5 , we proceed as we did when we had {v} as a p-stable model of Q1 . To show the performance of each approach we use some examples in [2]. In the next table we can see the time in seconds it took to find a p-stable model of some of those examples using each of the three approaches. A ”-” character means that we stopped the execution after 10 seconds. In the fifth column is the time to find a stable model by smodels. The sixth and seventh columns show the number of atoms and rules of each test program. In the last column is the number of modules in which the program was initially partitioned. 100 12 Angel Marı́n George, Claudia Zepeda Cortés problem app. 1 app. 2 app. 3 smodels atoms rules modules blocks world - 4 .14 .228 2848 28238 600 blocks world variant - .15 .18 .188 3227 28817 487 n queens .01 1.24 .83 .016 149 1539 3 spanning tree .14 .05 .1 .008 930 1572 276 planning from initial - .21 .2 .26 4910 41439 510 weight constraints .26 .22 .23 .228 887 29662 115 planning in observations - - - 6.172 24639 1098619 22100 It is worth to mention that if we modify the consequence test(...) such that it always return true, instead of using tranf ormations iterated(...) we apply some similar reductions (see [10]), and if all the tautological rules like a ← b, not b, c are removed, then we end up with a stratified minimal model solver, a detailed description of our stratified minimal model semantics solver can be found in [10]. 4 Conclusions and future work Some preliminary tests to the p-stable solver presented in this paper, shows a bad performance respect to a stable semantics solver(smodels[11]), for big programs, due to the backtracking driven by the failure of the consequence test, one of the inconveniences of this implementation is that the search space is very big for some programs, research is needed to develop algorithms that reduce the search space or heuristics that show a good performance for some classes of programs. 101 Implementing the p-stable semantics 13 Algorithm 1 function getM odules() ModuleList modules {list of modules} create the graph of dependencies G numerate the nodes of G according to the DFS exiting time transpose the graph(compute GT ) Do a DFS(depth first search), and in the main loop choose the nodes with bigger exiting time first. {Each tree found by the DFS represents a strongly connected component} for each strongly connected component c do create a new module mod for each atom a in c do add to mod all the rules r that H(r) = a end for modules.add(mod) end for Algorithm 2 function transf ormations iterated(M odule P )) {when P is a module obtained from the stratification of a bigger set of rules, use {r ∈ P : a ∈ B + (r)} instead of P (a), and use {r ∈ P : a ∈ B − (r)} instead of N (a)} global List Lp,Lf while |Lp ∪ Lf | > 0 do if Lp is not empty then a = Lp.removeElement() {apply a partial version of SUB} remove all rules in H(a) for all r in P (a) do {apply SUCC} remove atom f rom rule(a, r, B + (r)) end for for all r in N (a) do {apply RED− } remove rule(r) end for else a = Lf.removeElement() for all r in P (a) do {apply NAF } remove rule(r) end for for all r in N (a) do {apply RED+ } remove atom f rom rule(a, r, B − (r)) end for end if end while 102 14 Angel Marı́n George, Claudia Zepeda Cortés References 1. 2. Chitta Baral. Knowledge representation, reasoning and declarative problem solv- ing. http://www.baral.us/bookone/code/smodels.html. 3. J. Carballido, J.C. Nieves, and M. Osorio. Inferring preferred extensions by pstable semantics. Accepted in Revista Iberomericana de Inteligencia Artificial, 2008. 4. J. L. Carballido. PhD thesis, BUAP, 2008. 5. W.F. Dowling and J.H. Gallier. Linear time algorithm for testing the satisfiability of propositional horn formulae. Journal of logic programming, 1984. 6. Phan Minh Dung. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77(2):321–358, 1995. 7. Michael Gelfond and Vladimir Lifschitz. The Stable Model Semantics for Logic Programming. In R. Kowalski and K. Bowen, editors, 5th Conference on Logic Programming, pages 1070–1080. MIT Press, 1988. 8. John W. Lloyd. Foundations of Logic Programming. Springer, Berlin, second edition, 1987. 9. Yuting Zhao Lintao Zhang Matthew H. Moskewicz, Conor F. Madigan and Sharad Malik. Chaff. Chaff: Engineering an efficient sat solver. In DAC 01: Pro- ceedings of the 38th Conference on Design Automation, Las Vegas, NV, USA, June 2001., 2001. 10. Angel Marin George Mauricio Osorio, Juan Carlos Nieves. Computing the stratified minimal models semantic(unpublished). 2009. 11. Ilkka Niemela and Patrik Simons. Smodels - an implementation of the stable model and well-founded semantics for normal logic programs. volume 1265 of Lecture Notes in Artificial Intelligence (LNCS), pages 420–429, 1997. 12. Mauricio Osorio, José Arrazola, and José Luis Carballido. Logical weak comple- tions of paraconsistent logics. Journal of Logic and Computation, Published on line on May 9, 2008. 13. Mauricio Osorio and Jose Luis Carballido. Brief study of G’3 logic. To appear in Journal of Applied Non-Classical Logic, 18(4):79–103, 2009. 14. Mauricio Osorio, Juan Antonio Navarro, José Arrazola, and Verónica Borja. Logics with common weak completions. Journal of Logic and Computation, 16(6):867–890, 2006. 15. Mauricio Osorio and Claudia Zepeda. Update sequences based on minimal gener- alized pstable models. In MICAI, pages 283–293, 2007. 16. Mauricio Osorio and Claudia Zepeda. Pstable theories and preferences. In Elec- tronic Proceedings of the 18th International Conference on Electronics, Communi- cations, and Computers (CONIELECOMP 2008), March, 2008. 17. S. Pascucci and A. Lopez. Syntactic transformation rules under p-stable semantics: theory and implementation. 2009. 18. S. Pascucci and A. Lopez. Implementing p-stable with simplification capabilities. Submmited to Inteligencia Artificial, Revista Iberoamericana de I.A., Spain, 2008. 19. Simone Pascucci. Syntactic properties of normal logic program under pstable se- mantics: theory and implementation. Master’s thesis, March 2009. 20. David Pearce. Stable Inference as Intuitionistic Validity. Logic Programming, 38:79–91, 1999. 21. Clifford Stain Thomas H. Cormen, Charles E. Leiserson Ronald L. Rivest. 22. Allen van Gelder, Kenneth A. Ross, and John S. Schlipf. The well-founded seman- tics for general logic programs. Journal of the ACM, 38:620–650, 1991. 103 Implementing the p-stable semantics 15 Algorithm 3 function LOOP(M odule P ) {for this algorithm it is necessary to associate to each rule r an integer pCount(r) and to each atom a a boolean of M M (a). } List prop initialize pCount(r) = |B + (r)| for each rule r initialize of M M (a) = f alse for each atom a initialize prop = {a ∈ LP : ∃r ∈ P : H(r) = a, B + (r) = ∅} { sets of M M (a) = true iff a ∈ M M (POS(P )) } while |prop| > 0 do a = prop.remove element() set of M M (a) = true for each r such that a ∈ B + (r) do pCount(r) = pCount(r) − 1 if pCount(r) = 0 then prop.add(H(r)) end if end for end while {removes rules r for which of M M (a) = f alse and a ∈ B + (r) } for each atom a for which of M M (a) = f alse do for each r in P (a) do remove rule(r) end for end for 104 16 Angel Marı́n George, Claudia Zepeda Cortés Algorithm 4 function bool new P S(M odule P ) {solver is a MINISAT solver associated to P , IDS(a) is the integer that represents the atoms a in solver, when solver = N U LL no models of P have been computed} if solver = N U LL then transf ormations iterated(P ) end if if the number of atoms in LP whose state is state undef ined is >= 2 then {initialize solver} if solver = N U LL then solver=new solver() add to solver all the rules in P set i = −1 for each a ∈ LP for which state(a) = state undef ined do solver.newV ar() set IDS(a) = + + i end for end if {generates minimal models of P , returns true if the consequence test returns true} while solver.solve() do if consequence test(solver.model) then {create a clause lits with the model generated but negated} for each atom a in the solver do if solver.model[IDS(a)] = l T rue then set state(a) = state f act lits.push(∼ IDS(a)) else set state(a) = state no f act end if end for {add the clause to the solver to generate a different minimal model the next iteration} if i > 0 then solver.addClause(lits) else add to solver the clauses {a} and {¬a} for some atom a end if return true end if end while {returns false because no p-stable model of P was found} solver=NULL return false else {there is nothing to solve, the p-stable model was found by transf ormations iterated(P )} if solver 6= N U LL then set solver = N U LL return false else set solver = (Solver∗)1{just assign a non-NULL value} return true end if end if 105 Implementing the p-stable semantics 17 Algorithm 5 function bool f irst P S recursive(M odule P ) {stratify(P) returns true iff P could be stratified into more than two modules } {If P is stratified into P = P1 ∪ ... ∪ Pn , as the modules Pi are in the list submodules, head(submodules(P )) = P1 , rear(submodules(P )) = Pn , next(Pi ) = Pi+1 1 <= i < n, back(Pi ) = Pi−1 1 < i <= n, next(Pn ) = back(P1 ) = N U LL} if stratif y(P ) then reductions iterated(P ) set Q = head(submodules(P )) {picks the first element of submodules(P )} if not new P S(Q) then return false end if set Q = next(Q) while Q 6= N U LL {visits all the modules in submodules(P )} do while not f irst P S recursive(Q) do {backtracking} if not next P S recursive(back(Q)) then return false end if end while set Q = next(Q) end while else if not new P S(P ) then return false end if end if return true Algorithm 6 function bool next P S recursive(P ) repeat {if P was not divided into more than one modules} if |submodules(P )| = 0 then if new P S(P ) then return true end if else Q = rear(submodules(P )) if next P S recursive(Q) then return true end if end if if back(P ) = N U LL or not next P S recursive(back(P )) then return false end if {leaves the module as it was when created} reset component(P ) until f irst P S recursive(P ) return true 106