Please wait ...

Benchmark(s) have been added to cart.

Tag has been added.

• Login
• Links
• FAQs
• Contact

Navigation

• Instance
  • Show Instances
• Problem
  • Show Problems
• Show Tags
• Search
• Cart

Encoding hanoi.dlv.1

Name	hanoi.dlv.1
Class Tree	[Root]    Unclassified (114)    TowersOfHanoiCompetition (5)
Submitter	Martin Gebser
Author	n/a
Description
Created	2009-03-30 13:03
Modified	2009-03-12 21:35
Languages	dlv
Language Features
Compatible Instance Classes	TowersOfHanoiCompetition
Input Predicates	disk/1 on0/2 ongoal/2 steps/1 time/1
Output Predicates	put/3
Encoding Parameter
Standalone	No
Tags
Attributes
Content	#maxint=987654321. number_of_moves(X):- steps(X). largest_disc(X) :- #max{D:disk(D)}=X. trasd(N,1):- largest_disc(N). trasd(X,Y):- trasd(X1,Y1), #succ(X,X1), #succ(Y1,Y), X>3. disc(X) :- trasd(_,X). init_state1(0,1). init_state1(V,H) :- init_state1(V1,H1), on0(H1,H), trasd(H,D), AUX1=V1*10, V=AUX1+D. init_state2(0,2). init_state2(V,H) :- init_state2(V1,H1), on0(H1,H), trasd(H,D), AUX1=V1*10, V=AUX1+D. init_state3(0,3). init_state3(V,H) :- init_state3(V1,H1), on0(H1,H), trasd(H,D), AUX1=V1*10, V=AUX1+D. initial_state(V1,V2,V3) :- #max{V:init_state1(V,_)}=V1, #max{V:init_state2(V,_)}=V2, #max{V:init_state3(V,_)}=V3. goal_conf1(0,1). goal_conf1(V,H) :- goal_conf1(V1,H1), ongoal(H1,H), trasd(H,D), AUX1=V1*10, V=AUX1+D. goal_conf2(0,2). goal_conf2(V,H) :- goal_conf2(V1,H1), ongoal(H1,H), trasd(H,D), AUX1=V1*10, V=AUX1+D. goal_conf3(0,3). goal_conf3(V,H) :- goal_conf3(V1,H1), ongoal(H1,H), trasd(H,D), AUX1=V1*10, V=AUX1+D. goal(V1,V2,V3) :- #max{V:goal_conf1(V,_)}=V1, #max{V:goal_conf2(V,_)}=V2, #max{V:goal_conf3(V,_)}=V3. % from P1 to P2 put(S,D1,D2) :- move(S,V1,V2,V3), move(S1,W1,W2,W3),V1>W1,W2>V2, legalstack_top_rest(V1,T2,W1), legalstack_top_rest(V2,T1,_), trasd(D1,T1), trasd(D2,T2), V2!=0, S1=S+1. put(S,2,D2) :- move(S,V1,0,V3), move(S1,W1,W2,W3),V1>W1,W2>0, legalstack_top_rest(V1,T2,W1), trasd(D2,T2), S1=S+1. % from P1 to P3 put(S,D1,D2) :- move(S,V1,V2,V3), move(S1,W1,W2,W3),V1>W1,W3>V3, legalstack_top_rest(V1,T2,W1), legalstack_top_rest(V3,T1,_), trasd(D1,T1), trasd(D2,T2), V3!=0, S1=S+1. put(S,3,D2) :- move(S,V1,V2,0), move(S1,W1,W2,W3),V1>W1,W3>0, legalstack_top_rest(V1,T2,W1), trasd(D2,T2), S1=S+1. % from P2 to P1 put(S,D1,D2) :- move(S,V1,V2,V3), move(S1,W1,W2,W3),V2>W2,W1>V1, legalstack_top_rest(V2,T2,W2), legalstack_top_rest(V1,T1,_), trasd(D1,T1), trasd(D2,T2), V1!=0, S1=S+1. put(S,1,D2) :- move(S,0,V2,V3), move(S1,W1,W2,W3),V2>W2,W1>0, legalstack_top_rest(V2,T2,W2), trasd(D2,T2), S1=S+1. % from P2 to P3 put(S,D1,D2) :- move(S,V1,V2,V3), move(S1,W1,W2,W3),V2>W2,W3>V3, legalstack_top_rest(V2,T2,W2), legalstack_top_rest(V3,T1,_), trasd(D1,T1), trasd(D2,T2), V3!=0, S1=S+1. put(S,3,D2) :- move(S,V1,V2,0), move(S1,W1,W2,W3),V2>W2,W3>0, legalstack_top_rest(V2,T2,W2), trasd(D2,T2), S1=S+1. % from P3 to P1 put(S,D1,D2) :- move(S,V1,V2,V3), move(S1,W1,W2,W3),V3>W3,W1>V1, legalstack_top_rest(V3,T2,W3), legalstack_top_rest(V1,T1,_), trasd(D1,T1), trasd(D2,T2), V1!=0, S1=S+1. put(S,1,D2) :- move(S,0,V2,V3), move(S1,W1,W2,W3),V3>W3,W1>0, legalstack_top_rest(V3,T2,W3), trasd(D2,T2), S1=S+1. % from P3 to P2 put(S,D1,D2) :- move(S,V1,V2,V3), move(S1,W1,W2,W3),V3>W3,W2>V2, legalstack_top_rest(V3,T2,W3), legalstack_top_rest(V2,T1,_), trasd(D1,T1), trasd(D2,T2), V2!=0, S1=S+1. put(S,2,D2) :- move(S,V1,0,V3), move(S1,W1,W2,W3),V3>W3,W2>0, legalstack_top_rest(V3,T2,W3), trasd(D2,T2), S1=S+1. % Employ the notion of legal stacks, which carry information of the top % element and the rest of the stack in addition to the entire stack itself. % ------ legal non-empty stacks, their top element and the rest stack ------ legalstack_top_rest(D,D,0) :- disc(D). legalstack_top_rest(S,T,B) :- legalstack_top_rest(B,T1,R1), disc(T), T < T1, AUX = B * 10, S = AUX + T. % ------ possible moves ------ possible_state(0,S1,S2,S3) :- initial_state(S1,S2,S3). possible_state(I,S1,S2,S3) :- possible_move(I,_,_,_,S1,S2,S3). % From stack one to stack two. possible_move(I1,L1,L2,L3,S1,S2,L3) :- possible_state(I,L1,L2,L3), number_of_moves(J), I < J, #succ(I,I1), legalstack_top_rest(L1,X,S1), legalstack_top_rest(S2,X,L2). % From stack one to stack three. possible_move(I1,L1,L2,L3,S1,L2,S3) :- possible_state(I,L1,L2,L3), number_of_moves(J), I < J, #succ(I,I1), legalstack_top_rest(L1,X,S1), legalstack_top_rest(S3,X,L3). % From stack two to stack one. possible_move(I1,L1,L2,L3,S1,S2,L3) :- possible_state(I,L1,L2,L3), number_of_moves(J), I < J, #succ(I,I1), legalstack_top_rest(L2,X,S2), legalstack_top_rest(S1,X,L1). % From stack two to stack three. possible_move(I1,L1,L2,L3,L1,S2,S3) :- possible_state(I,L1,L2,L3), number_of_moves(J), I < J, #succ(I,I1), legalstack_top_rest(L2,X,S2), legalstack_top_rest(S3,X,L3). % From stack three to stack one. possible_move(I1,L1,L2,L3,S1,L2,S3) :- possible_state(I,L1,L2,L3), number_of_moves(J), I < J, #succ(I,I1), legalstack_top_rest(L3,X,S3), legalstack_top_rest(S1,X,L1). % From stack three to stack two. possible_move(I1,L1,L2,L3,L1,S2,S3) :- possible_state(I,L1,L2,L3), number_of_moves(J), I < J, #succ(I,I1), legalstack_top_rest(L3,X,S3), legalstack_top_rest(S2,X,L2). %------ actual moves ------ % a solution exists if and only if there is a "possible_move" % leading to the goal. % in this case, starting from the goal, we proceed backward % to the initial state to single out the full set of moves. % Choose from the possible moves. move(I,A1,A2,A3) :- goal(A1,A2,A3), possible_state(I,A1,A2,A3). move(I,A1,A2,A3) v nomove(I,A1,A2,A3) :- move(J,S1,S2,S3), #succ(I,J), possible_move(J,A1,A2,A3,S1,S2,S3). %------ at most one move at each step ------ :- move(I,L1,L2,L3), move(I,M1,M2,M3), L1 < M1. :- move(I,L1,L2,L3), move(I,M1,M2,M3), L2 < M2. :- move(I,L1,L2,L3), move(I,M1,M2,M3), L3 < M3. %------ at least one move at each step ------ :- time(I), not moved(I). moved(I) :- move(I,_,_,_).