J Moore's Problem

Date: Wed, 4 Apr 2001
From: Vladimir Lifschitz
To: TAG

At a recent faculty lunch here at UT Austin, Professor J Moore asked the
following question:

     Consider two processes, A and B, each of which is
     reading and writing a shared variable C. Each process is
     in an infinite loop, repeatedly executing: 

       C = C + C;

     By this we mean ``read the value of C, read the value of
     C again, add the two results and store the sum in C.''
     The two reads store the values in ``local registers'' of
     the process. Reads and writes are atomic but there is no
     synchronization between the two processes. The initial
     value of C is 1. 

     Problem: Given an arbitrary positive integer n is there an
     execution that assigns C the value n? 

The answer to this question turns out to be yes, and several proofs
have been posted at http://www.cs.utexas.edu/users/xli/prob/ (under
Problem 4).

Moore's question can be thought of as a planning problem.  Can you use
answer set programming to find solutions for specific values of n, say
n=7 and n=19 ?

=============

Date: Mon, 9 Apr 2001
From: Joohyung Lee
To: Vladimir Lifschitz

% moore.t

:- sorts
  number; process; cycle; register.

:- macros
  maxInt -> 20;
  sum(#1,#2,#3) ->
        #1 is max(1, min((#2)+(#3),maxInt));
  toWrite -> 0;
  toRead1 -> 1;
  toRead2 -> 2.

:- constants
  1..maxInt               :: number;
  toWrite..toRead2        :: cycle;
  a,b                     :: process;
  1,2                     :: register;
  even                    :: fluent;
  c                       :: inertialFluent(number);
  mem(process,register)   :: inertialFluent(number);
  cycle(process)          :: inertialFluent(cycle);
  read(process,register),
  write(process)          :: action.

:- variables
  X                       :: computed;
  I,J                     :: number;
  P,P1                    :: process;
  R                       :: register;
  A                       :: action.

% alternating even and -even
caused -even after even.
caused even after -even.

% prohibit writing in even steps
nonexecutable write(P) if even.
% prohibit reading in odd steps
nonexecutable read(P,R) if -even.

% change cycles in a process
% - single action
caused cycle(P) eq toRead2 after o(read(P,1)) && -o(read(P,2)).
read(P,2) causes cycle(P) eq toWrite.
write(P) causes cycle(P) eq toRead1.

% - concurrent actions: two read actions
caused cycle(P) eq toWrite after o(read(P,1)) && o(read(P,2)).


% read from the shared variable and write into a local register of a process
read(P,R) causes mem(P,R) eq I if c eq I.

% prohibit from reading into the second register before the first
caused false after -o(read(P,1)) && o(read(P,2)) && cycle(P) eq toRead1.

% read can be executed only at right cycles
nonexecutable read(P,1) if -(cycle(P) eq toRead1).
nonexecutable read(P,2) if cycle(P) eq toWrite.


% write the sum of values in two local registers into shared variable c
write(P) causes c eq X if mem(P,1) eq I && mem(P,2) eq J && sum(X,I,J).

% write can be executed only at the right cycle
nonexecutable write(P) if -(cycle(P) eq toWrite).

% prohibit concurrency while there is a write action
caused false after o(write(P)) && o(read(P1,R)).
caused false after o(write(P)) && o(write(P1)) && -(P=P1).


% domain control knowledge
never c eq maxInt.

% no waiting
caused false after (/\A: -o(A)).

:- plan
facts ::
 0: even,
 0: /\P: cycle(P) eq toRead1,
 0: c eq 1;
goals ::
 7..8: c eq 7.

:- plan
label :: 1;
facts ::
 0: even,
 0: /\P: cycle(P) eq toRead1,
 0: c eq 1;
goals ::
 11..12: c eq 19.


/*
| ?- loadf('moore.t').
% loading file /u/cise/appsmurf/ccalc.1.9-moore/C.t
% loading file /u/cise/appsmurf/ccalc.1.9-moore/moore.t
% 100 atoms, 947 rules, 1323 clauses (135 new atoms)
Grounding time: 410 msec
Completion time: 420 msec
yes
| ?- plan 0.

calling sato 3.1.2...
run time (seconds)                 0.19
  No plan of length 7,


calling sato 3.1.2...
run time (seconds)                 0.30

0:  even  c eq 1  cycle(a) eq 1  cycle(b) eq 1  mem(a,1) eq 8  mem(a,2) eq 1  mem(b,1) eq 8  mem(b,2) eq 8

ACTIONS:  read(a,1)  read(b,1)  read(b,2)

1:  c eq 1  cycle(a) eq 2  cycle(b) eq 0  mem(a,1) eq 1  mem(a,2) eq 1  mem(b,1) eq 1  mem(b,2) eq 1

ACTIONS:  write(b)

2:  even  c eq 2  cycle(a) eq 2  cycle(b) eq 1  mem(a,1) eq 1  mem(a,2) eq 1  mem(b,1) eq 1  mem(b,2) eq 1

ACTIONS:  read(a,2)  read(b,1)  read(b,2)

3:  c eq 2  cycle(a) eq 0  cycle(b) eq 0  mem(a,1) eq 1  mem(a,2) eq 2  mem(b,1) eq 2  mem(b,2) eq 2

ACTIONS:  write(a)

4:  even  c eq 3  cycle(a) eq 1  cycle(b) eq 0  mem(a,1) eq 1  mem(a,2) eq 2  mem(b,1) eq 2  mem(b,2) eq 2

ACTIONS:  read(a,1)

5:  c eq 3  cycle(a) eq 2  cycle(b) eq 0  mem(a,1) eq 3  mem(a,2) eq 2  mem(b,1) eq 2  mem(b,2) eq 2

ACTIONS:  write(b)

6:  even  c eq 4  cycle(a) eq 2  cycle(b) eq 1  mem(a,1) eq 3  mem(a,2) eq 2  mem(b,1) eq 2  mem(b,2) eq 2

ACTIONS:  read(a,2)  read(b,1)  read(b,2)

7:  c eq 4  cycle(a) eq 0  cycle(b) eq 0  mem(a,1) eq 3  mem(a,2) eq 4  mem(b,1) eq 4  mem(b,2) eq 4

ACTIONS:  write(a)

8:  even  c eq 7  cycle(a) eq 1  cycle(b) eq 0  mem(a,1) eq 3  mem(a,2) eq 4  mem(b,1) eq 4  mem(b,2) eq 4


yes



| ?- loadf('moore.t').
% loading file /u/cise/appsmurf/ccalc.1.9-moore/C.t
% loading file /u/cise/appsmurf/ccalc.1.9-moore/moore.t
% 220 atoms, 5087 rules, 7491 clauses (819 new atoms)
Grounding time: 2020 msec
Completion time: 2440 msec
yes
| ?- plan 1.

calling sato 3.1.2...
run time (seconds)                14.49
  No plan of length 11,


calling sato 3.1.2...
run time (seconds)                15.56

0:  even  c eq 1  cycle(a) eq 1  cycle(b) eq 1  mem(a,1) eq 20  mem(a,2) eq 20  mem(b,1) eq 20  mem(b,2) eq 12

ACTIONS:  read(a,1)  read(a,2)  read(b,1)

1:  c eq 1  cycle(a) eq 0  cycle(b) eq 2  mem(a,1) eq 1  mem(a,2) eq 1  mem(b,1) eq 1  mem(b,2) eq 12

ACTIONS:  write(a)

2:  even  c eq 2  cycle(a) eq 1  cycle(b) eq 2  mem(a,1) eq 1  mem(a,2) eq 1  mem(b,1) eq 1  mem(b,2) eq 12

ACTIONS:  read(a,1)  read(a,2)  read(b,2)

3:  c eq 2  cycle(a) eq 0  cycle(b) eq 0  mem(a,1) eq 2  mem(a,2) eq 2  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  write(a)

4:  even  c eq 4  cycle(a) eq 1  cycle(b) eq 0  mem(a,1) eq 2  mem(a,2) eq 2  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  read(a,1)  read(a,2)

5:  c eq 4  cycle(a) eq 0  cycle(b) eq 0  mem(a,1) eq 4  mem(a,2) eq 4  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  write(a)

6:  even  c eq 8  cycle(a) eq 1  cycle(b) eq 0  mem(a,1) eq 4  mem(a,2) eq 4  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  read(a,1)  read(a,2)

7:  c eq 8  cycle(a) eq 0  cycle(b) eq 0  mem(a,1) eq 8  mem(a,2) eq 8  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  write(a)

8:  even  c eq 16  cycle(a) eq 1  cycle(b) eq 0  mem(a,1) eq 8  mem(a,2) eq 8  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  read(a,1)

9:  c eq 16  cycle(a) eq 2  cycle(b) eq 0  mem(a,1) eq 16  mem(a,2) eq 8  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  write(b)

10:  even  c eq 3  cycle(a) eq 2  cycle(b) eq 1  mem(a,1) eq 16  mem(a,2) eq 8  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  read(a,2)

11:  c eq 3  cycle(a) eq 0  cycle(b) eq 1  mem(a,1) eq 16  mem(a,2) eq 3  mem(b,1) eq 1  mem(b,2) eq 2

ACTIONS:  write(a)

12:  even  c eq 19  cycle(a) eq 1  cycle(b) eq 1  mem(a,1) eq 16  mem(a,2) eq 3  mem(b,1) eq 1  mem(b,2) eq 2


yes
| ?-
*/

=============

Date: Tue, 10 Apr 2001
From: Pedro Cabalar
To: Vladimir Lifschitz

Thank you for posting this nice problem. I send you attached my solution
using PAL. I hope it is enough self-explaining.

Some remarks which perhaps can be interesting:

1) I've used a unique accumulator register Ri per each processor i. This
allows to reduce each program to the 3 instructions:
    0  Ri <- C
    1  Ri <- C + Ri
    2  C <- Ri

