Fun and Games with CRV: The Zebra Puzzle

The Zebra Puzzle is a classic logic puzzle, first published by Life International in 1962. Older versions of it exist and it is also sometimes called Einstein's puzzle. According to "Of Camels and Committees" by Tom Fitzpatrick and Dave Rich, it was used in the early days of constrained random verification (CRV) to show off EDA tools at marketing events.

The puzzle consists of a set of fifteen statements:

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.

(Life International, 1962)

Based on these statements, the reader is asked to deduce who drinks water and who owns the zebra.

Deductive reasoning makes my head hurt, so I want to have the computer solve it for me. As with Sudoku, we don't want to build an algorithm that finds the solution. This is exactly the kind of problem constraint programming is perfect for: expressing logical relations between variables. Let's dive right in!

The first step is to formalize the problem. We know that the houses are of different colors, contain people of specific nationalities that drink some things, smoke some cigarette brands and own some pets, again all different. We will model all of these as enumerations.

First let's handle the house colors:

typedef enum { RED, GREEN, IVORY, YELLOW, BLUE } color_e;

Second, nationality is mentioned:

typedef enum { ENGLISH, SPANISH, UKRANIAN, NORWEGIAN, JAPANESE } nationality_e;

Third, here are the pets:

typedef enum { DOG, SNAILS, FOX, HORSE, ZEBRA } pet_e;

Fourth, this is what the inhabitants like to drink:

typedef enum { COFFEE, TEA, MILK, ORANGE_JUICE, WATER } drink_e;

And fifth, this is what they like to smoke:

typedef enum { OLD_GOLD, KOOL, CHESTERFIELD, LUCKY_STRIKE, PARLIAMENT } cigarettes_e;

The easiest way to model the houses is by using a struct:

typedef struct {
  rand color_e       color;
  rand nationality_e nationality;
  rand pet_e         pet;
  rand drink_e       drink;
  rand cigarettes_e  cigarettes;
} house_t;

The second step is to write the starting statements as constraints. We can't know on which instance of the house to apply a specific statement; this is what we want to find out. The statements must apply to all houses (with the exception of a few that apply to a specific house), which means that for the most part we will write foreach constraints.

Statement 1 just says that there are five houses. This isn't a constraint per se, but more of a modeling topic. We model this by declaring our neighborhood as a vector of houses that contains five elements:

class zebra_puzzle_solver;
  rand house_t house[5];
  
  // ...
endclass

Statement 2 says that the Englishman lives in the red house:

constraint statement2_c {
  foreach (house[i])
    house[i].nationality == ENGLISH -> house[i].color == RED;
}

From statement 3 we learn that the Spaniard owns the dog:

constraint statement3_c {
  foreach (house[i])
    house[i].nationality == SPANISH -> house[i].pet == DOG;
}

Statement 4 tells us that the person who drinks coffee lives in the green house:

constraint statement4_c {
  foreach (house[i])
    house[i].drink == COFFEE -> house[i].color == GREEN;
}

We know from statement 5 that the Ukrainian drinks tea:

constraint statement5_c {
  foreach (house[i])
    house[i].nationality == UKRANIAN -> house[i].drink == TEA;
}

Statement 6 is a bit tricky. It tells us that the green house is immediately to the right of the ivory house. This means that we have to take care in our foreach constraint that we don't end up outside the neighborhood (i.e. access a non-existing location in our vector):

constraint statement6_c {
  foreach (house[i])
    if (i < 4)  // make sure we don't go out of bounds
      house[i].color == IVORY -> house[i+1].color == GREEN;
}

Moving on, statement 7 informs us that the Old Gold smoker owns snails:

constraint statement7_c {
  foreach (house[i])
    house[i].cigarettes == OLD_GOLD -> house[i].pet == SNAILS;
}

At the same time, as per statement 8, the Kools smoker lives in the yellow house:

constraint statement8_c {
  foreach (house[i])
    house[i].cigarettes == KOOL -> house[i].color == YELLOW;
}

Statement 9 only applies to the middle house and says that milk is drunk there:

constraint statement9_c {
  house[2].drink == MILK; // no. 2 is the middle house
}

Statement 10 also only applies to only one house, the first one, and tells us that the Norwegian lives there:

constraint statement10_c {
  house[0].nationality == NORWEGIAN;  // no. 0 is the first house
}

Statement 11 becomes tricky again. From it we know that the Chesterfield smoker lives next to the fox owner. "Next to" means either to the left or to the right. As with statement 6, we have to make sure we don't fall off of the neighborhood map. We have three cases to consider. If he lives in the first house (the leftmost) then this means his neighbor to the right owns the fox. Likewise, if he lives in the last house (the rightmost), this means that his neighbor to the left owns the fox. However, if he lives in one of the middle houses, then either one of his neighbors could potentially own the fox. Expressed as constraints, this would look like this:

constraint statement11_c {
  house[0].cigarettes == CHESTERFIELD -> house[1].pet == FOX;
  house[4].cigarettes == CHESTERFIELD -> house[3].pet == FOX;
  
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].cigarettes == CHESTERFIELD ->
        (house[i-1].pet == FOX) || house[i+1].pet == FOX);
}

Statement 12 is similar to the previous one, but it tells us that the Kools smoker lives next to the horse owner. The constraint looks very much like the one before:

constraint statement12_c {
  house[0].cigarettes == KOOL -> house[1].pet == HORSE;
  house[4].cigarettes == KOOL -> house[3].pet == HORSE;
  
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].cigarettes == KOOL ->
        (house[i-1].pet == HORSE) || house[i+1].pet == HORSE);
}

Statement 13 is simple again and informs us that the Lucky Strike smoker drinks orange juice:

constraint statement13_c {
  foreach (house[i])
    house[i].cigarettes == LUCKY_STRIKE -> house[i].drink == ORANGE_JUICE;
}

Similarly, from statement 14 we find out that the Japanese smokes Parliament:

constraint statement14_c {
  foreach (house[i])
    house[i].nationality == JAPANESE -> house[i].cigarettes == PARLIAMENT;
}

Statement 15 is again more involved, finally telling us that the Norwegian lives next to the blue house. We could type a bit less here (because we know the Norwegian lives in the first house) and directly say that the second house is blue, but I want the constraint solver to work hard for its money. Let's just write the constraint as we did for statements 11 and 12:

constraint statement15_c {
  house[0].nationality == NORWEGIAN -> house[1].color == BLUE;
  house[4].nationality == NORWEGIAN -> house[3].color == BLUE;
  
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].nationality == NORWEGIAN ->
        (house[i-1].color == BLUE) || house[i+1].color == BLUE);
}

Ideally, the third step should be to just run our code and find the solution, but as always nothing works right on the first try. I kept getting some very weird results at first, that were completely off. The reason for this is that we used implication constraints. Saying that being English implies you live in the red house is not enough. We don't know the order in which fields are assigned by the solver, so we also need to say that if you live in the red house, then you are English. Luckily, SystemVerilog provides us the equivalence operator <->. Here's how the constraint for statement 2 should really look like:

constraint statement2_c {
  foreach (house[i])
    house[i].nationality == ENGLISH <-> house[i].color == RED;
}

For brevity I won't show all of the fixed constraints here.

Even with the equivalence constraints in place, I got three Japanese and two Norwegians in my neighborhood. I looked at each of the constraints and they all applied (though some vacuously). The last one, however (the one I chose to write long), didn't, but only because the compiler had no problem with me saying that the Norwegian lives next to the house with the color fox (you won't see it in the code I posted as I already fixed that).  Surprisingly, there was no error, no warning, no nothing, even though such a conversion is illegal. Let this be a lesson to us for the future: some simulators are a bit more relaxed with their interpretation of the SystemVerilog standard and we need to make sure to enforce strict LRM compliance, otherwise we're going to have a bad time debugging implicit type conversions.

Even after fixing the foxy house, I still got a neighborhood full of Norwegians with all blue houses. Three of them smoked Chesterfields, while the other two liked Old Gold (and had snails as well, of course). Most drank milk and only one drank water. Also, the middle guy had the zebra. You get the idea, something was still missing. Well, the wording of the puzzle is important. It always said "the Norwegian..." or "the Lucky Strike smoker..." which means there is only one Norwegian and only one Lucky Strike smoker. The original article in Life International adds this fact as a clarification: "[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]."

To reflect this, we just need to add a uniqueness constraint. Unfortunately, because constraint operands have to be of integral types, we can't just say that the houses are unique. We have to declare auxiliary lists for nationalities, pets, etc. and constrain these to be unique. In e we could have accessed these directly, without the need for extra fields, but here is how it looks like in SystemVerilog:

local rand color_e       color[5];
local rand nationality_e nationality[5];
local rand pet_e         pet[5];
local rand drink_e       drink[5];
local rand cigarettes_e  cigarettes[5];

constraint create_sublists_c {
  foreach (house[i]) (
    color[i] == house[i].color &&
    nationality[i] == house[i].nationality &&
    pet[i] == house[i].pet &&
    drink[i] == house[i].drink &&
    cigarettes[i] == house[i].cigarettes
  ); 
}

constraint all_unique_c {
  unique { color };
  unique { nationality };
  unique { pet };
  unique { drink };
  unique { cigarettes };
}

Even with the uniqueness constraint in place, we still get a contradiction error. This one took me a bit to figure out. The problem is with our "complicated" constraints (the ones for statements 11, 12 and 15). Here is how the constraint for statement 11 looks after swapping implication for equivalence, in particular the constraint for the middle houses:

constraint statement11_c {
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].cigarettes == CHESTERFIELD <->
        (house[i-1].pet == FOX) || house[i+1].pet == FOX);
}

The mistake is with respect to the relation between the equivalence and logical operators. Let's take a step back and let me explain what I mean by that. For the case of implication, the following is true:

a -> (b || c) == (a -> b) || (a -> c)

The same is however not true for equivalence:

a <-> (b || c) != (a <-> b) || (a <-> c)

For all of you math enthusiasts, this means that equivalence is not distributive over disjunction. If you write the truth tables you will see that this is the case. What we're interested in is the right hand side of the expression (the neighbor on the left smokes Chesterfields or the neighbor on the right smokes Chesterfields), but what we have implemented is the expression on the left hand side. Now that we know this, we can fix the constraints (shown for statement 11):

constraint statement11_c {
  foreach (house[i])
    if (i > 0 && i < 4)
      (house[i].cigarettes == CHESTERFIELD <-> house[i-1].pet == FOX) ||
      (house[i].cigarettes == CHESTERFIELD <-> house[i+1].pet == FOX);
}

Technically, more correct would have been to say A <-> B xor A <-> C, because the neighbor can only be either on the left or on the right. This might speed things up a bit and might also make it so that uniqueness constraints are not needed. Unfortunately, we can't try this out as there is no logical exclusive "or" operator in SystemVerilog.

After fixing this last thing, everything now works! We find out that the Norwegian drinks water and that the Japanese owns the zebra. Much easier than deductive reasoning...

I hope you enjoyed this post. It was a lot of fun to make and I learned a bit more about the constraint capabilities of SystemVerilog. If you want to play with the solver, you can download it from SourceForge.

Stay tuned for more fun and games with CRV!