/*

  Global constraint all_differ_from_at_least_k_pos in Picat.

  From Global Constraint Catalog
  http://www.emn.fr/x-info/sdemasse/gccat/Call_different_from_at_least_k_pos.html
  """
  Enforce all pairs of distinct vectors of the VECTORS collection to differ 
  from at least K positions.
  
  Example
  (
   2, <
   vec-<2, 5, 2, 0>,
   vec-<3, 6, 2, 1>,
   vec-<3, 6, 1, 0>
   >
 )
  
  The all_differ_from_at_least_k_pos constraint holds since:
   * The first and second vectors differ from 3 positions, which is 
     greater than or equal to K=2.
   * The first and third vectors differ from 3 positions, which is greater 
     than or equal to K=2.
   * The second and third vectors differ from 2 positions, which is greater 
     than or equal to K=2.
  """

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

*/

import util.
import cp.

main => go.

go =>
   Rows = 3,
   Cols = 4,

   X = new_array(Rows,Cols).array_matrix_to_list_matrix(),

   XList = vars(X),
   XList :: 0..6,


   K :: 0..Cols,
   K #= 2,

   % the example above
   % X = [[2,5,2,0],
   %      [3,6,2,1],
   %      [3,6,1,0]],

   X = [[2,5,2,_],
        [3,6,2,1],
        [3,6,1,0]],
   

   % fails
   % X = [[2,5,2,0],
   %     [2,5,2,1],
   %     [3,6,1,0]],

   all_differ_from_at_least_k_pos(K,X),

   Vars = XList ++ [K],
   solve([],Vars),

   write(k=K),nl,
   foreach(Row in X) writeln(Row) end,
   nl.



all_differ_from_at_least_k_pos(K,X) =>
   Len = X.length(),
   foreach(I in 1..Len, J in 1..Len)
      if I != J then
         sum([(R1 #!= R2) : {R1,R2} in zip(X[I],X[J])]) #>= K
      end
   end.