2) I've also introduced a control rule for efficiency purposes. When the
two processes consecutively read C, their ordering is not relevant. I've
ruled out sequences like:
read_process2 -> read_process1

3) I have used both the built-in PAL algorithm, based on WFS (reg.out),
and the translation I made for using smodels* as a back-end (reg2.out) 

* note: this translation is still slightly inefficient: PAL does the
whole grounding; besides, it does not use cardinality constraints yet.

4) Finally, to make the answers more readable, I've also written the
solutions in a text table (reg.txt).

Regards,
Pedro.

=====

options
  not concurrent,solutions=1;

constants
  k = 7;
  maxval = k;			# maximum value of a word
  n = 2; 			# number of processes
sets
  process = [1,n];
  word = [0,maxval];
    
fluents
  c : -> word;			# the memory position 'c'
  r : process -> word;		# acum. register (for each process)
  ip : process -> [0,2];	# instruction pointer (for each process)
    
actions
  fetch : process;
  
vars
  P : process;

rules
  # moving the instruction pointer
  ip(P):=(prev(ip(P))+1)%3 if fetch(P);

  # executing instructions 0, 1 and 2
  r(P):=c 		if ip(P)=0 and fetch(P);
  r(P):=prev(r(P))+c 	if ip(P)=1 and fetch(P);
     c:=r(P) 		if ip(P)=2 and fetch(P);

  # control rule: process 1 cannot read if process 2 has just read
  false if prev(fetch(2)) and prev(ip(2))!=2 and fetch(1) and ip(1)!=2;
