/* 

  The High-IQ society problem in Picat.

  From the Prolog code in
  Simon Colton's AI lecture "Constraint Satisfaction Problems"
  http://www.doc.ic.ac.uk/~sgc/teaching/pre2012/v231/lecture15.html 
  """ 
  I was perhaps most proud of AI on a Sunday. On this particular Sunday, 
  a friend of mine found an article in the Observer about the High-IQ society, 
  a rather brash and even more elitist version of Mensa. Their founder said 
  that their entrance test was so difficult that some of the problems had 
  never been solved. The problem given below was in the Observer as such an 
  unsolved problem. After looking at it for a few minutes, I confidently 
  told my friend that I would have the answer in half an hour. 

  After just over 45 minutes, I did indeed have an answer, and my friend 
  was suitably impressed. See the end of these notes for the details. Of 
  course, I didn't spend my time trying to figure it out (if you want to 
  split the atom, you don't sharpen a knife). Instead, I used the time to 
  describe the problem to a constraint solver, which is infinitely better 
  at these things than me. The constraint solver is part of good old 
  Sicstus Prolog, so specifying the problem was a matter of writing it as 
  a logic program - it's worth pointing out that I didn't specify how to 
  find the solution, just what the problem was. With AI programming 
  languages such as Prolog, every now and then the intelligence behind 
  the scenes comes in very handy. Once I had specified the problem to 
  the solver (a mere 80 lines of Prolog), it took only one hundredth 
  of a second to solve the problem. So not only can the computer solve 
  a problem which had beaten many high IQ people, it could solve 100 of 
  these "difficult" problems every second. A great success for AI.

  (
    Caption of picture: The square below contains 24 smaller squares, each 
    with a different integral size. Determine the length of the shaded square.
  )
  """

  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 =>
  Top = 200,
  println(top=Top),
  go(Top, List),
  println(List),
  nl.

/*
  """
  type go(200, Answer) to run the program. 200 is the highest side
  length it will look for.
  """
*/
go(Top, List) =>
    List = [L1,L2,L3,L4,L5,L6,L7,L8,L9,L10,L11,L12,L13,L14,
            L15,L16,L17,L18,L19,L20,L21,L22,L23,L24,L25],
    statistics(runtime,_),

    /* Domains */
    List :: 1..Top,

    /* Ordering */
    increasing(List),
    all_different(List),

    /* Sum of Squares Constraint */
    List[25]**2 #= sum([List[I]**2 : I in 1..24]),

    /* Length Constraints */
    L1 + L3 #= L4, L4 + L1 #= L5,
    L4 + L5 #= L7, L5 + L7 #= L8,
    L3 + L4 + L7 #= L9, L1 + L5 + L8 #= L11,
    L2 + L12 #= L14, L2 + L14 #= L15,
    L2 + L15 #= L16, L10 + L11 #= L17,
    L7 + L8 + L9 #= L18, L6 + L16 #= L19,
    L6 + L19 #= L20, L9 + L18 #= L21,
    L10 + L17 #= L22, L14 + L15 #= L23,
    L13 + L20 #= L24, L21 + L22 + L23 #= L25,
    L18 + L21 + L24 #= L25, L19 + L20 + L24 #= L25,
    L15 + L16 + L19 + L23 #= L25,
    
    /* Find the Answer */
    solve([ff],List),

    /* Write the Answer */
    foreach(I in 1..25)
       printf("L%d = %d\n", I, List[I])
    end,
    nl,

    /* Double check the Answer */
    LHS = sum([List[I]*List[I] : I in 1..24]),

    RHS = L25*L25,
    println(lhs=LHS),
    println(rhs=RHS),nl,

    /* Stop the timer */
    statistics(runtime,[_,TimeTaken]),
    printf("TimeTaken: %d ms", TimeTaken),
    nl.

increasing(List) =>
   foreach(I in 2..List.length) List[I-1] #< List[I] end.