% 
% The Logical Labyrinth (Smullyan) puzzle in MiniZinc.
%
% 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

%
% This model was inspired by the XPress Mosel model created by Martin Chlond.
% http://www.chlond.demon.co.uk/puzzles/sol4s3.html

%
% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc
%

int: door  = 9;
int: prize = 3; % 1 = Lady, 2 = Tiger, 3 = Empty

array[1..door, 1..prize] of var 0..1: x; % x(i,j) = 1 if door i hides prize j, else 0
array[1..door] of var 0..1: t; %! t(i) = 1 if statement on door i is true, else 0

solve satisfy;

constraint

  % 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
  forall(i in 1..door) (
     sum(j in 1..prize) (x[i,j]) = 1 
  )
  /\
  % only one room contains lady
  sum(i in 1..door) (x[i,1]) = 1
  /\
  % sign on lady's door is true
  forall(i in 1..door) (
    t[i] >= x[i,1] 
  )
  /\
  % sign on tigers' doors are false
  forall(i in 1..door) (
     t[i] <= 1 - x[i,2]
  )
  /\

  % 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
;

output [
  if j = 1 then "\n" else " " endif ++
  show(x[i,j])
  | i in 1..door, j in 1..prize
];