initially
  c:=1,r(P):=0,ip(P):=2;
  
query
  ...{12} c=k?

=====

*** PAL 1.3 (Pertinence Action Language)
*** (c) 1999-2000 Pedro Cabalar, Apr 10 2001, AI Lab, Univ. of Corunna
*** http://www.dc.fi.udc.es/ai/~cabalar/pal/

Restart

Solution 1:
1)
fetch(1):=true
r(1):=1
ip(1):=0
2)
fetch(1):=true
r(1):=2
ip(1):=1
3)
fetch(2):=true
r(2):=1
ip(2):=0
4)
fetch(1):=true
c:=2
ip(1):=2
5)
fetch(1):=true
r(1):=2
ip(1):=0
6)
fetch(1):=true
r(1):=4
ip(1):=1
7)
fetch(2):=true
r(2):=3
ip(2):=1
8)
fetch(1):=true
c:=4
ip(1):=2
9)
fetch(1):=true
r(1):=4
ip(1):=0
10)
fetch(2):=true
c:=3
ip(2):=2
11)
fetch(1):=true
r(1):=7
ip(1):=1
12)
fetch(1):=true
c:=7
ip(1):=2

1 solution
2 actions, 5 fluents, 170 basic rules, 0.310 seconds.
*** PAL 1.3 (Pertinence Action Language)
*** (c) 1999-2000 Pedro Cabalar, Nov  7 2000, AI Lab, Univ. of Corunna
*** http://www.dc.fi.udc.es/ai/~cabalar/pal/

