At Last: A Puzzle!Next Things Next

Armed with all that, we can try some examples. We’ll walk through two examples, and then you can try some on your own. You really have all you need to formulate them correctly: all you lack is the practice.

For a logic puzzle, let’s examine the Four Spies Problem.

You will see that the problem is the usual one for these puzzles, of matching up a list of people against a list of countries and a list of status levels. It is easy to list all three of these as enumerated sorts.

What we want the solver to determine are two functions, assigning to each spy a location and a status. These are declared in the “Vocabulary” box. The functions must have different names from the sorts, so that the solver does not get confused. So “place” and “location” are completely different expressions, for instance. Note that the keyword “function” can be followed by a set of function specifications enclosed in braces. This saves some clutter and tedium but does not affect the meaning.

Each of the functions will be a one-to-one mapping, since no two spies have the same status or are in the same place. This is such a common feature of logic puzzles that there is a special quick way of representing it: in the braces after each function declaration, we write the expression “all_different”, meaning that the function cannot give the same value for any two different arguments. Since the three domains are all the same size, this ensures that the spies are paired with the places and also with the statuses.

Now click on the SOLVE button under the SOLVER.

Notice that some comments have been included in the “Constraints” box. The special character “%” means that any text from there to the end of the line will be disregarded, so you can use it to put in helpful messages to yourself.

Most of the constraints are straightforward. The first one

status(Cuban) > status(Belgian).

for instance, says that the status of the Cuban is better (i.e. comes later in the list of status levels) than the status of the Belgian.

Two of the constraints, however, are worth a closer look. Consider clue 3:

ALL x ( (status(x)=retired) = (location(x)=Greece) ).

This is basically an equation, but it is an equation between two smaller equations. What does this mean? Perhaps the best English reading is

Saying that x has status "retired" is the same thing as saying that x is in Greece.

Look at the parentheses to give you the overall structure of the constraint.