-
Notifications
You must be signed in to change notification settings - Fork 54
Zebra puzzle
For an example of nondeterministic programming, we're going to solve the well-known Zebra puzzle. This is the version given on Wikipedia:
- There are five houses.
- The Englishman lives in the red house.
- The Spaniard owns the dog.
- Coffee is drunk in the green house.
- The Ukrainian drinks tea.
- The green house is immediately to the right of the ivory house.
- The Old Gold smoker owns snails.
- Kools are smoked in the yellow house.
- Milk is drunk in the middle house.
- The Norwegian lives in the first house.
- The man who smokes Chesterfields lives in the house next to the man with the fox.
- Kools are smoked in the house next to the house where the horse is kept.
- The Lucky Strike smoker drinks orange juice.
- The Japanese smokes Parliaments.
- The Norwegian lives next to the blue house.
Now, who drinks water? Who owns the zebra?
In the interest of clarity, it must be added that each of the five houses is painted a different color, and their inhabitants are of different national extractions, own different pets, drink different beverages and smoke different brands of American cigarets [sic]. One other thing: in statement 6, right means your right.
—Life International, December 17, 1962
Fans of Prolog will know that Prolog can solve this problem very elegantly. Given that Mercury has many similarities to Prolog, you might hope that the same elegant solution could be expressed in Mercury. Unfortunately not, as Mercury does not support Prolog-style logic variables.
Instead, we are limited to the more basic generate-and-test approach: generate a potential solution to the problem, then test if it satisfies the conditions. If not, backtrack to generate and test another potential solution. This would not be viable when the search space is very large, but it's okay for this small puzzle.
The puzzle's clues mention various entities: houses, people, pets, drinks and cigarettes. In the solution that we are presenting, we will only require a type to represent the five people, identified by nationality. The other entities will be represented by variables.
:- type person
---> english
; spanish
; ukrainian
; norwegian
; japanese.
The key to the solution is to generate different assignments of people
to houses, house colours, pets, drinks, and cigarettes.
The list
module contains a predicate that does what we need.
% perm(List0, List):
%
% True iff `List' is a permutation of `List0'.
%
:- pred perm(list(T)::in, list(T)::out) is multi.
For a call perm([1, 2, 3], Perm)
we would expect to get
these values of Perm
:
- [1, 2, 3]
- [1, 3, 2]
- [2, 1, 3]
- [3, 1, 2]
- [2, 3, 1]
- [3, 2, 1]
Let's consider how perm/2
is implemented.
The only permutation of an empty list is an empty list, so we can write:
perm([], []).
The only permutation of a singleton list is itself:
perm([X], [X]).
A list of two elements has two permutations:
perm([X, Y], [X, Y]).
perm([X, Y], [Y, X]).
We saw that there are six ways to permuate a list of three elements.
Before we go and write down the clauses, let's think about it a bit.
If we know that PermXs
is a permutation of Xs
, then to get a
permutation of [X | Xs]
then we just need to insert X
somewhere into
PermXs
. Then perm/2
can be implemented as:
:- pred perm(list(T), list(T)).
:- mode perm(in, out) is multi.
perm([], []).
perm([X | Xs], Perm) :-
perm(Xs, PermXs),
insert(X, PermXs, Perm).
We also need the insert/3
predicate:
:- pred insert(T, list(T), list(T)).
:- mode insert(in, in, out) is multi.
insert(X, [], [X]).
insert(X, [Y | Ys], Zs) :-
(
Zs = [X, Y | Ys]
;
insert(X, Ys, Zs0),
Zs = [Y | Zs0]
).
Onto the puzzle. There are five people living in five houses. We will use
a variable to represent each house, First
, Second
, Third
, Fourth
,
Fifth
, numbered from left to right. We will assign to each variable the
person living in that house. We can generate all the possible assignments
like this:
perm([english, spanish, ukrainian, norwegian, japanese],
[First, Second, Third, Fourth, Fifth])
Clue 10 states that the Norwegian lives in the first house, so there is no
point assigning different values to the First
variable. We can reduce the
number of permutations to test from 5! to 4! immediately.
% 10. The Norwegian lives in the first house.
First = norwegian,
perm([english, spanish, ukrainian, japanese],
[Second, Third, Fourth, Fifth]),
After the call to perm
, each of the variables First
through Fifth
will be assigned a value. If, later, it turns out that assignment does
not satisfy some condition of the puzzle, we can backtrack and try
another assignment of values.
Each of the five houses is painted a different colour. As before, we'll use one variable per colour, and the value of each variable will indicate the person living in a house of that colour.
One of the clues allows us to immediately assign a value to a variable. Then we generate assignments for the other colours:
% 2. The Englishman lives in the red house.
Red = english,
perm([spanish, ukrainian, norwegian, japanese],
[Green, Ivory, Yellow, Blue]),
Clue 10 and clue 15 together imply that the second house must be blue, so the person living in the second house must also be the person living in the blue house. We can check that:
% 10. The Norwegian lives in the first house.
% 15. The Norwegian lives next to the blue house.
Second = Blue,
Clue 6 provides another clue regarding house colours:
% 6. The green house is immediately to the right of the ivory house.
(
Ivory = First, Green = Second
;
Ivory = Second, Green = Third
;
Ivory = Third, Green = Fourth
;
Ivory = Fourth, Green = Fifth
),
That works, but we can make it a little neater with a helper predicate that tests if A is immediately to the left of B in a list:
:- pred left_of(list(T), T, T).
:- mode left_of(in, in, in) is semidet.
left_of([A, B | _], A, B).
left_of([_ | List], A, B) :-
left_of(List, A, B).
Now we can rewrite the rule for clue 6 more compactly:
Houses = [First, Second, Third, Fourth, Fifth],
% 6. The green house is immediately to the right of the ivory house.
left_of(Houses, Ivory, Green),
We will use variables to represent the owner of each pet, and generate the assignments of owners:
% 3. The Spaniard owns the dog.
Dog = spanish,
perm([english, ukrainian, norwegian, japanese],
[Snails, Fox, Horse, Zebra]),
There are a number of clues regarding who drinks what. We can write them down directly:
% 4. Coffee is drunk in the green house.
Green = Coffee,
% 5. The Ukrainian drinks tea.
Tea = ukrainian,
% 9. Milk is drunk in the middle house.
Milk = Third,
However, we must generate assignments of drinkers to beverages other than tea:
perm([english, spanish, norwegian, japanese],
[Coffee, Milk, Juice, Water]),
Note that we already have values assigned to Coffee
and Milk
.
The perm
call will still generate permutations in which the first two
elements of the permutation do not match Coffee
and Milk
, only to
be rejected after perm
returns. It's slightly unsatisfying.
Now to take care of the clues regarding the smokes:
% 7. The Old Gold smoker owns snails.
Snails = OldGold,
% 8. Kools are smoked in the yellow house.
Kools = Yellow,
% 13. The Lucky Strike smoker drinks orange juice.
LuckyStrike = Juice,
% 14. The Japanese smokes Parliaments.
Parliament = japanese,
perm([english, spanish, ukrainian, norwegian],
[OldGold, Kools, Chesterfield, LuckyStrike]),
Clue 11 says "The man who smokes Chesterfields lives in the house next to the man with the fox", which we can check like this:
% 11. The man who smokes Chesterfields lives in the house
% next to the man with the fox.
(
Chesterfield = First, Fox = Second
;
Chesterfield = Second, ( Fox = First ; Fox = Third )
;
Chesterfield = Third, ( Fox = Second ; Fox = Fourth )
;
Chesterfield = Fourth, ( Fox = Third ; Fox = Fifth )
;
Chesterfield = Fifth, Fox = Fourth
),
Let's introduce a helper predicate for the next-to relation:
:- pred next_to(list(T), T, T).
:- mode next_to(in, in, in) is semidet.
next_to(List, A, B) :-
( left_of(List, A, B)
; left_of(List, B, A)
).
Now we can rewrite clue 11 more compactly:
% 11. The man who smokes Chesterfields lives in the house
% next to the man with the fox.
next_to(Houses, Chesterfield, Fox),
Clue 12 is similar to clue 11:
% 12. Kools are smoked in the house next to the house
% where the horse is kept.
next_to(Houses, Kools, Horse),
That's all the clues accounted for.
For reasons that will become apparent, we'll put all that previous stuff
into a predicate called puzzle
that returns the complete solution as
a single term (a tuple). The predicate must be nondet
because we can't be
sure that it will find any solution (hence it cannot be multi
),
or that it won't find more than one solution (hence it cannot be semidet
).
:- pred puzzle({list(person), list(person), list(person), list(person),
list(person)}).
:- mode puzzle(out) is nondet.
puzzle({Houses, Colours, Pets, Drinks, Smokes}) :-
/* stuff goes here */
Houses = [First, Second, Third, Fourth, Fifth],
Colours = [Red, Green, Ivory, Yellow, Blue],
Pets = [Dog, Snails, Fox, Horse, Zebra],
Drinks = [Coffee, Tea, Milk, Juice, Water],
Smokes = [OldGold, Kools, Chesterfield, LuckyStrike, Parliament].
The main
predicate will call puzzle/1
to get the solution then show it to
the user. Assume we have a predicate to print out the solution. We might try
this:
:- pred main(io::di, io::uo) is det.
main(!IO) :-
puzzle(Solution),
write_solution(Solution, !IO).
Oh, there is a problem. puzzle/1
fails if it does not find a solution,
so we need to account for the failure. Next attempt:
main(!IO) :-
( if puzzle(Solution) then
write_solution(Solution, !IO)
else
write_string("No solution found.\n", !IO)
).
The compiler complains again:
zebra.m:007: In `main'(di, uo):
zebra.m:007: error: determinism declaration not satisfied.
zebra.m:007: Declared `det', inferred `multi'.
zebra.m:178: Call to `zebra.puzzle'(out) can succeed more than once.
zebra.m:179: In clause for `main(di, uo)':
zebra.m:179: in argument 2 of call to predicate `zebra.write_solution'/3:
zebra.m:179: mode error: variable `STATE_VARIABLE_IO_0' has instantiatedness
zebra.m:179: `mostly_unique',
zebra.m:179: expected instantiatedness was `unique'.
We haven't considered what to do if puzzle/1
finds multiple solutions.
We basically have three choices:
-
We can collect all the solutions before printing them out. We might choose to do this if we care about the different solutions, or to make sure that the solution is unique.
-
We can print out each solution immediate after finding it, instead of collecting them all first. This would show the user something even if exhaustively checking all possibilities would take too long.
-
We can print the first solution that
puzzle/1
finds and stop there.
The solutions
module provides a predicate to collect all solutions:
% solutions/2 collects all the solutions to a predicate and returns
% them as a list in sorted order, with duplicates removed.
%
:- pred solutions(pred(T), list(T)).
:- mode solutions(pred(out) is multi, out(non_empty_list)) is det.
:- mode solutions(pred(out) is nondet, out) is det.
We are going to pass puzzle/2
as the first argument to solutions/2
,
so that explains why we had to squeeze all the outputs of puzzle/1
into a tuple instead of returning them as separate arguments.
main(!IO) :-
solutions(puzzle, Solutions),
foldl(write_solution, Solutions, !IO).
Solutions
will contain a list of solutions, which are then printed
out with write_solution
.
If we want just a single solution, any solution, we can make use of committed choice nondeterminism.
There are two committed choice nondeterminism categories. cc_multi says that the procedure can produce one or more solutions but, unlike multi, will return only one of them; which one is arbitrary. cc_nondet says that the procedure can produce zero or more solutions but, unlike nondet, will return at most one of them; which one is arbitrary.
Consider one of our earlier attempts at main/2
.
:- pred main(io, io).
:- mode main(di, uo) is det.
main(IO0, IO) :-
( if puzzle(Solution) then
write_solution(Solution, IO0, IO)
else
write_string("No solution found.\n", IO0, IO)
).
The problem here was that the call to puzzle
can produce multiple
solutions so, for completeness, it must be possible to backtrack into
puzzle
for the second and subsequent solutions. It is not possible
to backtrack over I/O (we would need to be able to revert to an earlier
state-of-the-world) so this definition doesn't compile.
However, main/2
can be declared to have determinism cc_multi
, meaning
it is acceptable if main/2
prints only the first solution found by
puzzle/1
, whatever it is. We won't need any other solution from
puzzle/1
so backtracking over I/O is not required.
:- pred main(io, io).
:- mode main(di, uo) is cc_multi.
main(!IO) :-
( if puzzle(Solution) then
write_solution(Solution, !IO)
else
write_string("No solution found.\n", !IO)
).
A committed-choice procedure can only be called in a single-solution
context. A goal with no output variables is in a single-solution context.
The body of a procedure declared with cc_multi
or cc_nondet
is also
in a single-solution context so, in effect, "cc-ness" propagates up the
call graph up to main/2
. For more information about single-solution
contexts, please see the reference manual.
The third choice we had was to print solutions immediately after
puzzle/1
returns. We can do this using another predicate in the
solutions
module:
% unsorted_aggregate/4 generates all the solutions to a predicate
% and applies an accumulator predicate to each solution in turn.
% Declaratively, the specification is as follows:
%
% unsorted_aggregate(Generator, AccumulatorPred, Acc0, Acc) <=>
% unsorted_solutions(Generator, Solutions),
% list.foldl(AccumulatorPred, Solutions, Acc0, Acc).
%
% Operationally, however, unsorted_aggregate/4 will call the
% AccumulatorPred for each solution as it is obtained, rather than
% first building a list of all the solutions.
%
:- pred unsorted_aggregate(pred(T), pred(T, U, U), U, U).
:- mode unsorted_aggregate(pred(out) is nondet, pred(in, di, uo) is det,
di, uo) is cc_multi.
% many other modes omitted
It can be used just like this:
main(!IO) :-
unsorted_aggregate(puzzle, write_solution, !IO).
But notice that the mode of unsorted_aggregate
has determinism
cc_multi
so main/2
must be declared cc_multi
as well.
Why does unsorted_aggregate
have determinism cc_multi
and not det
?
Consider a call in which an accum
predicate collects the solutions produced
by gen
:
unsorted_aggregate(gen, accum, [], List)
The order that solutions are presented to accum
depends on the order
that they are generated by gen
. If gen
produces 1
first, then 2
,
the final value of List
might be [1, 2]
. On the other hand, if gen
produces the same solutions in the opposite order, then
the final value of List
might be [2, 1]
.
Since a single call unsorted_aggregate(gen, accum, [], List)
with the same input arguments can produce different solutions,
it can't be det
. cc_multi
indicates that unsorted_solutions
arbitrarily returns one of multiple valid solutions.
:- module zebra.
:- interface.
:- import_module io.
:- pred main(io, io).
:- mode main(di, uo) is cc_multi. % or det for all-solutions
:- implementation.
:- import_module list.
:- import_module solutions.
% perm
:- pred my_perm(list(T), list(T)).
:- mode my_perm(in, out) is multi.
my_perm([], []).
my_perm([X | Xs], Perm) :-
my_perm(Xs, PermXs),
my_insert(X, PermXs, Perm).
:- pred my_insert(T, list(T), list(T)).
:- mode my_insert(in, in, out) is multi.
my_insert(X, [], [X]).
my_insert(X, [Y | Ys], Zs) :-
(
Zs = [X, Y | Ys]
;
my_insert(X, Ys, Zs0),
Zs = [Y | Zs0]
).
% The puzzle
:- type person
---> english
; spanish
; ukrainian
; norwegian
; japanese.
:- pred left_of(list(T), T, T).
:- mode left_of(in, in, in) is semidet.
left_of([A, B | _], A, B).
left_of([_ | List], A, B) :-
left_of(List, A, B).
:- pred next_to(list(T), T, T).
:- mode next_to(in, in, in) is semidet.
next_to(List, A, B) :-
( left_of(List, A, B)
; left_of(List, B, A)
).
:- pred puzzle({list(person), list(person), list(person), list(person),
list(person)}).
:- mode puzzle(out) is nondet.
puzzle({Houses, Colours, Pets, Drinks, Smokes}) :-
% 10. The Norwegian lives in the first house.
First = norwegian,
perm([english, spanish, ukrainian, japanese],
[Second, Third, Fourth, Fifth]),
% 2. The Englishman lives in the red house.
Red = english,
perm([spanish, ukrainian, norwegian, japanese],
[Green, Ivory, Yellow, Blue]),
% 10. The Norwegian lives in the first house.
% 15. The Norwegian lives next to the blue house.
Second = Blue,
% 6. The green house is immediately to the right of the ivory house.
left_of(Houses, Ivory, Green),
% 3. The Spaniard owns the dog.
Dog = spanish,
perm([english, ukrainian, norwegian, japanese],
[Snails, Fox, Horse, Zebra]),
% 4. Coffee is drunk in the green house.
Green = Coffee,
% 5. The Ukrainian drinks tea.
Tea = ukrainian,
% 9. Milk is drunk in the middle house.
Milk = Third,
perm([english, spanish, norwegian, japanese],
[Coffee, Milk, Juice, Water]),
% 7. The Old Gold smoker owns snails.
Snails = OldGold,
% 8. Kools are smoked in the yellow house.
Kools = Yellow,
% 13. The Lucky Strike smoker drinks orange juice.
LuckyStrike = Juice,
% 14. The Japanese smokes Parliaments.
Parliament = japanese,
perm([english, spanish, ukrainian, norwegian],
[OldGold, Kools, Chesterfield, LuckyStrike]),
% 11. The man who smokes Chesterfields lives in the house
% next to the man with the fox.
next_to(Houses, Chesterfield, Fox),
% 12. Kools are smoked in the house next to the house
% where the horse is kept.
next_to(Houses, Kools, Horse),
Houses = [First, Second, Third, Fourth, Fifth],
Colours = [Red, Green, Ivory, Yellow, Blue],
Pets = [Dog, Snails, Fox, Horse, Zebra],
Drinks = [Coffee, Tea, Milk, Juice, Water],
Smokes = [OldGold, Kools, Chesterfield, LuckyStrike, Parliament].
% Printing a solution
:- pred write_solution({list(person), list(person), list(person),
list(person), list(person)}::in, io::di, io::uo) is det.
write_solution({Houses, Colours, Pets, Drinks, Smokes}, !IO) :-
write_string("--------\n", !IO),
write_assignments(["1st", "2nd", "3rd", "4th", "5th"],
Houses, !IO),
write_assignments(["red", "green", "ivory", "yellow", "blue"],
Colours, !IO),
write_assignments(["dog", "snails", "fox", "horse", "zebra"],
Pets, !IO),
write_assignments(["coffee", "tea", "milk", "juice", "water"],
Drinks, !IO),
write_assignments(["oldgold", "kools", "chesterfield",
"luckystrike", "parliament"], Smokes, !IO).
:- pred write_assignments(list(string)::in, list(person)::in,
io::di, io::uo) is det.
write_assignments(Labels, Persons, !IO) :-
foldl_corresponding(write_assignment, Labels, Persons, !IO),
nl(!IO).
:- pred write_assignment(string::in, person::in, io::di, io::uo) is det.
write_assignment(Label, Person, !IO) :-
write_string(Label, !IO),
write_string(" - ", !IO),
write(Person, !IO),
write_string("\n", !IO).
% main
main(!IO) :-
% Print all solutions.
/*
solutions(puzzle, Solutions),
foldl(write_solution, Solutions, !IO).
*/
% Print solutions as they are found.
/*
unsorted_aggregate(puzzle, write_solution, !IO).
*/
% Print one solution.
( if puzzle(Solution) then
write_solution(Solution, !IO)
else
write_string("No solution found.\n", !IO)
).
--------
1st - norwegian
2nd - ukrainian
3rd - english
4th - spanish
5th - japanese
red - english
green - japanese
ivory - spanish
yellow - norwegian
blue - ukrainian
dog - spanish
snails - english
fox - norwegian
horse - ukrainian
zebra - japanese
coffee - japanese
tea - ukrainian
milk - english
juice - spanish
water - norwegian
oldgold - english
kools - norwegian
chesterfield - ukrainian
luckystrike - spanish
parliament - japanese