Restart

Solution 1:
1)
fetch(1):=true
r(1):=1
ip(1):=0
2)
fetch(1):=true
r(1):=2
ip(1):=1
3)
fetch(2):=true
r(2):=1
ip(2):=0
4)
fetch(1):=true
c:=2
ip(1):=2
5)
fetch(1):=true
r(1):=2
ip(1):=0
6)
fetch(1):=true
r(1):=4
ip(1):=1
7)
fetch(1):=true
c:=4
ip(1):=2
8)
fetch(1):=true
r(1):=4
ip(1):=0
9)
fetch(2):=true
r(2):=5
ip(2):=1
10)
fetch(2):=true
c:=5
ip(2):=2
11)
fetch(1):=true
r(1):=9
ip(1):=1
12)
fetch(2):=true
r(2):=5
ip(2):=0
13)
fetch(2):=true
r(2):=10
ip(2):=1
14)
fetch(1):=true
c:=9
ip(1):=2
15)
fetch(1):=true
r(1):=9
ip(1):=0
16)
fetch(2):=true
c:=10
ip(2):=2
17)
fetch(1):=true
r(1):=19
ip(1):=1
18)
fetch(1):=true
c:=19
ip(1):=2

1 solution
2 actions, 5 fluents, 890 basic rules, 40.320 seconds.

=====

*** PAL 1.3 (Pertinence Action Language)
*** (c) 1999-2000 Pedro Cabalar, Apr 10 2001, AI Lab, Univ. of Corunna
*** http://www.dc.fi.udc.es/ai/~cabalar/pal/

Restart

Solution 1:
1)
fetch(1):=true
r(1):=1
ip(1):=0
2)
fetch(2):=true
r(2):=1
ip(2):=0
3)
fetch(2):=true
r(2):=2
ip(2):=1
4)
fetch(2):=true
c:=2
ip(2):=2
5)
fetch(1):=true
r(1):=3
ip(1):=1
6)
fetch(2):=true
r(2):=2
ip(2):=0
7)
fetch(2):=true
r(2):=4
ip(2):=1
8)
fetch(2):=true
c:=4
ip(2):=2
9)
fetch(2):=true
r(2):=4
ip(2):=0
10)
fetch(1):=true
c:=3
ip(1):=2
11)
fetch(2):=true
r(2):=7
ip(2):=1
12)
fetch(2):=true
c:=7
ip(2):=2

1 solution
2 actions, 5 fluents, 170 basic rules, 2.850 seconds.
*** PAL 1.3 (Pertinence Action Language)
*** (c) 1999-2000 Pedro Cabalar, Apr 10 2001, AI Lab, Univ. of Corunna
*** http://www.dc.fi.udc.es/ai/~cabalar/pal/

Restart

