Solution to the Open Problem: AnsProlog encoding of win and lose (Chs 2,4)

The goal here is to develop an AnsProlog program that has the same characterization of winning and losing as the following logic program with respect to the well-founded semantics.

win(X) ← move(X, Y), not win(Y). an arbitrary set of ‘move’ facts.

We will now give another characterization of this which does not appeal to the well-founded semantics.

1. We have a set of nodes.

2. We are given a set of facts about a binary predicate move. Intuitively, move(a, b) means that there is an available move from node a to node b.

3. A strategy S is a function from nodes to nodes such that S(X) = Y only if move(X,Y) is true.

4. Given two strategies S_{1} and S_{2}, and a node a we define the trajectory followed by alternatively applying S_{1} and S_{2} as: traj(a, S_{1}, S_{2}) = X_{0}^{a,S_{1},S_{2}}X_{1}^{a,S_{1},S_{2}} …, where

X_{0}^{a,S_{1},S_{2}} = a X_{k+1}^{a,S_{1},S_{2}} = S_{1}(X_{k}^{a,S_{1},S_{2}}) if k is even

= S_{2}(X_{k}^{a,S_{1},S_{2}}) if k is odd

5. The length of a trajectory X_{0}X_{1} … X_{k} is k.

6. A node a is said to be a winning node if there exists S_{1} such that for all S_{2} the sequence traj(a, S_{1}, S_{2}) terminates and its length is odd.

7. A node a is said to be a losing node if for all S_{1} there exists S_{2} such that the sequence traj(a, S_{1}, S_{2}) terminates and its length is even.

Question 1: Write an AnsProlog program Π whose answer set semantics corresponds to the win and lose above. (The solution to this is known.)

Question 2: Write an AnsProlog program Π which has a unique answer set corresponding to the win and lose above. (To the best of my knowledge, this is an open problem.)

Acknowledgement: Bertram Ludaescher first posed this question to me in July 2002. Later in August 2002 I discussed this with Vladimir Lifschitz and his group in Austin. The above formulation was developed during my presentation in Austin.

A solution to Question 2 has been given by Carlos Damasio (cd@di.fct.unl.pt) on 1/22/04. See the next page for the solution.

The Solution

The solution is based on simulating the well-founded semantics. Recall that answer sets (stable models) are defined as fixpoints of an operator F. The well-founded semantics is given as the pair ⟨lfp(F^{2}), HB \ gfp(F^{2})⟩, and lfp(F^{2}) can be computed iteratively by applying F^{2} repeatedly starting from ∅ until a fixpoint is reached. gfp(F^{2}) is obtained by applying F to lfp(F^{2}).

The Solution consists of the following:

1. Defining node:

node(X) ← move(X, Y). node(Y) ← move(X, Y).

2. Defining int:

int(0)…. int(max).

where max is an even number large enough that F^{2} reaches the least fixpoint by then.

3. Defining win aux: This predicate computes win at different iterations of F.

win aux(X, S + 1) ← int(S), move(X, Y), not win aux(Y, S).

4. Defining win, ¬win, and draw:

win(X) ← win aux(X, max).

¬win(X) ← node(X), not win aux(X, max − 1).

draw(X) ← node(X), not win(X), not ¬win(X).

Following is the solution in Smodels.

#maxint=20.
node(a;b;c;d;e;f;g)
move(a,b).
move(b,c).
move(b,d).
move(b,g).
move(c,c).
move(d,f).
move(f,d).
winaux( X, S ) :- #int(S), move(X,Y), #succ(S1,S), not winaux(Y,S1).
win(X)  :- winaux(X,#maxint).
-win(X)  :- node(X), #succ(S1,#maxint), not winaux(X, S1).
draw(X) :- node(X), not win(X), not -win(X).

It is fundamental that #maxint is an even number. When S is odd steps we compute F by predicate winaux( ,S) and in even steps F^{2}, and thats it. This technique can be used in general for computing the WFM by ASP. You can also include some rules for detecting the fixpoint of F^{2}, like the ones below. In this way you do not need anymore to enforce #maxint to be an even number.

CB, ASU  DRAFT  5

It just has to be big enough. I think that it is possible to change winaux/2 in order to stop after end. That is not difficult, after having end.

win(X)  :- end(S), winaux(X,S).
-win(X)  :- end(S), #succ(S1,S), node(X), not winaux(X, S1).
draw(X) :- node(X), not win(X), not -win(X).
end(S) :- #int(S1), S1 >= 1, S = 2 * S1, not change(S), not
ended_before(S).
ended_before (S) :- end(S1), #int(S), S1 < S .
change(S) :- winaux(X,S), #succ(S1,S), #succ(S2,S1), not
winaux(X,S2).