/* 

  Peaceable Army of queens in Picat.

  Translation of the ESSENCE' model in the Minion Translator examples:
  http://www.cs.st-andrews.ac.uk/~andrea/examples/peacableArmyOfQueens/peaceableArmyOfQueens.eprime
  """
  Place 2 equally-sized armies of queens (white and black)
  on a chess board without attacking each other
  Maximise the size of the armies.

  'occurrence' representation 
  """

  Also see:
  "Peaceable Queens - Numberphile"
  (Neil Sloane discusses peaceable queens and chess)
  https://www.youtube.com/watch?v=IN1fPtY9jYg


  Compare with the MiniZinc model: http://hakank.org/minizinc/peaceableArmyOfQueens.mzn


  Max number of (white) queens for specific N

  N   # max queens    SAT     CP 
  -----------------------------------------------------------
  1   0               0.0s
  2   0               0.0s
  3   1               0.009
  4   2               0.135
  5   4               0.962
  6   5               0.448
  7   7               4.669
  8   9               7.635
  9  12              37.336
  10 14              98.488
  11 17             767.273
  12 21           14332.1
  13
  14
  15
  

  Cf: https://oeis.org/A250000
  "Peaceable coexisting armies of queens: the maximum number m such that m white queens and m 
   black queens can coexist on an n X n chessboard without attacking each other."
  N: 1  2  3  4  5  6  7  8   9  10  11  12  13  14  15
  m: 0  0  1  2  4  5  7  9  12  14  17  21  24  28  32 


  Some optimal solutions:

  N = 11
  amountOfQueens = 17 (767.3s)
  W W W _ _ _ _ _ W W _ 
  W W W W _ _ _ _ W W _ 
  _ W W W _ _ _ _ W _ _ 
  _ _ W W _ _ _ _ _ _ _ 
  _ _ _ _ _ _ _ B _ _ _ 
  _ _ _ _ _ _ _ _ _ _ B 
  _ _ _ _ _ _ _ _ _ _ B 
  _ _ _ _ B B _ _ _ _ B 
  _ _ _ _ B B B _ _ _ _ 
  _ _ _ _ B B B B _ _ _ 
  _ _ _ _ B B B B _ _ _ 


  N=12
  amountOfQueens = 21 (14332.1s)
  W _ _ _ _ W W W W _ _ _ 
  _ W _ _ _ W W W W _ _ _ 
  W _ _ _ _ _ W W W _ _ _ 
  W W _ _ _ _ _ W _ _ _ _ 
  W W _ _ _ _ _ _ _ _ _ _ 
  _ W _ _ _ W _ _ _ _ _ _ 
  _ _ _ _ _ _ _ _ _ B _ _ 
  _ _ _ _ _ _ _ _ _ B B _ 
  _ _ _ B _ _ _ _ _ B B B 
  _ _ B B B _ _ _ _ _ B B 
  _ _ B B B _ _ _ _ B _ B 
  _ _ B B B _ _ _ _ _ B _ 

N = 12 (vertical separation)

amountOfQueens = 21 (24.965s)

W _ W W W _ _ _ _ _ _ _ 
_ W _ W W W _ _ _ _ _ _ 
_ _ W _ W W _ _ _ _ _ _ 
_ _ _ _ _ _ _ _ B B B B 
_ _ _ _ _ _ _ _ _ B B B 
W W _ _ _ W _ _ _ _ _ _ 
W W W _ _ _ _ _ _ _ _ _ 
W W W W _ _ _ _ _ _ _ _ 
_ _ _ _ _ _ B B _ B _ _ 
_ _ _ _ _ _ B B B _ B _ 
_ _ _ _ _ _ _ B B B _ B 
_ _ _ _ _ _ _ _ B B B _ 




N = 13 (with the horizontal separation)

amountOfQueens = 24 (304.352s)
W _ _ _ _ _ _ W W W _ _ _ 
W W _ _ _ _ _ _ W W _ _ _ 
W W W _ _ _ _ W _ W _ _ _ 
W W W W _ _ _ _ W _ _ _ _ 
_ W W W _ _ _ _ _ W _ _ _ 
_ _ W W _ _ _ _ _ _ _ _ _ 
_ _ _ _ _ _ _ _ _ _ B _ B 
_ _ _ _ _ _ _ _ _ _ B B _ 
_ _ _ _ B _ _ _ _ _ B B B 
_ _ _ _ _ B _ _ _ _ B B B 
_ _ _ _ B B B _ _ _ _ B B 
_ _ _ _ B B B _ _ _ _ _ B 
_ _ _ _ B B B _ _ _ _ _ _ 


N = 13 (vertical separation)

amountOfQueens = 24 (90.083s)
W W _ W _ _ _ _ _ _ _ _ _ 
W W W _ W _ _ _ _ _ _ _ _ 
_ W W W _ W _ _ _ _ _ _ _ 
_ _ _ _ _ _ _ _ _ B B B B 
_ _ _ _ _ _ _ _ B B B B B 
_ _ _ _ _ _ _ B _ B B B B 
W W _ _ _ W _ _ _ _ _ _ _ 
W W W _ _ _ _ _ _ _ _ _ _ 
W W W W _ _ _ _ _ _ _ _ _ 
W W W _ _ _ _ _ _ _ _ _ _ 
_ _ _ _ _ _ B B B _ _ _ B 
_ _ _ _ _ _ _ B B B _ _ _ 
_ _ _ _ _ _ _ _ B B B _ _ 



N = 14 (horizontal separation)

amountOfQueens = 28 (735.773s)
W _ _ _ _ _ W W W W _ _ _ _ 
_ W _ _ _ _ W W W W _ _ _ _ 
W _ _ _ _ _ _ W W W _ _ _ _ 
W W _ _ _ _ _ _ W W _ _ _ _ 
W W W _ _ _ _ _ _ W _ _ _ _ 
W W W _ _ _ _ _ _ _ _ _ _ _ 
_ W W _ _ _ W _ _ _ _ _ _ _ 
_ _ _ _ _ _ _ _ _ _ B B _ _ 
_ _ _ _ _ _ _ _ _ _ B B B _ 
_ _ _ _ _ _ _ _ _ _ B B B B 
_ _ _ _ B _ _ _ _ _ _ B B B 
_ _ _ B B B _ _ _ _ B _ B B 
_ _ _ B B B _ _ _ _ _ B _ B 
_ _ _ B B B _ _ _ _ _ _ B _ 


N = 14 (vertical separation)

amountOfQueens = 28 (182.113s)
W W _ W _ W _ _ _ _ _ _ _ _ 
W W W _ W _ W _ _ _ _ _ _ _ 
_ W W W _ W _ _ _ _ _ _ _ _ 
_ _ _ _ _ _ _ _ _ B _ B B B 
_ _ _ _ _ _ _ _ B _ B B B B 
_ _ _ _ _ _ _ B _ B _ B B B 
_ _ _ _ _ _ _ _ B _ B _ B B 
W W W _ _ _ W _ _ _ _ _ _ _ 
W W W W _ _ _ _ _ _ _ _ _ _ 
W W W _ W _ _ _ _ _ _ _ _ _ 
W W _ W _ _ _ _ _ _ _ _ _ _ 
_ _ _ _ _ _ _ B B B _ _ _ B 
_ _ _ _ _ _ _ _ B B B _ _ _ 
_ _ _ _ _ _ _ _ _ B B B _ _ 


N = 15 (vertical separation)

amountOfQueens = 32 (5792.67s)
W W W W _ _ _ _ _ _ _ _ _ _ _ 
_ W W W W _ _ _ _ _ _ _ _ _ _ 
_ _ W W W W _ _ _ _ _ _ _ _ _ 
_ _ _ W W W W _ _ _ _ _ _ _ _ 
_ _ _ _ W W W _ _ _ _ _ _ _ _ 
_ _ _ _ _ _ _ _ _ _ _ B B B B 
_ _ _ _ _ _ _ _ _ _ B B B B B 
_ _ _ _ _ _ _ _ _ _ _ B B B B 
_ _ _ _ _ _ _ _ _ _ _ _ B B B 
_ _ _ _ _ _ _ B B _ _ _ _ B B 
W W W W _ _ _ _ _ _ _ _ _ _ _ 
W W W W W _ _ _ _ _ _ _ _ _ _ 
W W W W _ _ _ _ _ _ _ _ _ _ _ 
_ _ _ _ _ _ _ B B B B B B _ _ 
_ _ _ _ _ _ _ _ B B B B B B _ 



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

*/

