% fifteenPuzzle.pl for B-Prolog
% http://www.cs.kuleuven.be/~dtai/events/ASP-competition/Benchmarks/15P...
% by Neng-Fa Zhou, March 30, 2009

:-include(base).

solve(As):-
    (member(maxtime(Maxtime),As)->true;true),
    Maxtime1 is Maxtime+1,  % time(0),...,time(maxtime)
    length(States,Maxtime1),
    generate_states(States,Maxtime1),
    path(States),
    reverse(States,RStates),
    States=[state(InitBoard,_,_,_)|_],
    initial_state(As,InitBoard),
    RStates=[state(FinalBoard,_,_,_)|RStatesR],
    back_path(RStatesR),
    final_board(FinalBoard),
    label(States,0),!,
    output(States,0).
solve(_):-
    format("UNSATISFIABLE~n").

generate_states([],_).
generate_states([state(Board,I0,X0,Y0)|Ss],DistToFinal):-
    length(Cells,16),  % 16 cells
    Cells :: 0..15,    % each cell has an integer value from 0 to 15
    all_different(Cells),
    tile_indexes(Cells,0,[I0|Is]), % the indexes run from 1 to 16
    [X0,Y0] :: 1..4,
    X0-1 #= (I0-1)//4,
    Y0-1 #= (I0-1) mod 4,
    manhattan_dist(Is,1,2,Dist),
    Dist #=< DistToFinal,
    Board=..[board|Cells],
    DistToFinal1 is DistToFinal-1,
    generate_states(Ss,DistToFinal1).
    
tile_indexes(_,Tile,[]):-Tile>15,!.
tile_indexes(Cells,Tile,[Index|Indexes]):-
    element(Index,Cells,Tile),
    Tile1 is Tile+1,
    tile_indexes(Cells,Tile1,Indexes).

manhattan_dist([],_,_,0).
manhattan_dist([I|Is],X,Y,abs(Xi-X)+abs(Yi-Y)+Dist):-
    [Xi,Yi] :: 1..4,
    Xi-1 #= (I-1)//4,
    Yi-1 #= (I-1) mod 4,
    T is Y+1,
    (T==5->
     X1 is X+1, Y1=1;
     X1 is X, Y1=T),
    manhattan_dist(Is,X1,Y1,Dist).

label([],_).
label(States,T):-
    States=[state(_,I,_,_)|StatesR],
    indomain(I),
    T1 is T+1,
    label(StatesR,T1).

initial_state([],_):-!.
initial_state([in0(X,Y,N)|As],Board):-!,
    I is (X-1)*4+Y,
    arg(I,Board,N),
    initial_state(As,Board).
initial_state([_|As],Board):-
    initial_state(As,Board).

final_board(board(0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15)).

path([S1,S2|Ss]):-!,
    valid_move(S1,S2),
    path(S1,[S2|Ss],1),
    path([S2|Ss]).
path(_).

% S2 is the next state after S1. No more move if S1 is already final.
valid_move(state(S1,I1,X1,Y1),state(S2,I2,X2,Y2)):-
    sum_diff(S1,S2,Diff),
    final_board(F),
    sum_diff(S1,F,DiffF),
    edge_is_final(S1,F,[4,8,12,16],Col4IsFinal1),
    edge_is_final(S2,F,[4,8,12,16],Col4IsFinal2),
    Col4IsFinal1#=>Col4IsFinal2, % don't move this column if it is in final
    edge_is_final(S1,F,[13,14,15,16],Row4IsFinal1),
    edge_is_final(S2,F,[13,14,15,16],Row4IsFinal2),
    Row4IsFinal1#=>Row4IsFinal2, % don't move this row if it is in final
    sum(DiffF)#=0 #=> sum(Diff) #= 0,
    sum(DiffF)#\=0 #=> I1 #\= I2 #/\ abs(X1-X2)+abs(Y1-Y2)#=1.

