Assat: Computing Answer Sets of a logic Program By sat solvers


Download 326.53 Kb.

bet2/4
Sana28.03.2017
Hajmi326.53 Kb.
1   2   3   4

j

. Suppose otherwise,



there is a maximal loop L in S

j

for which r



∈ R

+

(L, S



j

). Now let L

be the maximal loop in S

i

used in the construction of S



i+1

. Then since

9


the head of r, p

k

, is an element in both L and L , L



∪ L is also a loop

in S


j

. So L


⊆ L as L is maximal. Now since r is deleted from S

j

,



by the construction of S

j+1


, all rules in R

+

(L, S



j

) whose head is p

k

are


also deleted. So there are no rules in R

+

(L , S



i

) whose head is p

k

, a


contradiction with the selection of r in the construction of S

i+1


.

• For each atom p ∈ A, there is a rule in S whose head is p. We prove this

by induction. We have shown this for S

0

as A is a model of Comp(P ).



Suppose that this is true for S

i

, we prove it below for S



i+1

. If there is

no loop in S

i

, then this is trivially true. Suppose it has a loop. By the



construction of S

i+1


, it is the result of deleting some of the rules in S

i

whose heads are identical to the head of the rule r :



p

k

← G used



in the construction. So for any atom p

∈ A that is different from p

k

,

there is a rule for it in S



i

by our inductive assumption, and the same

rule is also in S

i+1


by our construction. Now for this atom p

k

, as we



have shown above, r

∈ S


i+1

, which is a rule for p

k

.

• For every p ∈ A, S |= p. We prove this by contradiction using induc-



tion. Notice that we have proved the following by now: (1) for each

p

∈ A, there is a rule in S whose head is p; (2) for each rule in S,



both the head and the body are true in A; and (3) S does not have

any loops. Assume that there exists p

0

∈ A, s.t. S |= p



0

. Construct a

set of sequences of atoms in A inductively as follows. First of all, let

T

0



=

{p

0



}. Clearly, T

0

satisfies the following properties for T :



– T is a sequence of distinct atoms in A.

– None of atoms in T is entailed by S.

– If p

i

and p



i+1

are two consecutive elements in T , then p

i

depends


on p

i+1


in the sense that there is a rule p

i

← G in S such that



p

i+1


∈ G.

Suppose that we have a sequence T

k

= [p


0

, ..., p


k

] with the above prop-

erties, construct T

k+1


as follows: Let p

k

← G



k

be a rule in S. Since

S

|= p


k

, G


k

=

∅ and S |= G



k

. Thus there must exist p

k+1

∈ G


k

,

s.t. S



|= p

k+1


. Since S is loop free, and each of the atoms in T

k

de-



pends on the next one, so for any i, 0

≤ i ≤ k, p

k+1

= p


i

. Now let

T

k+1


= [p

0

,



· · · , p

k

, p



k+1

]. One can see that T

k+1

so constructed also



satisfies the two properties about T above. But this is impossible as

A is finite and we could construct T

k

this way for arbitrary k.



10

Thus P

A

|= p as S ⊆ P



A

. Now if P

A

|= p, then it must be the case that



p

∈ A as A is a model of Comp(P ), thus a model of P

A

taken as a set of



clauses. This proves that if A is a model of Comp(P )

∪ LF , then A is an

answer set of P .

Now suppose A is an answer set of P , then clearly A is a model of

Comp(P ). We need to show that A is also a model of LF . We prove this

by contradiction. Suppose L is a loop in P , and LF (L) its loop formula.

Suppose R

(L) in P is:



r

1

: p



1

← G


1

, G


1

,

. . .



r

n

: p



n

← G


n

, G


n

,

where G



i

is a set of atoms and G

i

a set of negative literals. If A does not



satisfy LF (L), then there must be a p

∈ L such that p ∈ A, and for each

rule r

i

in R



(L), A


|= G

i

∧ G



i

. Now if the following set of rules is the

Gelfond-Lifschitz reduct of R

(L) on A:



r

a

1



: p

a

1



← G

a

1



,

. . .


r

a

k



: p

a

k



← G

a

k



,

1

≤ a



i

≤ n, then for each 1 ≤ i ≤ k, A |= G

a

i

. Since p



∈ A, Cons(P

A

)



|= p.

So there must be a sequence of rules in P

A

:

r



1

: q


1

← Q


1

,

. . .



r

u

: q



u

← Q


u

.