import sat. % the best solver
% import cp.
% import mip. % seems to be better than cp
% import smt.

main => go.


go =>
  nolog,
  N = 9,
  println('N'=N),
  time2(queens(N, Board, AmountOfQueens)),
  println(amountOfQueens=AmountOfQueens),
  print_board(Board),
  println([n=N,queens=AmountOfQueens]),
  nl.


go2 =>
  nolog,
  Correct = new_map([3=1,4=2,5=4,6=5,7=7,8=9,9=12,10=14,11=17,12=21,13=24,14=28,15=32]),  
  Sols = [],
  foreach(N in 3..10)
    println('N'=N),
    time2(queens(N, Board, AmountOfQueens)),
    println(amountOfQueens=AmountOfQueens),
    print_board(Board),
    println([n=N,queens=AmountOfQueens]),
    nl,
    Sols := Sols ++ [AmountOfQueens],
    if AmountOfQueens != Correct.get(N) then
       printf("N=%d is not correct: was %d should be %d\n", N, AmountOfQueens, Correct.get(N)),
       halt
    end
  end,
  println("sols      "=Sols),

  println("should be="=Correct),
  if Sols != Correct then
    println("Something is wrong!")
  end,
  nl.


go3 =>
  nolog,
  Correct = new_map([3=1,4=2,5=4,6=5,7=7,8=9,9=12,10=14,11=17,12=21,13=24,14=28,15=32]),    
  foreach(N in 11..20)
    println('N'=N),
    time2(queens(N, Board, AmountOfQueens)),
    println(amountOfQueens=AmountOfQueens),
    print_board(Board),
    println([n=N,queens=AmountOfQueens]),        
    nl,
    if AmountOfQueens != Correct.get(N) then
      printf("N=%d is not correct: was %d should be %d\n", N, AmountOfQueens, Correct.get(N)),
      halt
    end

  end,
  nl.

