% 
% The first trial (Smullyan) puzzle in MiniZinc.
%
% From Martin Chlond Integer Programming Puzzles:
% http://www.chlond.demon.co.uk/puzzles/puzzles3.html, puzzle nr. 3.
% Description  : The First Trial
% 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/sol3s3.html

%
% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc
%
int: door = 2;
int: prize = 2; % 1 = Lady, 2 = Tiger

set of 1..door: D = 1..door;
set of 1..prize: P = 1..prize;
array[D,P] of var 0..1: x;  % x(i,j) = 1 if door i hides prize j, else 0
array[D] of var 0..1: t;    % t(i) = 1 if statement on door i is true, else 0
array[1..2] of var 0..1: d; % dummy variables

solve satisfy;

constraint
  % each door hides 1 prize
  forall(i in D) (
    sum(j in P) (x[i,j]) = 1
  )

  /\ % if statement on door 1 is true then set t[1] = 1, else t[1] = 0
  x[1,1]+x[2,2]-t[1] <= 1 /\
  x[1,1]+x[2,2]-2*t[1] >= 0 

  /\ % if statement on door 2 is true then set t[2] = 1, else t[2] = 0
  x[1,1]-x[2,2]-2*d[1] <= -1  /\
  x[1,1]-x[2,2]-d[1] >= -1 /\

  x[1,1]-x[2,2]+2*d[2] >= 1 /\
  x[1,1]-x[2,2]+2*d[2] <= 2 /\

  d[1]+d[2]-t[2] <= 1 /\
  d[1]+d[2]-2*t[2] >= 0 /\

  % only one statement true
  t[1]+t[2] = 1
;


output 
[
  if j = 1 then "\n" else " " endif ++
    show(x[i,j])
  | i in D, j in P
] ++
[
 if i = 1 then "\n" else "" endif ++
 show(t[i]) ++ "\n"
 | i in D
];