/* 

  The Logical Labyrinth (Smullyan) in Picat.

  From Martin Chlond Integer Programming Puzzles:
  http://www.chlond.demon.co.uk/puzzles/puzzles4.html, puzzle nr. 3
  Description  : The Logical Labyrinth
  Source       : Smullyan, R., (1991), The Lady or The Tiger, Oxford University Press
  """
  3. A Logical Labyrinth

  A prisoner is faced with a decision where he must open one of nine doors. The 
  rooms behind each door may be empty or contain either a lady or a tiger.

  If the prisoner opens a door to find a lady he will marry her and if he opens 
  a door to find a tiger he will be eaten alive. The prisoner would prefer to 
  be married than either be eaten alive or to face emptiness. Each door has a 
  sign bearing a statement which may be either true or false.

   The statements on the nine doors are:
   1. The lady is an odd-numbered room
   2. This room is empty
   3. Either sign 5 is right or sign 7 is wrong
   4. Sign 1 is wrong
   5. Either sign 2 or sign 4 is right
   6. Sign 3 is wrong
   7. The lady is not in room 1
   8. This room contains a tiger and room 9 is empty
   9. This room contains a tiger and sign 6 is wrong

  In addition, the prisoner is informed that only one room contains a lady; each 
  of the others either contain a tiger or are empty. The sign on the door of the 
  room containing the lady is true, the signs on all the doors containing tigers 
  are false, and the signs on the doors of empty rooms can be either true or false.

  The prisoner is told whether or not room eight is empty and this knowledge helps 
  him find a unique solution.(Smullyan)
  """

  This is a port of the Xpress-Mosel Model model 'trial12'
  """
  Description  : The Logical Labyrinth
  Source       : Smullyan, R., (1991), The Lady or The Tiger, Oxford University Press
  Date written : Xpress-MP 21/12/99, Mosel 19/4/03
  Written by   : M J Chlond 
  """ 

  Solution
  """
  The lady is in Room Seven. Note: If room 8 was empty then there is not enough 
  information to identify a unique location for the lady. Therefore, the king must 
  have informed the prisoner that room 8 was not empty. This may be verified by 
  experimentation with the following model.
  """

  Cf trial12.pi

  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 =>
  Door  = 9,
  Prize = 3, % 1 = Lady, 2 = Tiger, 3 = Empty

  % x(i,j) = 1 if door i hides prize j, else 0
  X = new_array(Door,Prize),
  X :: 0..1,

  % t(i) = 1 if statement on door i is true, else 0
  T = new_list(Door),
  T :: 0..1,

  % if statement on door 1 is true (i.e. x[1,1]+x[3,1]+x[5,1]+x[7,1]+x[9,1] = 1 ] 
  %                                       then t(1] = 1, else t(1] = 0
  T[1] #= X[1,1]+X[3,1]+X[5,1]+X[7,1]+X[9,1], 

  % if statement on door 2 is true (i.e. x[2,3]=1] then t[2] = 1, else t[2] = 0
  T[2] #= X[2,3], 

  % if statement on door 3 is true (i.e. t[5]+x[1,1] > 1 ] then t[3] = 1, else t[3] = 0
  T[5]+X[1,1]-2*T[3] #<= 0, 
  T[5]+X[1,1]-T[3] #>= 0, 

  % if statement on door 4 is true (i.e. t[1] = 0] then t[4] = 1, else t[4] = 0
  T[4] #= 1-T[1], 

  % if statement on door 5 is true (i.e. t[2]+t[4] > 1] then t[5] = 1, else t[5] = 0
  T[2]+T[4]-2*T[5] #<= 0, 
  T[2]+T[4]-T[5] #>= 0, 

  % if statement on door 6 is true (i.e. t[3] = 0 ] then t[6] = 1, else t[6] = 0
  T[6] #= 1-T[3], 

  % if statement on door 7 is true (i.e. x[1,1] = 0] then t[7] = 1, else t[7] = 0
  T[7] #= 1-X[1,1], 

  % if statement on door 8 is true (i.e. x[8,2]+x[9,3] = 2 ] then t[8] = 1, else t[8] = 0
  X[8,2]+X[9,3]-2*T[8] #<= 1, 
  X[8,2]+X[9,3]-2*T[8] #>= 0, 

  % if statement on door 9 is true (i.e. x[9,2]+t[3] = 2] then t[9] = 1, else t[9] = 0
  X[9,2]+T[3]-2*T[9] #<= 1, 
  X[9,2]+T[3]-2*T[9] #>= 0, 

  % each door hides 1 prize
  foreach(I in 1..Door)
    sum([X[I,J] : J in 1..Prize]) #= 1
  end,

  % only one room contains lady
  sum([X[I,1] : I in 1..Door]) #= 1,


  % sign on lady's door is true
  foreach(I in 1..Door)
    T[I] #>= X[I,1]
  end,

  % sign on tigers' doors are false
  foreach(I in 1..Door)
    T[I] #<= 1 - X[I,2]
  end,


  % if room 8 is empty then not enough information to pinpoint lady
  % min and max x[7,1] give different results

  % room 8 is empty
  % x[8,3] #= 1,

  % if room 8 is not empty then enough information
  % min and max x[7,1] gives same results
  % if the prisoner was able to deduce where the lady was then
  % room 8 must not have been empty

  % room 8 is not empty
  X[8,3] #= 0,

  Vars = X.vars ++ T,
  solve(Vars),

  % foreach(Row in X) println(Row.to_list) end,
  println(lady=[D : D in 1..Door, X[D,1] == 1]),
  % println(tiger=[D : D in 1..Door, X[D,2] == 1]),
  % println(empty=[D : D in 1..Door, X[D,3] == 1]),
  println(t=T),  
  nl,
  fail,

  nl.