s.t. q



u

= p, Q


1

=

∅, and for each 1 < i ≤ u, Q



i

⊆ {q


1

,

· · · , q



i−1

}. In this

sequence, there must be a v, 1

≤ v ≤ u, s.t. {q

1

,

· · · , q



v−1

} ∩ L = ∅ and

q

v

∈ L. Since Q



v

⊆ {q


1

,

· · · , q



v−1

}, Q


v

∩ L = ∅. So r

v

must be a reduct of a



rule in R

(L), i.e. for some 1



≤ i ≤ k, r

v

= r



a

i

. But this is a contradiction



as A must satisfy the body of r

v

but not that of r



a

i

. This proves that if A is



an answer set of P , then A is a model of Comp(P )

∪ LF .


The proof of the theorem also shows the following result:

11


Proposition 1 If S is a model of Comp(P), then S is an answer set of P

iff there is a P

⊆ P such that P does not have any loops, S satisfies the

body of every rule in P , and there is a rule in P for every atom in S.

4

Computing loops



By Theorem 1, a straightforward approach of using SAT solvers to compute

the answer sets of a logic program is to first compute all loop formulas, add

them to its completion, and call a SAT solver. Unfortunately this may not be

practical as there may be an exponential number of loops in a logic program.

For an example, consider the following program by Niemel¨

a [18] for finding

Hamiltonian cycles of a graph:

r

1



: hc(V 1, V 2)

← arc(V 1, V 2), not otherroute(V 1, V 2).

r

2

: otherroute(V 1, V 2)



← arc(V 1, V 2), arc(V 1, V 3),

hc(V 1, V 3), V 2 = V 3.

r

3

: otherroute(V 1, V 2)



← arc(V 1, V 2), arc(V 3, V 2),

hc(V 3, V 2), V 1 = V 3.

r

4

: reached(V 2)



← arc(V 1, V 2), hc(V 1, V 2), reached(V 1),

not initialnode(V 1).

r

5

: reached(V 2)



← arc(V 1, V 2), hc(V 1, V 2), initialnode(V 1).

initialnode(0).

r

6

:



← vertex(V ), not reached(V ).

For complete graphs, rule r

4

, when fully instantiated, will give rise to a loop



for every set of vertices.

Thus, it seems more practical to add loop formulas one by one, selectively.

This motivates the following procedure.

Procedure 1

1. Let T be Comp(P ).

2. Find a model M of T . If there is no such model, then terminate with

failure.

3. If M is an answer set, then exit with it (go back to step 2 when more

than one answer sets are needed).

12


4. If M is not an answer set, then find a loop L such that its loop formula

Φ

L



is not satisfied by M .

5. Let T be T

∪ {Φ

L

} and go back to step 2.



By Theorem 1, this procedure is sound and complete, provided a sound

and complete SAT solver is used.

The two key questions regarding this

procedure are as follows:

1. Are SAT solvers suitable for this purpose?

2. How to find a loop such that its loop formula is not satisfied by the

current model in step 4?

Question 1 is empirical. For programs without loops, experiments done by

Babovich et al. [2] and Huang et al. [8] pointed to a positive answer to this

question. Our experiments on logic programs, including those with loops,

seem to confirm this.

Question 2 is really the key to this procedure. If a set M of atoms is a

model of Comp(P ) but not an answer set of P , then by Theorem 1, there

must be a loop whose loop formula is not satisfied by M . But how hard it is

to find such a loop? As it turns out, such a loop can be found in polynomial

time. The key lies in the following set:

M



= M



− Cons(P

M

).



(Recall that P

M

is the Gelfond-Lifschitz reduct of P on M , and Cons(P



M

)

is the set of consequences of P



M

.)

Lemma 1 If M is a model of Comp(P ), then Cons(P



M

)

⊆ M.



Proof: We prove this by induction. Suppose Cons(P

M

) is not empty, then



for any p

∈ Cons(P


M

), there must be a sequence of rules in P

M

:

p



1

← G


1

,

. . .



p

k

← G



k

.

s.t. p



k

= p, G


1

=

∅, and for 1 < i ≤ k, G



i

⊆ {p


1

, . . . , p

i−1

}.

Let S



0

=

{p | p ← . ∈ P



M

}. Since Cons(P

M

) =


∅, S

0

=



∅. Now for any

p

∈ S



0

, there must be a corresponding rule r : p

← G



in P , s.t. G



is either

13