Solution 1:
1)
fetch(1):=true
r(1):=1
ip(1):=0
2)
fetch(1):=true
r(1):=2
ip(1):=1
3)
fetch(2):=true
r(2):=1
ip(2):=0
4)
fetch(1):=true
c:=2
ip(1):=2
5)
fetch(1):=true
r(1):=2
ip(1):=0
6)
fetch(1):=true
r(1):=4
ip(1):=1
7)
fetch(2):=true
r(2):=3
ip(2):=1
8)
fetch(2):=true
c:=3
ip(2):=2
9)
fetch(2):=true
r(2):=3
ip(2):=0
10)
fetch(1):=true
c:=4
ip(1):=2
11)
fetch(1):=true
r(1):=4
ip(1):=0
12)
fetch(1):=true
r(1):=8
ip(1):=1
13)
fetch(1):=true
c:=8
ip(1):=2
14)
fetch(1):=true
r(1):=8
ip(1):=0
15)
fetch(1):=true
r(1):=16
ip(1):=1
16)
fetch(1):=true
c:=16
ip(1):=2
17)
fetch(2):=true
r(2):=19
ip(2):=1
18)
fetch(2):=true
c:=19
ip(2):=2

1 solution
2 actions, 5 fluents, 890 basic rules, 102.980 seconds.

=====

PAL wf (0.310 sec)
        1 2 3 4 5 6 7 8 9 0 1 2
ip(1) 2 0 1   2 0 1   2 0   1 2
r(1)  0 1 2     2 4     4   7  
c     1       2       4   3   7
r(2)  0     1       3          
ip(2) 2     0       1     2    

PAL smodels2.25 (2.850 sec)
        1 2 3 4 5 6 7 8 9 0 1 2
ip(1) 2 0       1         2    
r(1)  0 1       3              
c     1       2       4   3   7
r(2)  0   1 2     2 4   4   7  
ip(2) 2   0 1 2   0 1 2 0   1 2

PAL wf (40.320)
        1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8
ip(1) 2 0 1   2 0 1 2 0     1     2 0   1 2 
r(1)  0 1 2     2 4   4     9       9   19
c     1       2     4     5       9   10  19
r(2)  0     1           5     5 10  
ip(2) 2     0           1 2   0 1     2

PAL smodels2.25 (102.980)
        1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8
ip(1) 2 0 1   2 0 1       2 0 1 2 0 1 2
r(1)  0 1 2     2 4         4 8   8 16
c     1       2       3   4     8     16  19
r(2)  0     1       3   3               19
ip(2) 2     0       1 2 0               1 2

=============

Date: Tue, 10 Apr 2001
From: Paolo Ferraris
To: Vladimir Lifschitz

I wrote two programs in smodels.
In the first one the state is expressed by a single predicate. As
the transitions bring to an ordered graph, I had not used the concept of
time in this example.
In the second one we have three predicates that express the state, one
for the shared variable and one for each task. In this example time is
present.
In both programs I used a single local variable per task as Pedro did.

About execution times I had not reported them but the first progrem is
decisely faster. It calculates a plan for 19 in a few minutes on my PC.
With the second one I stopped calculating them for about number 10.

===

% to be executed with:  lparse -c num=5 | smodels  <concur1

const read1 = 0.
const read2 = 1.
const write = 2.
const num = 3. 

step(0..2).
value(0..num).

%	+------------- value of shared variable
%	| +----------- next execution step for task 1
%	| |  +-------- value of local variable of task 1
%	| |  |  +----- next execution step for task 2
%	| |  |  |  +-- value of local variable of task 2
%	v v  v  v  v
% state(C,S1,V1,S2,V2)

%     +--------------- number of process
%     |       +------- same fields of "state"
%     |       |
%     v /-----------\
% act(P,C,S1,V1,S2,V2)


%%%%%%%%%%%%%%%%%%%%%%%%%
% initial state condition
state(1,read1,0,read1,0).


%%%%%%%%%%%%%%%
% one task acts
1 {act(1,C,S1,V1,S2,V2),act(2,C,S1,V1,S2,V2)} 1 :- state(C,S1,V1,S2,V2),
		C !=num, value(C), step(S1), step(S2), value(V1), value(V2).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% effects of an action of task 1
state(C,read2,C,S2,V2) :- act(1,C,read1,V1,S2,V2),
			value(C), step(S2), value(V1), value(V2).
state(C,write,Z,S2,V2) :- act(1,C,read2,V1,S2,V2), Z=C+V1, value(Z),
			value(C), step(S2), value(V1), value(V2).
