Missionaries and Cannibals: Discussion, Part 2
Date: Tue, 24 Aug 1999
From: Vladimir Lifschitz
To: Monica Nogueira and Mary Heidt
Thank you for your message which indeed answers all my questions. What
I found particularly interesting is the first line of your table: the
optimization of the control module reduces the computation time from
9 seconds to (practically) 0. The end of the table shows even more
dramatically how significant the role of the optimization is. We see
that Mary was right--the large difference between the computation times
for her formalization and mine is explained partially, but not completely,
by her use of an optimizing control module.
Another partial explanation probably comes from the fact that, in Mary's
formalization, cross(missionary,M) and cross(cannibal,N) are treated as
two actions executed in parallel; in mine, cross(M,N) is a single action.
"Action splitting" is known to be computationally advantageous.
(Incidentally, I am thinking now about action splitting as a representation
method that has conceptual advantages as well, because it makes the
formalization more elaboration tolerant. But this is a different
topic.)
I suspect that even these two factors together do not explain completely
the large difference between the computation times observed in Mary's
experiment and mine. We'll need to do more work on this.
Finally, a comment about your non-optimizing control module. It seems
to me (I didn't check this carefully) that it can be written more
concisely, more or less as follows:
noccurs(A,T):- action(A), time(T), not occurs(A,T), not goal(T).
occurs(A,T):- action(A), time(T), not noccurs(A,T), not goal(T).
:- agent(A1), agent(A2), num(N1), num(N2), time(T)
occurs(cross(A1,N1),T), occurs(return(A2,N2),T).
(plus a definition of action/1). Does this look plausible?
===========
Date: Sun, 29 Aug 1999
From: Mary Heidt
To: Vladimir Lifschitz
Using your suggestion we rewrote the control module as follows:
noccurs(A,T):- action(A), time(T), not occurs(A,T), not goal(T).
occurs(A,T):- action(A), time(T), not noccurs(A,T), not goal(T).
action(cross(A,N)):- agent(A), num(N), gt(N,0).
action(return(A,N)):- agent(A), num(N), gt(N,0).
I did not include the constraint that is in your suggestion. There are
already constraints that prevent these actions occuring in parallel, because
these actions can occur only if the boat is in the proper location. Also,
using this control module forced me to say that the actions cross and return
can only occur for N > 0. This is of course what I intended, but neglected
to include it in the original action definition.
===========
Date: Mon, 20 Sep 1999
From: Esra Erdem and Vladimir Lifschitz
To: Mary Heidt
We have studied your formalization and done some experiments with CCALC on
it. It was fun! We learned many things which also led to some improvements
in CCALC. The experiments described below were conducted using a new
version of CCALC (1.23) that will soon become publicly available.
We found that your solution to MCP differs from Vladimir's in three ways:
Vladimir uses a different formalization, a different control module, and a
different solver.
The comparison done by you and Monica shows to what degree the use of a
more sophisticated control module is responsible for the good computation
time of your solution.
Our goal was to investigate to what degree the use of another solver was
essential. To this end, we took your formalization with the simplest
control module and found its answer set using CCALC. The possibility of
doing this can be justified using the concept of a tight program. This
way of using CCALC is discussed at the end of Vladimir's new paper,
``Answer Set Planning'', available in the TAG bibliography.
Here is how we modified your program:
. We replaced
:- by <- and
the facts by the rules with the body ``true''.
. Since CCALC permits expressions like 0..15 in declarations, but not in
rules, we couldn't use your rules
time(0..15).
Instead, we declared time as a sort, and made 0..maxtime constants of
that sort. Here maxtime is a macro which expands to 15.
. We declared three more sorts: object, fluent and action.
. We declared
-- boat, missionary, cannibal as objects,
-- the instances of located(A,N), where A is an object and N is a
num, as fluents,
-- the instances of cross(A,N) and return(A,N), where A is
an object and N is a num, as actions,
-- the instances of goal(T), holds(F,T), ab(F,T), occurs(Act,T)
and noccurs(Act,T), where F is a fluent, Act is an action
and T is a time, as cwAtomicFormulas.
Here cwAtomicFormula is a subsort of atomicFormula declared in the
standard include file lp.b . That file (appended at the end of this
message) contains the rule
-_CWA <- not _CWA.
where _CWA is a variable of sort cwAtomicFormula.
. We dropped time(_) and num(_) appearing in the rules.
. We defined macros that correspond to the built-ins, gt/2, lt/2 and
eq/2, used in your formalization.
After that, we experimented with CCALC on this modified formalization:
| ?- sat.
calling sato...
run time (seconds) 0.16
Satisfying Interpretation: occurs(cross(cannibal,1),10)
occurs(cross(cannibal,2),0) occurs(cross(cannibal,2),2)
occurs(cross(cannibal,2),8) occurs(cross(missionary,1),10)
occurs(cross(missionary,2),4) occurs(cross(missionary,2),6)
occurs(return(cannibal,1),1) occurs(return(cannibal,1),3)
occurs(return(cannibal,1),5) occurs(return(cannibal,1),7)
occurs(return(missionary,1),5) occurs(return(missionary,1),9)
yes
Then we replaced the simplest control module by the more sophisticated
one. In this case we had to declare
mixed as an object constant
and
the instances of move(A,T), where A is an object and T is a time,
as cwAtomicFormulas.
We tried it with CCALC:
| ?- sat.
calling sato...
run time (seconds) 0.33
Satisfying Interpretation: occurs(cross(cannibal,1),0)
occurs(cross(cannibal,1),10) occurs(cross(cannibal,2),2)
occurs(cross(cannibal,2),8) occurs(cross(missionary,1),0)
occurs(cross(missionary,1),10) occurs(cross(missionary,2),4)
occurs(cross(missionary,2),6) occurs(return(cannibal,1),3)
occurs(return(cannibal,1),5) occurs(return(cannibal,1),7)
occurs(return(missionary,1),1) occurs(return(missionary,1),5)
occurs(return(missionary,1),9)
yes
We found that the more sophisticated control module does not improve the
computational efficiency with CCALC.
Then we wanted to compare the times SMODELS and CCALC need to find an
answer set.
We didn't find it very interesting to compare the grounding times since
the grounding processes of these two systems are so different:
-- CCALC is given sort information, SMODELS is not,
-- grounding in SMODELS is "intelligent", in SMODELS it is not,
-- SMODELS is written in C++, CCALC in Prolog.
(On our machine, lparse 0.99.28 spends 0.87 seconds, and CCALC 1.23 spends
4.87 seconds for grounding your program with the simplest control module.)
On our machine, SMODELS 2.23 spends 27.0 seconds (without grounding)
looking for an answer set, given your program with the simplest control
module. For CCALC 1.23, the time is 0.16 seconds. This is even better
than the computation time of SMODELS on your program with the optimizing
control module (1.0 seconds).
We attach the input file, which includes the simple control module, used
to experiment with CCALC below.
Regards,
Esra and Vladimir
---------------------------------------------------------------------------
% File: mary-mc.b
% Mary Heidt
% cannibals3
% Missionaries and Cannibals problem presented to smodels using
% the simplest control module.
% Three missionaries and three cannibals come to a river and find a boat that
% holds two. If the cannibals ever outnumber the missionaries on either bank,
% the missionaries will be eaten. How can they cross?
:- macros maxtime -> 15;
maxnum -> 3;
next(#1,#2) -> #1 >= 0, #1 < maxtime, (#2) is (#1) + 1;
gt(#1,#2) -> (#1) > (#2);
lt(#1,#2) -> (#1) < (#2);
eq(#1,#2) -> (#1) = (#2).
:- include 'lp.b'.
:- sorts object;
action;
fluent;
num;
time.
:- variables
X, X1 :: computed;
Act :: action;
F :: fluent;
A :: object;
N, N1 :: num;
T, T1 :: time.
:- constants
0..maxnum:: num;
0..maxtime:: time;
boat, missionary, cannibal :: object;
located(object,num) :: fluent;
cross(object,num), return(object,num) :: action;
agent(object),
vehicle(object),
holds(fluent,time),
ab(fluent,time),
occurs(action,time),
noccurs(action,time),
goal(time) :: cwAtomicFormula.
agent(cannibal) <- true.
agent(missionary) <- true.
vehicle(boat) <- true.
%-------------------------------------------------------------------------------
% DYNAMIC CAUSAL LAWS
%-------------------------------------------------------------------------------
%causes(cross(A,N),located(A,N1-N),[located(A,N1)])
holds(located(A,X),X1)<- X is N1-N, N1 >= N,
agent(A),
next(T,X1),
occurs(cross(A,N),T),
holds(located(A,N1),T).
ab(located(A,N1),T)<- agent(A), N1 >= N,
occurs(cross(A,N),T),
holds(located(A,N1),T).
holds(located(boat,0),X1)<- next(T,X1),
agent(A),
occurs(cross(A,N),T),
holds(located(boat,1),T).
ab(located(boat,1),T)<- agent(A),
occurs(cross(A,N),T),
holds(located(boat,1),T).
%causes(return(A,N),located(A,N1+N),[located(A,N1)])
holds(located(A,X),X1)<- X is N+N1, X =< maxnum,
agent(A),
next(T,X1),
occurs(return(A,N),T),
holds(located(A,N1),T).
ab(located(A,N1),T)<- X is N+N1, X =< maxnum,
agent(A),
occurs(return(A,N),T),
holds(located(A,N1),T).
holds(located(boat,1),X1)<- next(T,X1),
agent(A),
occurs(return(A,N),T),
holds(located(boat,0),T).
ab(located(boat,0),T)<- agent(A),
occurs(return(A,N),T),
holds(located(boat,0),T).
%-------------------------------------------------------------------------------
% INERTIA
%-------------------------------------------------------------------------------
holds(located(A,N),X1)<- agent(A),
next(T,X1),
holds(located(A,N),T),
not ab(located(A,N),T).
holds(located(boat,N),X1)<- next(T,X1),
holds(located(boat,N),T),
not ab(located(boat,N),T).
%-------------------------------------------------------------------------------
% CONSISTENCY
%-------------------------------------------------------------------------------
<- holds(located(boat,0),T),
holds(located(boat,1),T).
<- agent(A),
not eq(N,N1),
holds(located(A,N),T),
holds(located(A,N1),T).
%-------------------------------------------------------------------------------
% CONSTRAINTS
%-------------------------------------------------------------------------------
%it is impossible for more agents to cross than are on the first side
<- agent(A),
occurs(cross(A,N),T),
holds(located(A,N1),T),
gt(N,N1).
%it is impossible for more agents to return than are on the other side
<- agent(A),
occurs(return(A,N),T),
holds(located(A,N1),T),
X is N+N1,
gt(X,maxnum).
%cannibals cannot outnumber missionaries on either side
<- holds(located(cannibal,N),T),
holds(located(missionary,N1),T),
gt(N,N1),
gt(N1,0).
<- holds(located(cannibal,N),T),
holds(located(missionary,N1),T),
lt(N1,maxnum),
lt(N,N1).
%agents cannot move if they are not on the same side with the boat
<- agent(A),
holds(located(boat,0),T),
occurs(cross(A,N),T).
<- agent(A),
holds(located(boat,1),T),
occurs(return(A,N),T).
%no more than two agents can be in the boat
%this constraint is not in the cannibals program
<- occurs(cross(cannibal,N),T),
occurs(cross(missionary,N1),T),
X is N+N1,
gt(X,2).
<- occurs(return(cannibal,N),T),
occurs(return(missionary,N1),T),
X is N+N1,
gt(X,2).
<- occurs(cross(cannibal,N),T),
gt(N,2).
<- occurs(return(cannibal,N),T),
gt(N,2).
<- occurs(cross(missionary,N),T),
gt(N,2).
<- occurs(return(missionary,N),T),
gt(N,2).
%-------------------------------------------------------------------------------
% INITIAL CONDITIONS
%-------------------------------------------------------------------------------
holds(located(cannibal,3),0) <- true.
holds(located(missionary,3),0) <- true.
holds(located(boat,1),0) <- true.
%-------------------------------------------------------------------------------
% CONTROL MODULE
%-------------------------------------------------------------------------------
noccurs(cross(cannibal,N),T)<- not occurs(cross(cannibal,N),T),
gt(N,0),
not goal(T).
occurs(cross(cannibal,N),T)<- not noccurs(cross(cannibal,N),T),
gt(N,0),
not goal(T).
noccurs(return(cannibal,N),T)<- not occurs(return(cannibal,N),T),
gt(N,0),
not goal(T).
occurs(return(cannibal,N),T)<- not noccurs(return(cannibal,N),T),
gt(N,0),
not goal(T).
noccurs(cross(missionary,N),T)<- not occurs(cross(missionary,N),T),
gt(N,0),
not goal(T).
occurs(cross(missionary,N),T)<- not noccurs(cross(missionary,N),T),
gt(N,0),
not goal(T).
noccurs(return(missionary,N),T)<- not occurs(return(missionary,N),T),
gt(N,0),
not goal(T).
occurs(return(missionary,N),T)<- not noccurs(return(missionary,N),T),
gt(N,0),
not goal(T).
%-------------------------------------------------------------------------------
% GOAL
%-------------------------------------------------------------------------------
goal(T)<- holds(located(missionary,0),T),
holds(located(cannibal,0),T).
<- not goal(12).
-------------------------------------------------------------------------------
% File: lp.b
:- op(600,fx,not).
:- macros
not (#1) -> -(#1).
:- sorts
atomicFormula >> cwAtomicFormula.
:- variables
_CWA :: cwAtomicFormula.
-_CWA <- not _CWA.
=============
Date: Tue, 21 Sep 1999
From: Vladimir Lifschitz
To: TAG
I'd like to add something to what Esra and I wrote in our previous message.
One of our goals is to develop "answer set programming"--a new programming
methodology in which solutions to a problem are represented by answer sets,
and systems for computing answer sets (such as dlv and smodels) are used as
computational tools. In many cases, the problem of finding an answer set
for a logic program can be reduced to the problem of finding a satisfying
interpretation for a set of propositional formulas. In such cases, answer
set programming does not require a system for computing answer sets;
propositional solvers, such as sato, can be used instead of dlv and smodels.
Our message about Mary's solution to the missionaries and cannibals problem
showed how it can be done in that particular case. We showed how the use
of ccalc allows us to replace smodels as a search engine by sato.
The following chart summarizes the computation times that we observed, as
quoted in the previous message:
| SEARCH TIME, IN SECONDS
----------------------------------------------------
| smodels | sato
Mary's program | |
with the simple | 27.0 | 0.16
control module | |
| |
Mary's program | |
with the optimizing | 1.0 | 0.33
control module | |
| |
This is certainly not enough information for a meaningful generalization.
But we'll be conducting more comparisons of this kind, and they will help
us answer an important question: in the cases when propositional solvers
can be used instead of answer set solvers, is it computationally
advantageous to do that?
Our answers to this question will need to be constantly re-evaluated,
because of the rapid progress in the development of solvers of both
kinds.
=============
Date: Fri, 24 Sep 1999
From: Michael Gelfond
To: Esra Erdem and Vladimir Lifschitz
We are very glad to learn about your experiments.
(We are also glad you had fun with them.)
It would be interesting to know what you needed
to modify in CCALC.
Here is an attempt on very preliminary explanation of why
planning (control) module which speeds up SMODELS
slows CCALC (or rather SATO) down.
We only started to study both so do not take it too seriously.
The efficiency of both solvers depends substantially
on the number of guesses they should make in the process
of computation. SMODELS makes guesses about the
values of literals which occur in the program under NOT.
(Of course we do not need to make guesses about all such literals
but still it gives us an upper bound).
SATO (potentially) needs to make guesses about arbitrary
variables and therefore an increase in the number of variables
makes its work more difficult. Our planning module substantially
cuts the number of literals under NOT but does it at the cost of
introducing new relations and therefore increasing the number of
variables in the SATO's input. Does it make sense?
==============
Date: Mon, 27 Sep 1999
From: Esra Erdem and Vladimir Lifschitz
To: Michael Gelfond
> It would be interesting to know what you needed
> to modify in CCALC.
The only modification of ccalc we did in connection with this example is
related to the form of the output.
> Here is an attempt on very preliminary explanation of why
> planning (control) module which speeds up SMODELS
> slows CCALC (or rather SATO) down.
> We only started to study both so do not take it too seriously.
>
> The efficiency of both solvers depends substantially
> on the number of guesses they should make in the process
> of computation. SMODELS makes guesses about the
> values of literals which occur in the program under NOT.
> (Of course we do not need to make guesses about all such literals
> but still it gives us an upper bound).
> SATO (potentially) needs to make guesses about arbitrary
> variables and therefore an increase in the number of variables
> makes its work more difficult. Our planning module substantially
> cuts the number of literals under NOT but does it at the cost of
> introducing new relations and therefore increasing the number of
> variables in the SATO's input. Does it make sense?
Yes, it makes sense. Thank you for your explanation.
==============
Date: Wed, 29 Sep 1999
From: Esra Erdem
To: TAG
The timings for our experiments with Mary's program that were reported
in our previous messages had an error. Here are the correct timings.
| SEARCH TIME, IN SECONDS
----------------------------------------------------
| smodels | sato
Mary's program | |
with the simple | 27.0 | 0.16
control module | |
| |
Mary's program | |
with the optimizing | 1.0 | 0.47
control module | |
| |
(Previously, the search time spent by sato for Mary's program with the
optimizing control module was reported as 0.33 seconds.) The new timings
do not lead to a qualitative change of our results though.