/* 

  Perfect man puzzle in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  See https://www.researchgate.net/publication/374588335_Measuring_reasoning_capabilities_of_ChatGPT
  """
  Puzzle 55. Perfect man

  Susan's perfect man has black hair, brown eyes, and is tall and slim. Susan knows four
  men: Arthur, Bill, Charles, and Dave. Only one of them has all the characteristics that
  Susan requires.
  1. Arthur and Bill have the same eye colour.
  2. Only one of the men has both black hair and brown eyes.
  3. Bill and Charles have the same hair colour.
  4. Only two of the men are both tall and slim.
  5. Charles and Dave are of differing build.
  6. Only two of the men are both tall and dark-haired.
  7. Dave and Arthur are the same height.
  8. Only three of the men are both slim and brown-eyed.
  Who is Susan's perfect man? (taken from Clessa (1996))
  """

  Here we have some assumptions. Either a person has/is
  - black hair or not
  - brown eyes or not
  - tall or not
  - slim or not
  And also that dark hair = black hair (clue 6)
  
  This model yields 2 solutions, both stating that Arthur is the perfect man.

  Here are the solutions with details:
  Arthur = [hair = [1,2,2,1],eyes = [1,1,1,2],height = [1,1,2,1],build = [1,1,1,2],person = [1]]
  Arthur = [hair = [1,2,2,1],eyes = [1,1,1,2],height = [1,2,1,1],build = [1,1,1,2],person = [1]]
                                                          ^ ^
  The difference is whether Bill and Charles are tall or not.

  Groza's Mace4 first order logic model yields 8 solutions, all stating that Arthur 
  is the perfect man.


  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 = 4,

  % The perfect man is the man with all 1s in Hair, Eyes, Height, and Build

  Names = [Arthur,Bill,Charles,Dave],
  Names = 1..N,
  NamesS = ["Arthur","Bill","Charles","Dave"],

  HairBlack = 1,
  HairNotBlack = 2,
  Hair = new_list(N),
  Hair :: [HairBlack,HairNotBlack],  
  
  EyesBrown = 1,
  EyesNotBrown = 2,
  Eyes = new_list(N),
  Eyes :: [EyesBrown,EyesNotBrown],

  HeightTall = 1,
  HeightNotTall = 2,
  Height = new_list(N),
  Height :: [HeightTall,HeightNotTall],

  BuildSlim = 1,
  BuildNotSlim = 2,
  Build = new_list(N),
  Build :: [BuildSlim,BuildNotSlim],

  % 1. Arthur and Bill have the same eye colour.
  Eyes[Arthur] #= Eyes[Bill],
  
  % 2. Only one of the men has both black hair and brown eyes.
  sum([Hair[P] #= HairBlack #/\ Eyes[P] #= EyesBrown : P in 1..N]) #= 1,
  
  % 3. Bill and Charles have the same hair colour.
  Hair[Bill] #= Hair[Charles],
  
  % 4. Only two of the men are both tall and slim.
  sum([Height[P] #= HeightTall #/\ Build[P] #= BuildSlim : P in 1..N]) #= 2,
  
  % 5. Charles and Dave are of differing build.
  Build[Charles] #!= Build[Dave],
  
  % 6. Only two of the men are both tall and dark-haired.
  % hakank: I assume that dark-haired = Black hair
  sum([Height[P] #= HeightTall #/\ Hair[P] #= HairBlack  : P in 1..N]) #= 2,  
  
  % 7. Dave and Arthur are the same height.
  Height[Dave] #= Height[Arthur],
  
  % 8. Only three of the men are both slim and brown-eyed.
  sum([Build[P] #= BuildSlim #/\ Eyes[P] #= EyesBrown : P in 1..N]) #= 3,

  % Who is Susan's perfect man? (taken from Clessa (1996))

  % Susan's perfect man has black hair, brown eyes, and is tall and slim.
  Person :: 1..N,
  element(Person,Hair,HairBlack),
  element(Person,Eyes,EyesBrown),
  element(Person,Height,HeightTall),
  element(Person,Build,BuildSlim),

  Vars = [hair=Hair,eyes=Eyes,height=Height,build=Build,person=[Person]],
  solve(Vars),
  
  println(NamesS[Person]=Vars),
  fail,
  nl.
go => true.