state(V1,read1,V1,S2,V2) :- act(1,C,write,V1,S2,V2),
			value(C), step(S2), value(V1), value(V2).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% effects of an action of task 2
state(C,S1,V1,read2,C) :- act(2,C,S1,V1,read1,V2),
			value(C), step(S1), value(V1), value(V2).
state(C,S1,V1,write,Z) :- act(2,C,S1,V1,read2,V2), Z=C+V2, value(Z),
			value(C), step(S1), value(V1), value(V2).
state(V2,S1,V1,read1,V2) :- act(2,C,S1,V1,write,V2),
			value(C), step(S1), value(V1), value(V2).

%%%%%%%%%%%%%%
% one solution
:- {state(num,S1,V1,S2,V2): step(S1): step(S2): value(V1): value(V2)} 0.

hide.
show state(C,S1,V1,S2,V2).

===

% to be executed with:  lparse -c num=5 | smodels <concur2

const read1 = 0.
const read2 = 1.
const write = 2.
const num = 3.
const maxtime = 6*num.

step(0..2).
value(0..num).
task(1..2).
time(0..maxtime).

%	 +------------- time step
%	 | +----------- value of shared variable
%	 v v
% shared(T,C)

%	+-------------- time step
%	| +------------ process number
%	| | +---------- next execution step for the task
%	| | | +-------- value of local variable of the task
%	v v v v
% local(T,P,S,V)

%     +---------------- time step
%     | +-------------- process running
%     v v
% act(T,P)



%%%%%%%%%%%%%%%
% initial state
shared(0,1).
local(0,P,0,0) :- task(P).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% only one acts and only if we have not found a solution
1 {act(T,P): task(P)} 1 :- time(T), shared(T,C), value(C), C!=num, T<maxtime.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% no action may cause a variable to assume value greater than num 
:- act(T,P), shared(T,C), local(T,P,1,V), C+V > num,
			value(C), time(T), task(P), value(V).


%%%%%%%%%%%%%%%%%%%%
% how shared changes
shared(T+1,V) :- act(T,P), local(T,P,2,V),
			time(T), task(P), value(V).
shared(T+1,C) :- act(T,P), local(T,P,S,V), shared(T,C), S!=2,
			value(C), step(S), time(T), task(P), value(V).


%%%%%%%%%%%%%%%%%%%
% how local changes
local(T+1,P,0,V) :- act(T,P), local(T,P,2,V),
			time(T), task(P), value(V).
local(T+1,P,1,C) :- act(T,P), local(T,P,0,V), shared(T,C),
			value(C), time(T), task(P), value(V).
local(T+1,P,2,Z) :- act(T,P), local(T,P,1,V), shared(T,C), Z = C+V,
			value(C), time(T), task(P), value(V), value(Z).
local(T+1,P,S,V) :- act(T,P2), local(T,P,S,V), P != P2,
			step(S), time(T), task(P), task(P2), value(V).


%%%%%%%%%%%%%%%%%%%%%%
% we want one solution
:- {shared(T,num): time(T)} 0.


hide.

show act(T,P).

=============

Date: Tue, 10 Apr 2001
From: Vladimir Lifschitz
To: Paolo Ferraris

> I wrote two programs in smodels and I am sending them in attachment.
> In the first one the state is expressed by a single predicate. As
> the transitions bring to an ordered graph, I had not used the concept of
> time in this example.

That's a great idea!  In Esra's paper on wire routing published in CL-2000,
joint with Martin Wong and myself, the question was formalized as a planning
problem.  Then Tommi Syrjanen, and later Deborah East and Mirek Truszczynski
(who gave a paper about this at the recent symposium on answer set
programming) expressed this question as a graph problem, and they didn't
use time.  This turned out to be computationally advantageous.  Now you did
the same with Moore's problem, and...

> About execution times I had not reported them but the first program is
> decisely faster.

...the result is similar!

> It calculates a plan for 19 in a few minutes on my PC.

I expect that this will be even faster if we use a sat solver to find an
answer set for your program.  I hope somebody will try that.