/* 

  Reindeer ordering in Picat.

  From https://dmcommunity.org/challenge/challenge-dec-2017/
  """
  Santa always leaves plans for his elves to determine the order in which the 
  reindeer will pull his sleigh. This year, for the European leg of his 
  journey, his elves are working to the following schedule, which will form a 
  single line of nine reindeer. 

  Here are the rules:

      Comet behind Rudolph, Prancer and Cupid
      Blitzen behind Cupid
      Blitzen in front of Donder, Vixen and Dancer
      Cupid in front of Comet, Blitzen and Vixen
      Donder behind Vixen, Dasher and Prancer
      Rudolph behind Prancer
      Rudolph in front of Donder, Dancer and Dasher
      Vixen in front of Dancer and Comet
      Dancer behind Donder, Rudolph and Blitzen
      Prancer in front of Cupid, Donder and Blitzen
      Dasher behind Prancer
      Dasher in front of Vixen, Dancer and Blitzen
      Donder behind Comet and Cupid
      Cupid in front of Rudolph and Dancer
      Vixen behind Rudolph, Prancer and Dasher.

  Create a decision model that determines the order of the reindeer and send 
  your solution to DecisionManagementCommunity@gmail.com.
  """

  Answer: prancer, cupid, rudolph, dasher, blitzen, vixen, comet, donder, dancer

  Notes:
  - All 15 constraints are not needed. In fact only 10 are needed in order
    to solve the problem without search (using the CP solver).
  - However, for the sat solver we need solve/1.


  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import cp.

main => go.

go ?=>
  S = [blitzen,comet,cupid,dancer,dasher,donder,prancer,rudolph,vixen],
  X = [Blitzen,Comet,Cupid,Dancer,Dasher,Donder,Prancer,Rudolph,Vixen],
  Len = X.len,
  X :: 1..Len,
  Order = new_list(Len),  Order :: 1..Len,

  all_different(X),
  all_different(Order),
  assignment(X,Order),

  % Note: We don't need to use all 15 constraint; 9 of them is enough!

  % behind(Comet,[Rudolph,Prancer, Cupid]), % not needed
  % behind(Blitzen, [Cupid]), % not needed
  in_front_of(Blitzen,[Donder,Vixen,Dancer]),
  in_front_of(Cupid, [Comet, Blitzen,Vixen]),
  % behind(Donder,[Vixen, Dasher, Prancer]),
  % behind(Rudolph, [Prancer]), % not needed
  in_front_of(Rudolph, [Donder, Dancer, Dasher]),
  in_front_of(Vixen, [Dancer,Comet]),
  behind(Dancer, [Donder, Rudolph,Blitzen]),
  in_front_of(Prancer, [Cupid, Donder, Blitzen]),
  % behind(Dasher,[Prancer]), % not needed
  in_front_of(Dasher, [Vixen, Dancer, Blitzen]),
  behind(Donder, [Comet,Cupid]),
  in_front_of(Cupid,[Rudolph,Dancer]),
  % behind(Vixen, [Rudolph, Prancer, Dasher]), % not needed


  println(xBefore=X),
  println(orderBefore=Order),

  solve(X ++ Order), % not needed for cp solver

  println(order=[S[Order[I]] : I in 1..Len]),
  nl,
  fail,
  
  nl.


go => true.

%
% Show the progress of the propagations, and use all constraints.
%
go1 ?=>
  S = [blitzen,comet,cupid,dancer,dasher,donder,prancer,rudolph,vixen],
  X = [Blitzen,Comet,Cupid,Dancer,Dasher,Donder,Prancer,Rudolph,Vixen],
  Len = X.len,
  X :: 1..Len,
  Order = new_list(Len),  Order :: 1..Len,

  all_different(X),
  all_different(Order),
  assignment(X,Order),

  behind(Comet,[Rudolph,Prancer, Cupid]), 
  
  behind(Blitzen, [Cupid]),
  println(x=X),
  println(order=Order),
  in_front_of(Blitzen,[Donder,Vixen,Dancer]),
  println(x=X),
  println(order=Order),

  in_front_of(Cupid, [Comet, Blitzen,Vixen]),
  println(x=X),
  println(order=Order),

  behind(Donder,[Vixen, Dasher, Prancer]),
  println(x=X),
  println(order=Order),

  behind(Rudolph, [Prancer]),
  println(x=X),
  println(order=Order),

  in_front_of(Rudolph, [Donder, Dancer, Dasher]),
  println(x=X),
  println(order=Order),

  in_front_of(Vixen, [Dancer,Comet]),
  println(x=X),
  println(order=Order),

  behind(Dancer, [Donder, Rudolph,Blitzen]),
  println(x=X),
  println(order=Order),

  in_front_of(Prancer, [Cupid, Donder, Blitzen]),
  println(x=X),
  println(order=Order),

  behind(Dasher,[Prancer]),
  println(x=X),
  println(order=Order),

  in_front_of(Dasher, [Vixen, Dancer, Blitzen]),
  println(x=X),
  println(order=Order),

  behind(Donder, [Comet,Cupid]),
  println(x=X),
  println(order=Order),

  in_front_of(Cupid,[Rudolph,Dancer]),
  println(x=X),
  println(order=Order),

  behind(Vixen, [Rudolph, Prancer, Dasher]),
  println(x=X),
  println(order=Order),


  println(xBefore=X),
  println(orderBefore=Order),

  solve(X ++ Order), % not needed for cp solver

  println(order=[S[Order[I]] : I in 1..Len]),
  nl,
  fail,
  
  nl.


go1 => true.




% Plain LP approach: 52.5s
% Note that we use all_different/1 and assignment/2 from the CP module but there's 
% neither domains nor search.
go2 => 
  X = [Blitzen,Comet,Cupid,Dancer,Dasher,Donder,Prancer,Rudolph,Vixen],
  Len = X.len,

  % slightly faster than between/3
  member(Blitzen,1..Len),
  member(Comet,1..Len),
  member(Comet,1..Len),
  member(Cupid,1..Len),
  member(Dancer,1..Len),
  member(Dasher,1..Len),
  member(Donder,1..Len),
  member(Prancer,1..Len),
  member(Rudolph,1..Len),
  member(Vixen,1..Len),

  /*
  between(1,Len,Blitzen),
  between(1,Len,Comet),
  between(1,Len,Comet),
  between(1,Len,Cupid),
  between(1,Len,Dancer),
  between(1,Len,Dasher),
  between(1,Len,Donder),
  between(1,Len,Prancer),
  between(1,Len,Rudolph),
  between(1,Len,Vixen),
  */

  all_different(X),

  behind(Comet,[Rudolph,Prancer, Cupid]),
  behind(Blitzen, [Cupid]),
  in_front_of(Blitzen,[Donder,Vixen,Dancer]),
  in_front_of(Cupid, [Comet, Blitzen,Vixen]),
  behind(Donder,[Vixen, Dasher, Prancer]),
  behind(Rudolph, [Prancer]),
  in_front_of(Rudolph, [Donder, Dancer, Dasher]),
  in_front_of(Vixen, [Dancer,Comet]),
  behind(Dancer, [Donder, Rudolph,Blitzen]),
  in_front_of(Prancer, [Cupid, Donder, Blitzen]),
  behind(Dasher,[Prancer]),
  in_front_of(Dasher, [Vixen, Dancer, Blitzen]),
  behind(Donder, [Comet,Cupid]),
  in_front_of(Cupid,[Rudolph,Dancer]),
  behind(Vixen, [Rudolph, Prancer, Dasher]),

  assignment(X,Order),
  println(x=X),
  println(order=Order),
  nl,
  % fail,

  nl.

