=Paper=
{{Paper
|id=Vol-533/paper-6
|storemode=property
|title=Implementing the p-stable semantics
|pdfUrl=https://ceur-ws.org/Vol-533/08_LANMR09_05.pdf
|volume=Vol-533
|dblpUrl=https://dblp.org/rec/conf/lanmr/GeorgeC09
}}
==Implementing the p-stable semantics==
https://ceur-ws.org/Vol-533/08_LANMR09_05.pdf
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