empty or a set of negative literals which are satisfied by M . Since M is a

model of P , p

∈ M. So we have S

0

⊆ M. Suppose we have S



k

, and S


k

⊆ M.


Construct S

k+1


as: S

k+1


= S

k

∪ {p | r : p ← G



ki

∈ P


M

and G


ki

⊆ S


k

}.

For any p



∈ S

k+1


− S

k

, let the rule about p in P



M

be r : p


← G

ki

and



the one in P be r : p

← G


ki

, G


ki

, since G



ki

⊆ S


k

and S


k

⊆ M, G


ki

⊆ M.


Considering that r is the Gelfond-Lifschitz reduct of r, G

ki



is satisfied by

M , so M satisfies the body of r. Since M is a model of Comp(P ), p

∈ M.

So we have S



k+1

⊆ M.


Let S =

i=0,1,...

S

i

, then S = Cons(P



M

). So we have Cons(P

M

)

⊆ M.



Lemma 2 For any p

∈ M


, there must be a rule p

← G about p in P

M

such



that G contains some q

∈ M


. Furthermore, any such rule about p in P

M

must have this property, i.e. its body contains an atom in M



.

Proof: Since p is in M , and M satisfies Comp(P ), there must be a rule



about p in P whose body is satisfied by M . If G is the positive literals in the

body of this rule, then p

← G must be in P

M

. Now G must have an atom in



M

, otherwise, they must be all in Cons(P



M

), which means that p must be

in Cons(P

M

) as well, a contradiction with p



∈ M

.



From this Lemma, the following proposition follows easily.

Proposition 2 There is at least one loop L in P such that L

⊆ M



. Fur-



thermore, for any p

∈ M


, there must be a loop L

⊆ M



such that for some



q

∈ L, there is a (directed) path from p to q in G

P

.

Proof: Let p



∈ M

, then by Lemma 2 and the construction of ∆, there



must be a q

∈ M


such that (p, q) is an arc in ∆. Since p is any node, and ∆

has only finite number of nodes, so this must lead to a cycle, thus a strongly

connected component reachable from p.

Definition 3 Let P be a program, and G

P

its positive dependency graph.



Let M be a model of Comp(P ). We say that a loop L of P is a maximal

loop under M if L satisfies the following two conditions:

1. L

⊆ M


, and


14

2. L is maximal in M

, i.e. there is no other loop L



⊆ M

such that



L

⊂ L .


In other words, L is a strongly connected component of the subgraph of G

P

induced by M



. A maximal loop L under M is called a terminating one if

there does not exist another maximal loop L

1

under M such that for some



p

∈ L and q ∈ L

1

, there is a path from p to q such that all vertices in the



path are in M

.



Theorem 2 If M is a model of Comp(P ) but not an answer set of P , then

there must be a terminating loop of P under M . Furthermore, M does not

satisfy the loop formula of any of the terminating loops of P under M .

Proof: By Proposition 2, there is a loop in M

. Since M



is finite, there

must be a maximal loop under M . Suppose now there are no terminating

loops. Since G

P

is finite, there must be more than one maximal loops under



M , and there will be a path from any maximal loop under M to any other

maximal loop under M in the subgraph of G

P

induced by M



. This means

that the union of all these maximal loops is also a maximal loop under M , a

contradiction with the fact that there are more than one maximal loops. So

there must be a terminating loop under M .

Now let α be a terminating loop on M . Its loop formula in P is of the

form:

(

¬G



1

∧ · · · ∧ ¬G

n

)

⊃ (¬p



1

∧ · · · ∧ ¬p

k

),

where p



i

’s are atoms in α, and G

i

’s are the bodies of rules in R



(α, P ). Since

α

⊆ M


⊆ M, to show that M does not satisfy this formula, we only need

to show that for any p

∈ α, and any rule p ← G that is in R

(α), M


|= ¬G.

Suppose M

|= G, then p ← G

+

is in P



M

, where G

+

is the set of positive



literals in G. Now there are two cases: Case 1: G

+

does not contain any



atom in M

, in this case G



+

must be in Cons(P

M

), this means that p must



be in Cons(P

M

) as well, a contradiction with our assumption that p



∈ M

;



Case 2: G

+

contains a q



∈ M

, in this case, by Proposition 2 there must be



a loop, thus a maximal loop β under M such that there is a path from q to

an atom in β. This means that there is a path from p to an atom in β as

well. Since p

← G is not in R

+

