/*
The first trial (Smullyan) puzzle in Picat.
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
"""
The following [...] puzzles are taken from Raymond Smullyan's "The Lady or the Tiger".
In each puzzle a prisoner is faced with a decision where he must open one of two doors.
Behind each door is either a lady or a tiger. They may be both tigers, both ladies
or one of each. 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. Of course, the prisoner
would prefer to be married than eaten alive. Each of the doors has a sign bearing a
tatement that may be either true or false.
3. The First Trial
The statement on door one says, "In this room there is a lady, and in the other
room there is a tiger."
The statement on door two says, "In one of these rooms there is a lady, and in
one of these rooms there is a tiger."
The prisoner is informed that one of the statements is true and one is false.
Door 1 - tiger
Door 2 - lady
"""
This model was inspired by the XPress Mosel model created by Martin Chlond.
http://www.chlond.demon.co.uk/puzzles/sol3s3.html
This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
See also my Picat page: http://www.hakank.org/picat/
*/
import cp.
import util.
main => go.
go =>
Door = 2,
Prize = 2, % 1 = Lady, 2 = Tiger
% 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,
% dummy variables
D = new_list(2),
D :: 0..1,
% each door hides 1 prize
foreach(I in 1..Door)
sum([X[I,J] : J in 1..Prize]) #= 1
end,
% 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 is true
T[1]+T[2] #= 1,
Vars = X.vars() ++ T ++ D,
solve(Vars),
println(t=T),
printf("Statement on door %d is true.\n", find_first_of(T,1)),
println(x=X),
printf("The Lady is behind door %d\n", find_first_of(X[1],1)),
printf("The Tiger is behind door %d\n", find_first_of(X[2],1)),
nl.