% prob_rushhour.pi (in Picat, by Neng-Fa Zhou, July 2014) % See a ProB model at http://www.stups.uni-duesseldorf.de/ProB/index.php5/User_Manual % The original version allowed vehicles to move both vertically and horizontally. % The current version only allows vehicals to move either forward or backward. % Thanks to Michael Leuschel for the discussions that led to this corrected version. % % Picat finds a best plan of 81 steps for the given instance in about 2 seconds. import ordset,planner. main => init_state(S), best_plan(S,Plan), foreach(Step in Plan) writeln(Step) end, writeln(Plan.length). init_state(S) => L11 = [(0,4),(1,4),(3,0),(3,1),(4,3),(5,0),(5,5)], % 1*1 spaces L12 = [(1,1),(2,1),(2,4),(3,3),(4,0)], % 1*2 cars L21 = [(0,5),(1,0),(3,5),(4,4)], % 2*1 cars L13 = [(0,0),(5,1)], % 1*3 cars L31 = [(0,3)], % 3*1 cars LocRed = (3,2), % read car S = \$s(LocRed,L11,L12,L21,L13,L31). final(s((4,2),_,_,_,_,_)) => true. % the red car is at the exit action(s(LocRed,L11,L12,L21,L13,L31),NewS,Action,Cost) ?=> Cost=1, move_hcar(2,1,LocRed,NLocRed,L11,NL11,Action), NewS = \$s(NLocRed,NL11,L12,L21,L13,L31). action(s(LocRed,L11,L12,L21,L13,L31),NewS,Action,Cost) ?=> Cost=1, select(Loc,L12,L12R), move_vcar(1,2,Loc,NLoc,L11,NL11,Action), NL12 = L12R.insert_ordered(NLoc), NewS = \$s(LocRed,NL11,NL12,L21,L13,L31). action(s(LocRed,L11,L12,L21,L13,L31),NewS,Action,Cost) ?=> Cost=1, select(Loc,L21,L21R), move_hcar(2,1,Loc,NLoc,L11,NL11,Action), NL21 = L21R.insert_ordered(NLoc), NewS = \$s(LocRed,NL11,L12,NL21,L13,L31). action(s(LocRed,L11,L12,L21,L13,L31),NewS,Action,Cost) ?=> Cost=1, select(Loc,L13,L13R), move_vcar(1,3,Loc,NLoc,L11,NL11,Action), NL13 = L13R.insert_ordered(NLoc), NewS = \$s(LocRed,NL11,L12,L21,NL13,L31). action(s(LocRed,L11,L12,L21,L13,L31),NewS,Action,Cost) => Cost=1, select(Loc,L31,L31R), move_hcar(3,1,Loc,NLoc,L11,NL11,Action), NL31 = L31R.insert_ordered(NLoc), NewS = \$s(LocRed,NL11,L12,L21,L13,NL31). % Move a car of size W*H from P to NP. After this move, Spaces becomes NSpaces move_vcar(W,H,P@(X,Y),NP,Spaces,NSpaces,Action),Y>0 ?=> % up Y1 = Y-1, L = [(X1,Y1) : X1 in X..X+W-1], subset(L,Spaces), Action = \$move(W*H,P,up), NP = (X,Y1), Y2 = Y1+H, L1 = [(X1,Y2) : X1 in X..X+W-1], NSpaces = union(subtract(Spaces,L),L1). move_vcar(W,H,P@(X,Y),NP,Spaces,NSpaces,Action),Y+H<=5 => % down Y1 = Y+H, L = [(X1,Y1) : X1 in X..X+W-1], subset(L,Spaces), Action = \$move(W*H,P,down), NP = (X,Y+1), L1 = [(X1,Y) : X1 in X..X+W-1], NSpaces = union(subtract(Spaces,L),L1). move_hcar(W,H,P@(X,Y),NP,Spaces,NSpaces,Action),X>0 ?=> % left X1 = X-1, L = [(X1,Y1) : Y1 in Y..Y+H-1], subset(L,Spaces), Action = \$move(W*H,P,left), NP = (X1,Y), X2 = X1+W, L1 = [(X2,Y1) : Y1 in Y..Y+H-1], NSpaces = union(subtract(Spaces,L),L1). move_hcar(W,H,P@(X,Y),NP,Spaces,NSpaces,Action),X+W<=5 => % right X1 = X+W, L = [(X1,Y1) : Y1 in Y..Y+H-1], subset(L,Spaces), Action = \$move(W*H,P,right), NP = (X+1,Y), L1 = [(X,Y1) : Y1 in Y..Y+H-1], NSpaces = union(subtract(Spaces,L),L1).