%
% Show all optimal solutions.
%
go4 ?=>
  nolog,
  N = 5,
  time(queens(N, Board, AmountOfQueens, false)),
  println(amountOfQueens=AmountOfQueens),
  print_board(Board),

  All = find_all(Board2, queens(N, Board2, AmountOfQueens, false)),
  foreach(A in All)
    println("solution:"),
    print_board(A)
    
  end,
  println(num_solutions=All.len),
  nl,
  fail,
  nl.

go4 => true.

%
% Print the solution.
%
print_board(Board) =>
  foreach(Row in Board)
    foreach(R in Row)
      C = "_",
      if R == 1 then C := "W" end,
      if R == 2 then C := "B" end,      
      printf("%w ", C)
    end,
    nl
  end,
  nl.

%
% Solve the peacable army of queens problem.
%
queens(N, Board,AmountOfQueens) =>
  queens(N, Board,AmountOfQueens, true).
  
queens(N, Board,AmountOfQueens, Opt) =>
   Board = new_array(N,N),
   Board :: 0..2,
   AmountOfQueens :: 1..(N*N) div 2, 
   % println(amountOfQueens_domain=AmountfQueens),

   % let's place a white queen in the north-west corner
   % (symmetry breaking)
   % Hard code exception for N=5
   if N != 5 then
     Board[1,1] #= 1
   end,

   % Separating trick: Let's separate the white and black by a horizontal/vertical half line.
   % TODO: Test diagonal separation?
   if N != 11115 then 
     M = N div 2,
     K = cond(M mod 2 == 1, 2, 1),
     % println([m=M,K,'M-K'=(M-K),'M+K'=(M+K)]),
     Method = cols,
     % println(method=Method),
     % Tmp = new_array(N,N),
     % on rows
     if Method == rows then
       foreach(Row in 1..M-K, Col in 1..N)
         % printf("Row: %d Col: %d not 2\n", Row, Col),
         Board[Row,Col] #!= 2
         % Tmp[Row,Col] := 'not2'
       end,
       foreach(Row in N-K..N, Col in 1..N)
         % printf("Row: %d Col: %d not 1\n", Row, Col),    
         Board[Row,Col] #!= 1
         % Tmp[Row,Col] := 'not1'
       end
     elseif Method == cols then
       % on columns
       Rows = 1..N,
       Cols1 = 1..M,
       Cols2 = (N-K)..N,
       % println([rows=Rows, cols1=Cols1, cols2=Cols2]),
       foreach(Row in Rows, Col in Cols1)
         % printf("Row: %d Col: %d not 2\n", Row, Col),    
         Board[Row,Col] #!= 2
         % Tmp[Row,Col] := 'not2'
       end,

       foreach(Row in Rows, Col in Cols2)
         % printf("Row: %d Col: %d not 1\n", Row, Col),    
         Board[Row,Col] #!= 1
         % Tmp[Row,Col] := 'not1'
       end
    else
       % Diagonal
       % N=16 is wrong!
       foreach(Row in 1..N, Col in Row..N)
         % printf("Row: %d Col: %d not 2\n", Row, Col),    
         Board[Row,Col] #!= 2
         % Tmp[Row,Col] := 'not2'
       end,

       foreach(Row in 1..N, Col in 1..Row-1)
         % printf("Row: %d Col: %d not 1\n", Row, Col),    
         Board[Row,Col] #!= 1
         % Tmp[Row,Col] := 'not1'
       end
       
    end
    % foreach(R in Tmp)
    %   println(R)
    % end

  end,


   % TODO: Test mirrowing: if white in (row,col) <-> black in (col,row)
   % NOPE...
   % foreach(Row in 1..N, Col in Row+1..N)
   %   println([[Row,Col], [Col,Row]]),
   %   Board[Row,Col] #= 0 #<=> Board[Col,Row] #= 0,
   %   Board[Row,Col] #= 1 #<=> Board[Col,Row] #= 2
   % end,

   % we have the same amount of white as black queens
   sum([Board[Row,Col] #= 1 : Row in 1..N, Col in 1..N]) #= AmountOfQueens,
   sum([Board[Row,Col] #= 2 : Row in 1..N, Col in 1..N]) #= AmountOfQueens,

   % if we have a white queen at position row and column
   % there is no field on the same row/column/diagonal
   % that holds a black queen
   % 
   % if we have a black queen at position row and column
   % there is no field on the same row/column/diagonal
   % that holds a white queen
   %
   foreach(Row in 1..N, Col in 1..N)
      % check white (1) and black (2)
      foreach(Q in 1..2)
        Opposite = cond(Q==1,2,1), % the opposite color
        foreach(I in 1..N) 
          Board[Row, Col] #= Q #/\ I #!= Row #=> Board[I,Col] #!= Opposite,
          Board[Row, Col] #= Q #/\ I #!= Col #=> Board[Row,I] #!= Opposite,
          if Row+I <= N, Col+I <= N then Board[Row, Col] #= Q #=> Board[Row+I,Col+I] #!= Opposite end,
          if Row-I >  0, Col-I >  0 then Board[Row, Col] #= Q #=> Board[Row-I,Col-I] #!= Opposite end,
          if Row+I <= N, Col-I >  0 then Board[Row, Col] #= Q #=> Board[Row+I,Col-I] #!= Opposite end,
          if Row-I >  0, Col+I <= N then Board[Row, Col] #= Q #=> Board[Row-I,Col+I] #!= Opposite end
        end
     end
  end,
  if Opt == true ; var(AmountOfQueens) then
     solve($[max(AmountOfQueens),ff,updown,report(printf("z=%d\n", AmountOfQueens))], Board)
  else
     solve($[ff,updown,report(printf("z=%d\n", AmountOfQueens))], Board)  
  end.