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:

1. There are five houses.
2. The Englishman lives in the red house.
3. The Spaniard owns the dog.
4. Coffee is drunk in the green house.
5. The Ukrainian drinks tea.
6. The green house is immediately to the right of the ivory house.
7. The Old Gold smoker owns snails.
8. Kools are smoked in the yellow house.
9. Milk is drunk in the middle house.
10. The Norwegian lives in the first house.
11. The man who smokes Chesterfields lives in the house next to the man with the fox.
12. Kools are smoked in the house next to the house where the horse is kept.
13. The Lucky Strike smoker drinks orange juice.
14. The Japanese smokes Parliaments.
15. 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.

Data representation

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.

Generating permutations

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]
    ).

Houses

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.

Colours

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),

Pets

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]),

Drinks

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.

Smokes

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),

Putting it together

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.

Collecting all solutions

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.

Finding a single 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.

Printing solutions as they are found

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.

Source code

:- 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)
    ).

Program output

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