/* 

  Binary Sudoku in Picat.

  From http://eclipseclp.org/examples/binsudoku.ecl.txt
  The binary sudoku as explained here
  http://cstheory.stackexchange.com/questions/16982/how-hard-is-binary-sudoku-puzzle

  An NxN matrix must be filled with 0s and 1s such that:
   - each row and each column contains an equal number of 0s and 1s
   - no two rows or two columns are identical
   - no sequences of 3 or more consecutive 0s or 1s in rows or columns
  
  ?- solve(2, M).
  M = []([](1, 1, 0, 0, 1, 0, 1, 0, 1, 1, 0, 0),
         [](0, 1, 1, 0, 0, 1, 0, 1, 0, 0, 1, 1),
         [](1, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 0),
         [](1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0),
         [](0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1),
         [](0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0),
         [](1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1),
         [](1, 0, 1, 1, 0, 0, 1, 0, 0, 1, 0, 1),
         [](0, 1, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0),
         [](0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 0),
         [](1, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 1),
         [](0, 1, 0, 1, 0, 1, 0, 1, 1, 0, 0, 1))
  Yes (0.03s cpu, solution 1, maybe more)
  """

  Also see 
  * Marzio De Biasi: "Binary Puzzle is NP-complete"
    http://www.fractalmuse.org/vdisk/cstheory/binaryp.pdf

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

*/


% import util.
import cp.


main => go.


go =>
  Problem=2,
  time2(All=findall(Mat,binary_sudoku(Problem,Mat))),
  println(numSolutions=All.length),
  nl.

binary_sudoku(Problem,Mat) => 
  problem(Problem, Mat),
  println(problem=Problem),

  N = length(Mat),
  Mat.flatten() :: 0..1,
  K = N div 2,
  foreach(I in 1..N)
    sum([Mat[I,J] : J in 1..N]) #= K,
    sum([Mat[J,I] : J in 1..N]) #= K,
    sequence(1, 2, 3, [Mat[I,J] : J in 1..N]),
    sequence(1, 2, 3, [Mat[J,I] : J in 1..N]),
    foreach(J in I+1..N) 
      lex_ne([Mat[I,C] : C in 1..N], [Mat[J,C] : C in 1..N]),
      lex_ne([Mat[C,I] : C in 1..N], [Mat[C,J] : C in 1..N])
    end
  end,

  println(solve),
  solve([split],Mat),
  foreach(Row in Mat) println(Row) end,

  nl.


%
% Ensure that the lists L1 and L2 are not
% identical.
%
lex_ne(L1,L2) =>
  sum([L1[I] #!= L2[I] : I in 1..L1.length]) #> 0.


%
% sequence(+Low,+High,+K,+ZeroOnes)
%
% Definition from http://eclipseclp.org/doc/bips/lib/gfd/sequence-4.html
% """
% The number of occurrences of the value 1 is between Low and High for 
% all sequences of K variables in ZeroOnes
% """
%
sequence(Low,High,K,ZeroOnes) =>
  foreach(I in 1..ZeroOnes.length-K+1)
    V #= sum([ZeroOnes[J] : J in I..I+K-1]),
    V #>= Low,
    V #=< High
  end.

%
% Problem from http://eclipseclp.org/examples/binsudoku.ecl.txt
%
problem(2, Problem) => 
  Problem = 
    [
    [_,1,0,_,_,_,_,0,_,_,0,_],
    [_,1,1,_,_,1,_,_,_,_,_,_],
    [_,_,_,_,_,_,_,_,1,_,_,0],
    [_,_,0,0,_,_,_,_,_,_,_,0],
    [_,_,_,_,_,_,1,1,_,0,_,_],
    [_,1,_,0,_,1,1,_,_,_,1,_],
    [_,_,_,_,_,_,_,_,1,_,_,_],
    [1,_,_,1,_,_,_,_,_,_,0,_],
    [_,1,_,_,_,_,_,_,0,_,_,_],
    [_,_,_,_,_,_,_,0,_,_,_,_],
    [1,_,_,_,_,_,_,_,_,_,_,1],
    [_,1,_,1,_,_,_,_,_,0,0,_]
    ].