(α), q is not in α, so α must be different from



β, a contradiction with the assumption that α is a terminating and maximal

loop.


15

Thus given a model M of Comp(P ), if it is not an answer set, then

the problem of finding a loop whose loop formula is not satisfied by M can

be reduced to the problem of finding a terminating loop under M . Notice

that a terminating loop under M is a strongly connected component in the

subgraph of G

P

induced by M



, and that the strongly connected components

of a graph and their dependency chains can be computed in O(n+e) time[22],

where n is the number of nodes and e the number of arcs in the graph. So a

terminating loop under M can be found in O(m + k) time, where m is the

size of M

, and k the number of arcs in the subgraph of G



P

induced by M

.

Normally M



is quite small compared to the number of atoms in P . Once

we have identified a loop, its loop formula can be computed in time similar

to that for computing the completion of a program.

5

ASSAT(X)


ASSAT(X), where X is a SAT solver, is an implemented system based on

Procedure 1 in the last section:

ASSAT(X) – X a SAT solver

1. Instantiate a given program using lparse, the grounding system of

Smodels.

2. Do some simple simplifications to the instantiated program, such as

deleting all rules p

← G such that p ∈ G.

3. Compute the completion of the resulting program and convert it to

clauses.


2

4. Repeat

(a) Find a model M of the clauses using X.

(b) If no such M exists, then exit with failure.

(c) Compute M

= M



− Cons(P

M

).



2

When converting a program’s completion and loop formulas to clauses,

O(r) number

of extra variables may have to be used in order to avoid combinatorial explosion, where

r

is the number of rules. So far, we do not find this to be a problem. For instance, for graph



coloring and HC problems, no extra variables are needed. Notice that the approach in [3]

also needs a program’s completion as the base case.

16


(d) If M

=



∅, then return with M for in this case it is an answer set.

(e) Compute all maximal loops under M .

(f) For each of these loops, compute its loop formula, convert it to

clauses, and add them to the clausal set.

Notice that in the procedure above, when M is not an answer set, we will add

the loop formula of every maximal loop under M to the current clausal set,

instead of adding just the loop formula of one of the terminating loops if we

want to follow Procedure 1 strictly using Theorem 2. The procedure above

has the advantage of not having to check whether a loop is terminating. This

is a feasible strategy as we have found from our experiments that there are

usually not many such maximal loops.

6

Some experimental results



We experimented on a variety of benchmark domains. We report some of

our results here for the following three domains: graph coloring, the blocks

world planning, and Hamiltonian Circuit (HC) domains. More experimental

data can be found on our web site http://www.cs.ust.hk/assat.

For these three domains, we used Niemel¨

a’s [18] logic program encodings

that can be downloaded from Smodels’ web site

3

. Among the three domains,



only HC requires adding loop formulas to program completions. The graph

coloring programs are always loop-free, and while the logic programs for the

blocks world planning problems have loops, Babovich et al. [2] showed that

all models of the programs’ completions are answer sets. For graph coloring

and the blocks world planning, our results confirmed the findings of [8], but

we did it with many more and much larger instances.

For our system, ASSAT 2.0,we tried the following SAT solvers: Chaff2

(Mar 23, 2001 version) [17], Walksat 41 [19], GRASP (Feb, 2000 version)

[20], Satz 215.2 [13], and SATO 4.1 (Zhang) [25]. In our experiments, we

compare the performance of our system with Smodels version 2.27 [21] and

DLV (May 16, 2003 version) [12] on the problem of computing one answer set

of a normal logic program. More precisely, given a logic program, we measure

the performance of each system by how fast it returns the first answer set of

the program or reports that the program has no answer set.

3

http://www.tcs.hut.fi/Software/smodels/.



17

For Smodels and ASSAT, we used lparse 1.0.13, the grounding module

of Smodels, to ground a logic program (DLV has its own built-in grounding

routine). We have noticed that for both Smodels and ASSAT, their behaviors

are sometimes influenced by the parameters that one calls lparse with. For

our experiments, we use “lparse -d none” which seemed to optimize the

performance of both Smodels and ASSAT.

Our experiments were done on Sun Ultra 5 machines with 256M memory

running Solaris. The reported times are in CPU seconds as reported by Unix



Do'stlaringiz bilan baham:
1   2   3   4


Ma'lumotlar bazasi mualliflik huquqi bilan himoyalangan ©fayllar.org 2017
ma'muriyatiga murojaat qiling