edge_is_final(S,F,[I],(V1#=V2)):-!,
    arg(I,S,V1),arg(I,F,V2).
edge_is_final(S,F,[I|Is],(V1#=V2 #/\ IsFinal)):-
    arg(I,S,V1),arg(I,F,V2),
    edge_is_final(S,F,Is,IsFinal).

sum_diff(S1,S2,Diff):-
    sum_diff(S1,S2,16,Diff).

sum_diff(_S1,_S2,0,Diff):-!,Diff=[].
sum_diff(S1,S2,I,[B|Diff]):-
    arg(I,S1,V1),
    arg(I,S2,V2),
    V1#\=V2 #<=> B,
    I1 is I-1,
    sum_diff(S1,S2,I1,Diff).

%%
path(S1,[S2|Ss],K):-K=<6,!, % any cell can change after 7 or more moves
    constrain_unchanged_loop1(1,S1,S2,K),
    K1 is K+1,
    path(S1,Ss,K1).
path(_,_,_).

% S1 and S2 are K steps apart 
constrain_unchanged_loop1(I,_S1,_S2,_K):-I>16,!.
constrain_unchanged_loop1(I,S1,S2,K):-
    constrain_unchanged(I,S1,S2,K),
    constrain_unchanged_loop2(I,1,S1,S2,K),
    I1 is I+1,
    constrain_unchanged_loop1(I1,S1,S2,K).

% no tile can move >K distance away from a cell in K moves
constrain_unchanged_loop2(_I,J,_S1,_S2,_K):-J>16,!.
constrain_unchanged_loop2(I,J,S1,S2,K):-
    Xi is (I-1)//4+1, Yi is (I-1) mod 4+1,
    Xj is (J-1)//4+1, Yj is (J-1) mod 4+1,
    S1=state(Board1,_,_,_), S2=state(Board2,_,_,_),
    arg(I,Board1,V1),arg(J,Board2,V2),
    (abs(Xi-Xj)+abs(Yi-Yj)>K->V1#\=V2;true),
    J1 is J+1,
    constrain_unchanged_loop2(I,J1,S1,S2,K).
    
% every cell in T(k+i) that is K distance apart from 0 in T(i) remains unchanged 
constrain_unchanged(I,S1,S2,K):-
    X is (I-1)//4+1,
    Y is (I-1) mod 4+1,
    S1=state(Board1,_,X1,Y1), S2=state(Board2,_,X2,Y2),
    arg(I,Board1,V1), arg(I,Board2,V2),
    abs(X-X1)+abs(Y-Y1) #> K #=> V1#=V2 #/\ V1#\=0 #/\ V2#\=0,
    abs(X-X2)+abs(Y-Y2) #> K #=> V1#=V2 #/\ V1#\=0 #/\ V2#\=0.

% no two states are identical unless the later one is final
% prevent the 0 tile from moving back immediately
back_path([state(S,I2,_,_)|Ss]):-!,
    final_board(F),
    sum_diff(S,F,DiffF),
    sum_diff_neq_0(S,Ss,Conjs),
    (Ss=[_,state(_,I1,_,_)|_]->NoBack=(I1#\=I2);NoBack=1),
    sum(DiffF) #\= 0 #=> Conjs #/\ NoBack,
    back_path(Ss).
back_path(_).

sum_diff_neq_0(_S1,[],1).
sum_diff_neq_0(S1,[state(S2,_,_,_)|Ss],(sum(Diff)#\=0 #/\ Conjs)):-
    sum_diff(S1,S2,Diff),
    sum_diff_neq_0(S1,Ss,Conjs).

%%
output([state(S,_,_,_)|_],_):-final_board(S),!,nl.
output([_,State|Ss],T):-
    State=state(_,_,X,Y),
    format("move(~w,~w,~w). ",[T,X,Y]),
    T1 is T+1,
    output([State|Ss],T1).

%%%
test :-
    statistics(runtime,_),
    statistics(backtracks,B0), 
              solve([
                        maxtime(10),
                        in0(1,1,1), in0(1,2,2), in0(1,3,3), in0(1,4,7),
                        in0(2,1,4), in0(2,2,5), in0(2,3,6), in0(2,4,11),
                        in0(3,1,8), in0(3,2,9), in0(3,3,0), in0(3,4,10),
                        in0(4,1,12), in0(4,2,13), in0(4,3,14), in0(4,4,15)
                ]),
    statistics(runtime,[_,T]),
    statistics(backtracks,B1),
    B is B1-B0,
    format("~ncputime(~w) backtracks(~w)~n",[T,B]).
/*
test :- 
    statistics(runtime,_),
        solve([ 
                        maxtime(35), 
                        in0(1,1,4), in0(1,2,0), in0(1,3,3), in0(1,4,6), 
                        in0(2,1,12), in0(2,2,1), in0(2,3,11), in0(2,4,7), 
                        in0(3,1,9), in0(3,2,5), in0(3,3,10), in0(3,4,15), 
                        in0(4,1,13), in0(4,2,8), in0(4,3,14), in0(4,4,2)]),
    statistics(runtime,[_,T]),
    writeln(cputime(T)).
*/