/* 

  in Picat.

  From  From Tadao Kitzawa "Arithmetical, Geometrical and Combinatorial Puzzles from Japan", 
  problem 2, page 1
  """
  Problem 3
  The first 60 positive integers are to be partitioned into thirty pairs so that
  the difference between the two numbers in the same pair is either 1 or 10.
  Given that two of the pairs are (10,11) and (20,30), which number is paired
  with 41?
  """

  There are a lot of solutions given these constraints.
  Since we don't want to generate all solutions, here is another
  approach:
  * first get one solution (with T=40) 
  * if there are any solution where T != 40
  Since there isn't any solutions with T != 40, we conclude that 40 is the answer.
  
  The output is
    x = {{1,2},{3,13},{4,14},{5,15},{6,16},{7,17},{8,18},{9,19},{10,11},{12,22},{20,30},{21,31},{23,33},{24,34},{25,35},{26,36},{27,37},{28,38},{29,39},{32,42},{40,41},{43,44},{45,46},{47,48},{49,59},{50,60},{51,52},{53,54},{55,56},{57,58}}
    t = 40
    Our conjecture is that T = 40
    Is there any solution with T != 40?
    OK, we got no other solution!


  This 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,
  s(X,T,_),
  println(x=X),
  println(t=T),
  println("Our conjecture is that T"=T),
  printf("Is there any solution with T != %d?\n",T),  
  if not s(_X2,T2,T) then
     println("OK, we got no other solution!")
  else
     println("Not OK, we got another solution with T"=T2)  
  end,
  nl.
go => true.



s(X,T, Check) => 
  N = 60, % 1..60
  M = N div 2, % number of pairs

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

  % Partition the values
  all_distinct(X.vars),

  % 
  foreach(I in 1..M)
    X[I,1] #< X[I,2], % symmetry
    % Difference between each pair is either 1 or 10
    (X[I,2] - X[I,1] #= 1) #\/ (X[I,2] - X[I,1] #= 10)
  end,

  % Given
  [Ix1,Ix2] :: 1..M,
  matrix_element(X,Ix1,1,10), % For some row Ix1
  matrix_element(X,Ix1,2,11),

  matrix_element(X,Ix2,1,20), % For some row Ix2
  matrix_element(X,Ix2,2,30),

  % Symmetry
  increasing([X[I,1] : I in 1..M]),

  % The value we want. It can only be one of these values.
  T :: [31,40,42,51],
  % We don't know if T is the first or second value in the pair.
  sum([ (X[I,1] #=  T #/\ X[I,2] #= 41)
        #\/
        (X[I,1] #= 41 #/\ X[I,2] #=  T)
        : I in 1..M]) #= 1,

  if nonvar(Check) then
    T #!= Check % checking our conjecture: This fails so 40 is the answer.
  end,

  Vars = X.vars ++ [T,Ix1,Ix2],  
  solve($[ff,split],Vars).