/* 

  A diamond ring in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 140. A diamond ring

  We have a ring with diamond stone whose "atoms" are joined in 10 rows of 3 atoms
  each. Select 13 integers, of which 12 are different, and place them in the "atoms" so
  that each row totals 20. The smallest number needed is 1, the largest is 15. 

  [Groza: There are six solutions, with one of them illustrated below. Can you find 
  the other five?] 
  (adapted from puzzle 325 from Kordemsky (1992))
  """

        n1   n2     n3

           n4   n5

        n6  n7      n8

           n9   n10

        n11   n12   n13


  Without any symmetry breaking, this model yields 48 solutions. 

  Symmetry breaking and number of solutions:
  - 1) X[1] #= min([X[1],X[3],X[11],X[13]])   14 solutions
  - 2) X[2] #= min([X[2],X[6],X[8],X[12]])    12 solutions
  - 3) X[1] #= 11 (as Kordemsky's solution     4 solutions
  - 2) and 3)                                  2 solutions

  Here are the two solutions when combining symmetry breaking 2) and 3):

    x = [11,1,8,13,14,6,2,5,4,5,3,10,7]
    11       1       8 
        13       14
    6        2       5 
        4        5 
    3        10      7 

    x = [11,1,8,15,12,4,2,7,6,3,5,10,5]
    11       1       8 
        15       12
    4        2       7 
         6        3 
    5        10      5 



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

*/

import cp.

main => go.

go =>
  N = 13,
  M = 15,
  X = new_list(N),
  X :: 1..M,
  
  Rows = [
           [1,2,3],
           [1,6,11],
           [2,4,6],
           [2,5,8],
           [3,8,13],
           [4,7,10],
           [5,7,9],
           [6,9,12],
           [8,10,12],
           [11,12,13]
        ],
  foreach(Row in Rows)
    sum([X[I] : I in Row]) #= 20
  end,

  % There are 12 different values
  nvalue(12,X),

  % Symmetry breaking
  % X[1] is the minimum of the four corners
  % X[1] #= min([X[1],X[3],X[11],X[13]]), % 14 solutions
  
  % X[2] is the minimum of the mid border numbers
  X[2] #= min([X[2],X[6],X[8],X[12]]), % 12 solutions
  
  % As in Kordemsky's solution
  X[1] #= 11, % 4 solutions (with X[2] #= min(...): 2 solutions)

  Vars = X,
  solve(Vars),
  
  println(x=X),
  printf("%-2d       %-2d      %-2d\n",X[1],X[2],X[3]),
  printf("    %-2d       %-2d\n",X[4],X[5]),  
  printf("%-2d       %-2d      %-2d\n",X[6],X[7],X[8]),
  printf("    %-2d       %-2d\n",X[9],X[10]),    
  printf("%-2d       %-2d      %-2d\n",X[11],X[12],X[13]),
  nl,
  fail,

  nl.