/* 

  Schur numbers Picat.

  http://dominia.org/~damancha/part.html
  """
  1. A set S is said to be "sum-free" if there exist no three (not necessarilly 
     distinct) elements a,b,c in S where a+b=c

  2. A set S is said to be "weakly sum-free" if there exist no three distinct 
     elements of S a,b,c such that a+b=c

  3. Schur number s(n) is the maximum m, such that [1,m] can be partitioned into 
     n sum-free subsets (The known schur numbers are s(1)=1, s(2)=4, s(3)=13, s(4)=44) 
     known bounds for the 5th schur are 160<=s(5)<=315.
  """

  Also, see http://mathworld.wolfram.com/SchurNumber.html

  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 => time2(go).

% Testing n=4. Schur number is 44
go =>
   test_schur(4,50,4),
   nl.

% Testing n=5. Schur number is >= 160, <= 315
go2 =>
   foreach(Timeout in 10..10..1000)
       test_schur(5,160,315,Timeout)
   end,
   nl.


test_schur(N, Upper, Timeout) =>
   test_schur(N, 2, Upper, Timeout).

test_schur(N, Lower, Upper, Timeout) =>

   NBoxes = N,
   NBalls :: Lower..Upper,
   indomain(NBalls),

   println([boxes=NBoxes,balls=NBalls,timeout=Timeout]),

   time_out(once(schur(NBalls,NBoxes, X)),Timeout*1000, Status),

   if Status == success then
        print_boxes(X),
        fail
   else
        println(timeout)
   end,
   nl.



schur(NBalls,NBoxes,X) =>

    X = new_list(NBalls),
    X :: 1..NBoxes,
    
    foreach(I in 1..NBalls, J in 1..NBalls, K in 1..NBalls)
        if I+J==K then
           X[I] #!= X[J] #\/ X[J] #!= X[K]        
        end
    end,

    % symmetry breaking
    foreach(I in 1..min(NBoxes,NBalls)) 
       X[I] #=< I
    end,
  
    solve([ff,split], X).


print_boxes(X) => 
   println(x=X),
   foreach(Box in 1..max(X)) 
      printf("Box %2d: ", Box),
      foreach(Ball in 1..X.length)
         if X[Ball] == Box then
           printf("%3d ", Ball)
         end
      end,
      nl
   end,
   nl.