go2 => true.


%
% Plain programming, with reasoning about the relations: 0s
%
go3 => 
  X = [Blitzen,Comet,Cupid,Dancer,Dasher,Donder,Prancer,Rudolph,Vixen],
  Len = X.len,
  X = 1..Len,

  Map = new_map(),
  All = new_map(),

  behind(Comet,[Rudolph,Prancer, Cupid],1,Map,All),
  behind(Blitzen, [Cupid],2,Map,All),
  in_front_of(Blitzen,[Donder,Vixen,Dancer],3,Map,All),
  in_front_of(Cupid, [Comet, Blitzen,Vixen],4,Map,All),
  behind(Donder,[Vixen, Dasher, Prancer],5,Map,All),
  behind(Rudolph, [Prancer],6,Map,All),
  in_front_of(Rudolph, [Donder, Dancer, Dasher],7,Map,All),
  in_front_of(Vixen, [Dancer,Comet],8,Map,All),
  behind(Dancer, [Donder, Rudolph,Blitzen],9,Map,All),
  in_front_of(Prancer, [Cupid, Donder, Blitzen],10,Map,All),
  behind(Dasher,[Prancer],11,Map,All),
  in_front_of(Dasher, [Vixen, Dancer, Blitzen],12,Map,All),
  behind(Donder, [Comet,Cupid],13,Map,All),
  in_front_of(Cupid,[Rudolph,Dancer],14,Map,All),
  behind(Vixen, [Rudolph, Prancer, Dasher],15,Map,All),

  % AllCs = All.get(all),
  % foreach({I,A} in zip(1..AllCs.len,AllCs))
  %   println(I=A)
  % end,
  % println(allLen=All.get(all).len),

  % foreach(K in Map.keys().sort())
  %   println(K=Map.get(K))
  % end,
  % println(reduced_to=Map.keys().len),

  % Counting the number that are after each value _almost_ give the order:
  %   [7 = 1,3 = 2,8 = 3,5 = 4,1 = 5,9 = 5,2 = 7,6 = 7,4 = 8]
  % i.e. the only duplicates is that 2 and 6 share the 7'th place.
  % The order is the same as the solution but it's because 2 happend to be numerically < 6.
  NumAfter = new_map(),
  foreach(I in 1..Len) 
    C = Len - sum([1 : $(K < _) in Map.keys(), K = I]) - 1,
    NumAfter.put(I,C) % ,
    % println(I=C)
  end,
  % println(numAfter=NumAfter.sort_map(values)),
  % println('numAfter     '=[K : V=K in [V=K : K=V in NumAfter].sort()]),

  % OK, so we have to dig further and do some inferences about the relations:
  %    If we already got that I < J and also that J < A then we got I < A
  % Then these relations are added:
  % (1 < 2)
  % (2 < 4)
  % (3 < 5)
  % (5 < 2)
  % (7 < 4)
  % (8 < 1)
  % 
  Map2 = new_map(),
  foreach(K=V in Map) Map2.put(K,1) end, % copy from above
  foreach(I in 1..Len, J in 1..Len, I != J)
    if Map.has_key($(I < J)) then
       C = $(I < J),
       foreach(A in 1..Len, A != I, A!= J) 
         D1 = $(J < A), % If we have this 
         D2 = $(I < A), % then assert this (if we don't have it already)
         if Map2.has_key(D1), not Map2.has_key(D2) then
            % println(we_also_got=D2=Map2.get(D2,0)),
            Map2.put(D2,Map2.get(D2,0)+1)
         end
       end
    end
  end,
  % println(map2=Map2.keys().len),
  % println("Map2"),  
  % foreach(K in Map2.keys().sort())
  %   println(K=Map2.get(K))
  % end,
  % println(map2_len=Map2.keys().len),

  % And now we check the adjusted Map2
  NumAfter2 = new_map(),
  % Where we get the complete solution:
  %   [7 = 1,3 = 2,8 = 3,5 = 4,1 = 5,9 = 6,2 = 7,6 = 8,4 = 9]
  foreach(I in 1..Len) 
    C = Len-sum([1 : $(T < _V) in Map2.keys(), T=I]),
    NumAfter2.put(I,C)
    % , println(I=C)
  end,
  println(numAfter2=NumAfter2.sort_map(values)),
  println('order    '=[K : V=K in [V=K : K=V in NumAfter2].sort()]),
  nl,
  fail,

  nl.

go3 => true.


% Trying to see what constraints are redundant.
go4 ?=> 
  X = [Blitzen,Comet,Cupid,Dancer,Dasher,Donder,Prancer,Rudolph,Vixen],
  Len = X.len,
  X = 1..Len,

  Map = new_map(),
  All = new_map(),

  behind(Comet,[Rudolph,Prancer, Cupid],1,Map,All),
  behind(Blitzen, [Cupid],2,Map,All),
  in_front_of(Blitzen,[Donder,Vixen,Dancer],3,Map,All),
  in_front_of(Cupid, [Comet, Blitzen,Vixen],4,Map,All),
  behind(Donder,[Vixen, Dasher, Prancer],5,Map,All),
  behind(Rudolph, [Prancer],6,Map,All),
  in_front_of(Rudolph, [Donder, Dancer, Dasher],7,Map,All),
  in_front_of(Vixen, [Dancer,Comet],8,Map,All),
  behind(Dancer, [Donder, Rudolph,Blitzen],9,Map,All),
  in_front_of(Prancer, [Cupid, Donder, Blitzen],10,Map,All),
  behind(Dasher,[Prancer],11,Map,All),
  in_front_of(Dasher, [Vixen, Dancer, Blitzen],12,Map,All),
  behind(Donder, [Comet,Cupid],13,Map,All),
  in_front_of(Cupid,[Rudolph,Dancer],14,Map,All),
  behind(Vixen, [Rudolph, Prancer, Dasher],15,Map,All),

  AllCs = All.get(all),
  AllCsLen = AllCs.len,
  foreach({I,A} in zip(1..AllCs.len,AllCs))
     println(I=A)
  end,
  println(allLen=All.get(all).len),

  foreach(I in 1..Len, J in 1..Len, I != J)
    if Map.has_key($(I < J)) then
       C = $(I < J),
       foreach(A in 1..Len, A != I, A!= J) 
         D1 = $(J < A), % If we have this 
         D2 = $(I < A), % then assert this (if we don't have it already)
         if Map.has_key(D1), not Map.has_key(D2) then
            println(we_also_got=D2=Map.get(D2,0)),
            Map.put(D2,Map.get(D2,[])++[x=Map.get(C),Map.get(D1)])
         end
       end
    end
  end,

  foreach(K in Map.keys().sort())
    println(K=Map.get(K))
  end,

  foreach({I,As} in zip(1..AllCsLen, AllCs))
     % println(as=As),
     foreach(A in As) 
       foreach({J,Bs} in zip(1..AllCsLen,AllCs), I < J) 
         % printf("\t%w\n", Bs),
         foreach(B in Bs)
           % printf("\t\t%w\n", B),
           if A == B then
             println([B,from,J,bs=Bs,is_included_in,I,as=As])
           end
         end
       end
     end
  end,
  

  nl,
  fail,

  nl.

go4 => true.


%
% Testing how many constraints that are needed.
% Note: Here we see that we can skip 4 of constraints, but this model
% don't identify the exact constraints than can be skipped.
% It don't work to use 
%     if Active[I] #= 1 then call(C) end
% Note: This is very slow!
go5 => 
  S = [blitzen,comet,cupid,dancer,dasher,donder,prancer,rudolph,vixen],
  SS = ["Blitzen","Comet","Cupid","Dancer","Dasher","Donder","Prancer","Rudolph","Vixen"],
  X = [Blitzen,Comet,Cupid,Dancer,Dasher,Donder,Prancer,Rudolph,Vixen],
  Len = X.len,
  println(len=Len),
  X :: 1..Len,
  Order = new_list(Len),  Order :: 1..Len,
  all_different(X),
  all_different(Order),
  assignment(X,Order),

  Constraints = $[
    behind(Comet,[Rudolph,Prancer, Cupid]),
    behind(Blitzen, [Cupid]),
    in_front_of(Blitzen,[Donder,Vixen,Dancer]),
    in_front_of(Cupid, [Comet, Blitzen,Vixen]),
    behind(Donder,[Vixen, Dasher, Prancer]),
    behind(Rudolph, [Prancer]),
    in_front_of(Rudolph, [Donder, Dancer, Dasher]),
    in_front_of(Vixen, [Dancer,Comet]),
    behind(Dancer, [Donder, Rudolph,Blitzen]),
    in_front_of(Prancer, [Cupid, Donder, Blitzen]),
    behind(Dasher,[Prancer]),
    in_front_of(Dasher, [Vixen, Dancer, Blitzen]),
    behind(Donder, [Comet,Cupid]),
    in_front_of(Cupid,[Rudolph,Dancer]),
    behind(Vixen, [Rudolph, Prancer, Dasher])
  ],
  NumConstraints = Constraints.len,
  println(numConstraints=NumConstraints),

  Indices = new_list(NumConstraints),
  Indices :: 1..NumConstraints,
  all_distinct(Indices),
  
  %% This don't work...
  % Active constraints
  % Active = new_list(NumConstraints),
  % Active :: 0..1, 

  % check(X,Constraints,Indices,Active,NumAssigned,Degrees),
  check(X,Constraints,Indices,NumAssigned,Degrees),
  % Found by experiment that NumAssigned >= 5
  NumAssigned #= 6,

  % NumNotActive #= sum([A #= 0 : A in Active]),
  % NumNotActive #> 0,
  % NumNotActive #= NumConstraints - NumAssigned,

  println(numAssigned=NumAssigned),
  % println(numNotActive=NumNotActive),

  % solve($[max(NumAssigned),ff,split], Order ++ X ++ Indices),
  solve($[split], X ++ Order ++ Indices),

  println(order=[S[Order[I]] : I in 1..Len]),
  println(indices=Indices),
  % println(active=Active),
  println(degrees=Degrees),
  foreach(I in Indices) 
    C = Constraints[I],
    % printf("%% %w\n", C),
    if $behind(Deer,Deers) = C then
       printf("%w,\n", $behind(SS[Order[Deer]],[SS[Order[D]] : D in Deers])) 
    elseif $in_front_of(Deer,Deers) = C then
       printf("%w,\n",$in_front_of(SS[Order[Deer]],[SS[Order[D]] : D in Deers]))
    else 
       println("Bad constraint!"),
       halt
    end
  end,
  nl,
  fail,
  
  nl.

go5 => true.


sort_map(Map,values) = [K=V:_=(K=V) in sort([V=(K=V): K=V in Map])].
sort_map(Map,keys)   = sort([K=V:K=V in Map]).
sort_map(Map) = sort_map(Map,keys).


behind(X,List) => foreach(El in List) X #> El  end.
in_front_of(X,List) =>  foreach(El in List) X #< El  end.

behind(X,List,CIx,Map,All) => 
  Cs = [],                 
  foreach(El in List) 
     % C = $(X > El),
     C = $(El < X),
     Cs := Cs ++ [C],
     Map.put(C,Map.get(C,[])++[CIx])
  end,
  All.put(all,All.get(all,[])++[Cs]).

in_front_of(X,List,CIx,Map,All) =>  
   Cs = [],
   foreach(El in List) 
     C = $(X < El),
     % C = $(El > X),
     Cs := Cs ++ [C],
     Map.put(C,Map.get(C,[])++[CIx])
   end,
   All.put(all,All.get(all,[])++[Cs]).

sum_degrees(X) = sum([fd_degree(X[I]) : I in 1..X.len]).


% check(X,Constraints, Indices, Active, NumAssigned,Degrees1) =>
check(X,Constraints, Indices, NumAssigned,Degrees1) =>
  Degrees = [],
  CLen = Constraints.len,
  foreach(I in 1..CLen)
    element(I,Indices,Ix),
    nth(Ix,Constraints,C), % NOTE: Must use nth/3 here. Which makes it a non-pure CP problem!
    % element(Ix,Active,A),
    % (A #= 1 -> call(C), Degrees := Degrees ++ [sum_degrees(X)] ; true)
    call(C), Degrees := Degrees ++ [sum_degrees(X)]
  end,
  NumAssigned #= sum([D #= 0 : D in Degrees]),
  Degrees1 = Degrees.