/* 

  Lam's Problem in Picat.

  http://www.comp.rgu.ac.uk/staff/ha/ZCSP/prob025/prob025.pdf  
  
  From
  http://www.cse.unsw.edu.au/~tw/csplib/prob/prob025/
  """
  Consider a 111 by 111 binary matrix. The goal is to put 11 zeros in each 
  row in such a way that each column has 11 zeros, and each pair of rows 
  must have exactly one zero in the same column.
  
  This problem is equivalent to finding a projective plane of order 10. 
  It is also equivalent to the <111,111,11,11,1> BIBD problem (prob028).
  
  ...
  Results
  """
  The problem has no solution. This shows that finite projective planes of 
  order 10 do not exist.
  
  The proof caused some controversy as it used computer brute force 
  (2,000 hours on a Cray) and no one has been able (or is ever likely to 
  be able) to check it by hand. Can constraint satisfaction algorithms 
  reduce the size of this task?
  
  Browne, M. W. "Is a Math Proof a Proof If No One Can Check It?" 
  New York Times, Sec. 3, p. 1, col. 1, Dec. 20, 1988.
  
  Petersen, I. "Search Yields Math Proof No One Can Check." Science 
  News 134, 406, Dec. 24 & 31, 1988. 
  """

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

*/

import sat. % 41.3s
% import cp.
% import mip.
% import smt.


main => go.

go ?=>
  println("There is no solution to this problem!"),
  N = 11,
  M :: 0..N,
  X = new_array(N,N),
  X :: 0..1,

  % rows 
  foreach(I in 1..N)
    sum([X[I,J] #= 0 : J in 1..N]) #= M
  end,
  
  % columns
  foreach(J in 1..N)
    sum([X[I,J] #= 0 : I in 1..N]) #= M
  end,
  
  % pair of rows have exactly one 0 in same column
  foreach(I in 1..N, J in 1..N, I != J) 
    sum([X[I,K] #= X[J,K] #/\ X[J,K] #= 0 : K in 1..N]) #= 1
  end,

  Vars = X.vars ++ [M],
  solve([degree,split],Vars),

  println(m=M),
  foreach(Row in X) println(Row) end,
  nl,
  fail,

  
  nl.

go => true.