%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%
%%% March 2009
%%% %%% %%% %%% %%% %%% %%% %%% %%% %%% %%% %%% %%% %%% %%%
%%% Problem from no 89 of EATCS, page 183 (by Laurent Rosaz):
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%
%%% You are on the road.
%%% At km 0 is the unique gas station.
%%% You have N cars (and drivers) and you can fill the N cars at the gas station.
%%% No supplementary gas recipients are allowed.
%%% It is allowed at any time to decant gas from one car tank to another.
%%% A full tank allow a car to drive for a constant distance K.
%%% You have car number 1 and you can abandon the other cars on the road.
%%% How far can you go ?
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Let us assume that K is both
%%% - tank capacity, and
%%% - distance a car can walk with that fuel
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% To remove symmetries, we allow refill from
%%% higher to lower indexed cars only
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% K = 2,  N = 3, D = 4
%%% :-bmap(6). YES in 0.1s

%%% K = 4,  N = 3, D = 7
%%% :-bmap(9). YES in 5s

%%% K = 4,  N = 4, D = 8
%%% :-bmap(10). YES

k(4).    %%% = K
cars(4). %%% = N
dist(8). %%% = D

car(X) :-
   cars(N), interval(X,1,N).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

agent(X) :- cars(X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

fluent(tank(X),0,K) :-
     car(X),k(K).
fluent(distance(X),0,Max) :-
     car(X),k(K),cars(N),Max is N*K.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

action([X], move):-
   car(X).
action([X], refill(Y)) :-
   car(X),car(Y),X>Y.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

executable([X], move ,[tank(X) gt 0]) :-
       action([X], move).

executable([X],refill(Y),
        [distance(X)  eq distance(Y), tank(X)  gt 0, tank(Y) lt K]) :-
        action([X],refill(Y)),k(K).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

causes(tank(X) eq tank(X)^(-1) - 1, [actocc([X],move)]):-
        car(X).
causes(distance(X) eq distance(X)^(-1) + 1, [actocc([X],move)]) :-
        car(X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

causes( tank(X) eq 0,
       [actocc([X],refill(Y)), K - tank(Y) geq tank(X) ]):-
        action([X],refill(Y)),k(K).
causes( tank(Y) eq tank(Y)  + tank(X) ,
       [actocc([X],refill(Y)), K - tank(Y)  geq tank(X) ]):-
        action([X],refill(Y)),k(K).
causes( tank(Y) eq K,
       [actocc([X],refill(Y)), K - tank(Y)  lt tank(X) ]):-
        action([X],refill(Y)),k(K).
causes( tank(X) eq tank(X)^(-1) - K + tank(Y)^(-1),
       [actocc([X],refill(Y)), K - tank(Y)  lt tank(X) ]):-
        action([X],refill(Y)),k(K).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% INITIAL STATE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

initially(tank(X) eq K) :-
    k(K), car(X).
initially(distance(X) eq 0) :-
    car(X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% GOAL
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

goal(distance(1) geq D) :- dist(D).

%%% A little help:

holds(distance(C) eq A, A) :- car(C),
    k(K), A is K // 2.
holds(distance(C) eq A, B) :- car(C),
    k(K), A is K // 2,
    B is A+1.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%