/* 

  n-queens problem with degree of diversity of a set of solutions in Picat.

  The objective is to diversify 9 solutions of 10-queens problem, using two
  extra constraint lex_chain_less and soft_alldifferent (defined in this model).

  From 
  http://www.emn.fr/z-info/sdemasse/gccat/Kdegree_of_diversity_of_a_set_of_solutions.html
  """
  S1=[0,2,5,7,9,4,8,1,3,6],
  S2=[0,3,5,8,2,9,7,1,4,6],
  S3=[1,3,7,2,8,5,9,0,6,4],
  S4=[2,4,8,3,9,6,1,5,7,0],
  S5=[3,6,9,1,4,7,0,2,5,8],
  S6=[5,9,2,6,3,1,8,4,0,7],
  S7=[6,8,1,5,0,2,4,7,9,3],
  S8=[8,1,4,9,7,0,3,6,2,5],
  S9=[9,5,0,4,1,8,6,3,7,2]
  
  The costs associated with the soft_alldifferent_ctr constraints of columns 
  1,2,...,10 are respectively equal to 
  1, 1, 1, 0, 1, 0, 1, 1, 1, and 1. 
  """


  Here's is a better - and proven optimal - solution with just 
  one not distinct column.

    soft_cost: [0, 0, 0, 0, 0, 0, 1, 0, 0, 0]
    total_cost: 1
    [ 1,  3,  6,  9,  7, 10,  4,  2,  8,  5]
    [ 3, 10,  8,  2,  4,  9,  7,  5,  1,  6]
    [ 4,  2,  9,  6, 10,  7,  1,  3,  5,  8]
    [ 5,  9,  2,  4,  8,  1,  3,  6, 10,  7]
    [ 6,  4,  7, 10,  3,  5,  8,  1,  9,  2]
    [ 7,  5, 10,  1,  6,  4,  2,  8,  3,  9]
    [ 8,  1,  4,  7,  9,  2,  5, 10,  6,  3]
    [ 9,  6,  3,  5,  2,  8, 10,  7,  4,  1]
    [10,  8,  5,  3,  1,  6,  2,  9,  7,  4]

  
  For n = 8, the minimal total_cost is 3:

  soft_cost: [0, 0, 0, 1, 0, 1, 0, 1]
  total_cost: 3
  [1, 7, 4, 6, 8, 2, 5, 3]
  [2, 8, 6, 1, 3, 5, 7, 4]
  [3, 5, 7, 1, 4, 2, 8, 6]
  [4, 6, 1, 5, 2, 8, 3, 7]
  [5, 3, 8, 4, 7, 1, 6, 2]
  [7, 1, 3, 8, 6, 4, 2, 5]
  [8, 2, 5, 3, 1, 7, 4, 6]


  For n=7 the total_cost = 0
  soft_cost: [0, 0, 0, 0, 0, 0, 0]
  total_cost: 0
  [1, 3, 5, 7, 2, 4, 6]
  [2, 4, 6, 1, 3, 5, 7]
  [3, 5, 7, 2, 4, 6, 1]
  [4, 6, 1, 3, 5, 7, 2]
  [5, 7, 2, 4, 6, 1, 3]
  [6, 1, 3, 5, 7, 2, 4]


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

*/

import sat.


main => go.

go ?=>
  nolog,
  N = 8,
  println(n=N),

  time(queens_diversity(N, X,SoftCost,TotalCost)),
  foreach(Row in X)
    println(Row)
  end,
  println(softCost=SoftCost),
  println(totalCost=TotalCost),
  nl,
  
  nl.

go => true.

%
% Optimal solutions for N=2..10
% 
go2 ?=>
  nolog,
  member(N,2..10),
  println(n=N),

  if time(queens_diversity(N, X,SoftCost,TotalCost)) then
    foreach(Row in X)
      println(Row)
    end,
    println(softCost=SoftCost),
    println(totalCost=TotalCost),
    nl
  end,
  fail,
  
  nl.

go2 => true.



queens_diversity(N, X,SoftCost,TotalCost) =>
  % decision variables

  M = N-1,
  X = new_array(M,N),
  X :: 1..N, 

  % costs for soft_all_different
  SoftCost = new_list(N),
  SoftCost :: 0..1, 

  TotalCost #= sum(SoftCost),

  foreach(J in 1..N)
    % soft all different on columns
    soft_alldifferent([X[I,J] : I in 1..M], SoftCost[J])
  end,

  foreach(I in 1..M)
    queens(X[I])
  end,

  % symmetry breaking
  lex_chain_less(X),  
  % X[1,1] #= 1,

  % Checking (the soft costs from the example shown above)
  % if N = 10 then 
  %    SoftCost = [1,1,1,0,1,0,1,1,1,1]
  % end,
  
  Vars = X.vars ++ SoftCost,
  solve($[min(TotalCost),ff,split,report(printf("totalCost: %d\n",TotalCost))], Vars).


queens(Q) =>
  N = Q.len,
  all_different(Q),
  all_different($[Q[I]+I : I in 1..N]),
  all_different($[Q[I]-I : I in 1..N]).


%
% Require that all the rows are lexicographically sorted
% (but not the columns as in lex2).
% See: http://www.emn.fr/z-info/sdemasse/gccat/Clex_chain_less.html
%
lex_chain_less_xxx(A) =>
  Len1 = A.len,
  Len2 = A[1].len,
  foreach(I in 2..Len1)
     lex_le([A[I-1,J] : J in 1..Len2], 
            [A[I , J] : J in 1..Len1])
  end.

lex_chain_less(X) =>
  N = X.len,
  M = X[1].len,
  foreach(I in 2..N) 
    lex_lt([X[I-1, J] : J in 1..M], [X[I, J] : J in 1..M])
  end.


%
% Sum is the number of pairs that have the same value.
%
% See http://www.emn.fr/z-info/sdemasse/gccat/Csoft_alldifferent_ctr.html
%
soft_alldifferent(A,Sum) =>
  N = A.len,
  Sum #= sum([A[I] #= A[J] : I in 1..N, J in I+1..N]).