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.