Common KnowledgeMore Advanced Topics

Our example on this page is the Jobs Puzzle which has (for no especially good reason) been a standard problem for automatic theorem-proving programs for many years. As it dates from another millennium, and is written in the language of its time, we have to apply a little charity in interpretation. The SOLVER on the side has been set to point to it.

At first glance, there appear to be just five clues, plus maybe a little tricky logic to say that each person has two jobs. On closer examination, however, we see that in order to get a single solution out of these five, we have to use a lot of background assumptions which are not stated explicitly.

For one thing, much of the reasoning turns on who is male and who is female. We are supposed to know that Pete and Steve are male while Thelma and Roberta are female. Moreover, the puzzle requires the binary gender assumption that to be male is to fail to be female. All of this has to be made explicit for the problem encoding to work. It may seem that the first constraint, saying that the males are just the non-females, is redundant given the listing of who is male and who is female, but it is not. If you try removing it, you will see that you get solutions in which Pete is both male and female, and takes advantage of this by marrying herself.

The function “husband_of” is interesting. We are supposed to supply the information that if x is the husband of y, then x is male and y is female (that is how this function interacts with the rest of the setup to influence the possible solutions). The absence of same-sex marriages is not universally true, but is something we go along with for the purposes of this puzzle, as it is a classic and dates from ancient times. Not everyone has a husband of course. So “husband_of” is a partial function, not just because it sometimes takes us off the edge of the map, like “+”, but because for certain cases it really isn’t defined. It is also “all_different” (no two people can have the same husband, at least in the world of this puzzle) but it is not a one-to-one mapping of the “person” sort onto itself because there are people who are not anybody’s husband (Thelma is not a husband, for instance).

We also need to know what is the significance of Pete’s lack of education. In my suggested representation I have made “educated” an all-or-nothing affair, since there seems to be no need to bother with fine details like exactly which grade people reached. Education matters because teachers, nurses and police officers have to be educated past ninth grade. This also is not a necessary truth, but is something everybody knows.

The game of golf is of course irrelevant. The point of the fifth clue is simply that all three of the golfers are different people. Make sure you see how this is said logically. You should also check that you understand the constraints relating the functions “job1” and “job2” to the relation “is_a”. The one that says job1(x) comes before job2(x) is only there because the two jobs have to come in one order or the other – if you don’t see the point, try deleting that constraint and clicking on SOLVE.

Finally, the trick constraint required to get the solutions down to just one is that the waiter is male (female ones are “waitresses” apparently).

Like most of the puzzles in these pages, the Jobs Puzzle is artificial, but what goes for such “toy” problems as this goes double for problems in the real world. Taking account of background assumptions is one of the most important and most difficult aspects of mathematical modelling. Sometimes it is a simple matter of enforcing obvious conditions like saying that a dwarf cannot have a negative number of coins (i.e. gold hoards are not like bank accounts) but sometimes the issues are quite tricky. Things become especially interesting when the logical modelling exposes a background assumption which may be natural but may also be false!