Over
the weekend, I came across this riddle and thought of solving it using ‘e’.
Later on I challenged our team members over the WhatsApp and they took up the
challenge. They came up with their version of solution in SV and SVA. I thought of sharing this solution to show how constraints solver
engine can solve these kind of riddles. During the course of
solution, I observed specifics about constraint solving technology of Specman. But before that, let’s
look at the riddle. It is called with different names like Zebra Riddle or
Einstein’s Riddle. This riddle has different version of stories and none of it
has any solid proof to prove its origin. I’ve taken this riddle from one of the
student’s home
page from Stanford University website. Here is his version of the riddle
which we tried to solve.
Let
us assume that there are five houses of different colors next to each other on
the same road. In each house lives a man of a different nationality. Every man
has his different favorite drink, his different favorite brand of cigarettes,
and keeps different pets of a particular kind.
- The
Englishman lives in the red house.
- The
Swede keeps dogs.
- The
Dane drinks tea.
- The
green house is just to the left of the white one.
- The
owner of the green house drinks coffee.
- The
Pall Mall smoker keeps birds.
- The
owner of the yellow house smokes Dunhills.
- The
man in the center house drinks milk.
- The
Norwegian lives in the first house.
- The
Blend smoker has a neighbor who keeps cats.
- The
man who smokes Blue Masters drinks bier.
- The
man who keeps horses lives next to the Dunhill smoker.
- The
German smokes Prince.
- The
Norwegian lives next to the blue house.
- The
Blend smoker has a neighbor who drinks water.
The question to
be answered is: Who keeps fish?
Now to solve this riddle, I started thinking these clues as
constraints in ‘e’. Let’s go step by step how I approached this problem.
Here, we have 5 men who has different characteristics like
they live in specific house number which has specific color. Each one has
unique nationality, favorite drink, favorite brand of cigarettes and pet. So,
based on these attributes, we can create a struct which can have these 5
attributes. These five attributes can be enumerated and ‘man’ struct can be
defined as shown below.
type nationality_t : [english, swede, dane,
norweigian, german];
type house_color_t : [red, green, yellow, blue,
white];
type cigarette_t : [dunhill, blend, blue_masters,
prince, pall_mall];
type pet_t : [dog, bird, cat, horse, fish];
type drink_t : [tea, coffee, milk, bier, water];
struct man {
nationality : nationality_t;
house_color : house_color_t;
cigarette : cigarette_t;
pet : pet_t;
drink : drink_t;
};
Here, I’ve not captured the house number as an attribute
since I thought I can create list of struct which automatically will fix the
house number of each object.
Now, I’ve categorized the clues in 2 category. One category
which does not have house number order dependency and the other category which
has house number dependency. Like, clue number 1 “The Englishman lives in red
house” does not have any reference to the number of house, whereas clue no. 4
“The gree house is just to the left of the white one” has reference to the
house number order. Since I have not captured the house number as an attribute,
I’ve to split the clues into two different categories of constraints. One
without the reference of the house number can be part of the original struct
definition. One with the house number dependency can go to the place where list
of struct is created so that we have notion of the house orders using index
number of the list.
Let’s first capture the clues without house number ordering
as global constraints as part of struct declaration. Here is what I’ve
captured.
extend man {
//Englishman lives in
the red house
keep nationality ==
english => house_color == red;
//Swede keeps dog
keep nationality ==
swede =>
pet == dog;
//dane drinks tea
keep nationality ==
dane =>
drink == tea;
//owner of the green
house drinks coffee
keep house_color ==
green =>
drink == coffee;
//Pall Mall smoker
keeps bird
keep
cigarette == pall_mall =>
pet == bird;
//owner of the yellow
house smokes dunhill
keep house_color ==
yellow => cigarette ==
dunhill;
//Man who smokes Blue
Masters drinks bier
keep
cigarette == blue_masters =>
drink == bier;
//German smokes
prince
keep nationality ==
german => cigarette ==
prince;
};
Now let’s move on to declaring this struct as 5 objects as
shown below.
extend sys
{
men : list of man;
keep men.size() == 5;
};
Now over here, we can capture the clues with house number
ordering as different constraints involving different objects. Here, we’ll go
by clues.
Let’s look at the first constraint which has dependency on
the house number ordering. This clue is clue number 4 “The green house is just
to the left of the white one”. This can be captured as shown below. Here I’ve
assumed house numbers starts from 0 to 4 runs from left to right. Due to this
assumption, house number 0 does not have any house on left side of it.
extend sys {
//The green house is just to the left
of the white one.
keep men[1].house_color == white =>
men[0].house_color == green;
keep men[2].house_color == white =>
men[1].house_color == green;
keep men[3].house_color == white =>
men[2].house_color == green;
keep men[4].house_color == white =>
men[3].house_color == green;
};
Next clue which has dependency on the house number ordering
is clue number 8 “The man in the center house drinks milk”. This can be
captured easily as we know the house number 2 is in center.
extend sys {
//The man in the center house drinks
milk.
keep
men[2].drink == milk;
};
Next such clue is clue number 9 “The Norwegian lives in the
first house”. Again it is simple to capture.
extend sys {
//Norweigian lives in the first house
keep men[0].nationality == norweigian;
};
Next such clue is clue number 10 “The Blend smoker has a
neighbor who keeps cats”. This is how I captured it. It is obvious that man
staying in house 0 or 4 have only one neighbor and rest men have 2 neighbour.
extend sys {
//The Blend smoker has a neighbor who
keeps cats.
keep
men[0].pet == cat
=> men[1].cigarette == blend;
keep
men[1].pet == cat => men[0].cigarette
== blend or men[2].cigarette == blend;
keep
men[2].pet == cat =>
men[1].cigarette == blend or men[3].cigarette == blend;
keep
men[3].pet == cat =>
men[2].cigarette == blend or men[4].cigarette == blend;
keep men[4].pet
== cat => men[3].cigarette == blend;
};
Next clue is clue number 12 “The man who keeps horses lives
next to the Dunhill smoker”. Again it is captured just like the above
constraints for clue number 10.
extend sys {
//The man who keeps horses lives next
to the Dunhill smoker.
keep
men[0].pet == horse =>
men[1].cigarette == dunhill;
keep
men[1].pet == horse =>
men[0].cigarette == dunhill or men[2].cigarette == dunhill;
keep
men[2].pet == horse =>
men[1].cigarette == dunhill or men[3].cigarette == dunhill;
keep
men[3].pet == horse =>
men[2].cigarette == dunhill or men[4].cigarette == dunhill;
keep
men[4].pet == horse =>
men[3].cigarette == dunhill;
};
Next clue in this category is clue number 14 “The Norwegian
lives next to the blue house”. Since it is already declared in clue
number 9 “The Norwegian lives in the first house”, it is obvious that the blue
house is house number 1. The Here is how I’ve captured it.
extend sys {
//The Norwegian lives next to the blue
house.
keep men[1].house_color == blue;
};
If we do not want to capture it by interpreting it by
ourselves and want tool to interpret for us, we can capture it just like we
captured clue number 10 and 12. Here is how clue number 14 can be captured in
alternate way.
extend sys {
//The Norwegian lives next to the blue
house.
keep men[0].nationality == norweigian
=> men[1].house_color == blue;
keep men[1].nationality == norweigian
=> men[0].house_color == blue or men[2].house_color == blue;
keep men[2].nationality == norweigian
=> men[1].house_color == blue or men[3].house_color == blue;
keep men[3].nationality == norweigian
=> men[2].house_color == blue or men[4].house_color == blue;
keep men[4].nationality == norweigian
=> men[2].house_color == blue or men[4].house_color == blue;
};
Last clue that is clue number 15 “The Blend smoker has a
neighbor who drinks water” is again captured the way we have captured clue
number 10 and 12.
extend sys {
//The Blend smoker has a neighbor who
drinks water.
keep men[0].cigarette ==
blend => men[1].drink == water;
keep men[1].cigarette ==
blend => men[0].drink == water or men[2].drink == water;
keep men[2].cigarette ==
blend => men[1].drink == water or men[3].drink == water;
keep men[3].cigarette ==
blend => men[2].drink == water or men[4].drink == water;
keep men[4].cigarette ==
blend => men[3].drink == water;
};
Now we have captured all the clues as constraints. But when
we load this file into Specman and try to solve it, we get constraint error.
The reason is that we have not capture an important piece of information into
this solution, that is each man has unique values of each 5 attributes. Now
capturing this and informing Specman to generate uniq values for all 5 objects
of man struct is bit tricky in ‘e’. In system Verilog, randc operator helps us
capture it very easily, but in ‘e’ we have to do it with lot of codes. Here is
how I’ve done it.
extend sys {
//Let us assume that there are five
houses of different colors next to each other on the same road. In each house
lives a man of a different nationality. Every man has his favorite drink, his
favorite brand of cigarettes, and keeps pets of a particular kind.
//Unique nationality, house_color,
cigarette, pet and drink
keep men[0].nationality !=
men[1].nationality;
keep men[0].nationality !=
men[2].nationality;
keep men[0].nationality !=
men[3].nationality;
keep men[0].nationality !=
men[4].nationality;
keep men[0].house_color !=
men[1].house_color;
keep men[0].house_color !=
men[2].house_color;
keep men[0].house_color !=
men[3].house_color;
keep men[0].house_color !=
men[4].house_color;
keep men[0].cigarette !=
men[1].cigarette;
keep men[0].cigarette !=
men[2].cigarette;
keep men[0].cigarette !=
men[3].cigarette;
keep men[0].cigarette !=
men[4].cigarette;
keep
men[0].pet != men[1].pet;
keep
men[0].pet != men[2].pet;
keep
men[0].pet != men[3].pet;
keep
men[0].pet != men[4].pet;
keep
men[0].drink != men[1].drink;
keep
men[0].drink != men[2].drink;
keep
men[0].drink != men[3].drink;
keep
men[0].drink != men[4].drink;
keep men[1].nationality !=
men[2].nationality;
keep men[1].nationality !=
men[3].nationality;
keep men[1].nationality !=
men[4].nationality;
keep men[1].house_color !=
men[2].house_color;
keep men[1].house_color !=
men[3].house_color;
keep men[1].house_color !=
men[4].house_color;
keep men[1].cigarette !=
men[2].cigarette;
keep men[1].cigarette !=
men[3].cigarette;
keep men[1].cigarette !=
men[4].cigarette;
keep
men[1].pet != men[2].pet;
keep
men[1].pet != men[3].pet;
keep
men[1].pet != men[4].pet;
keep
men[1].drink != men[2].drink;
keep
men[1].drink != men[3].drink;
keep
men[1].drink != men[4].drink;
keep men[2].nationality !=
men[3].nationality;
keep men[2].nationality != men[4].nationality;
keep men[2].house_color !=
men[3].house_color;
keep men[2].house_color !=
men[4].house_color;
keep men[2].cigarette !=
men[3].cigarette;
keep men[2].cigarette !=
men[4].cigarette;
keep
men[2].pet != men[3].pet;
keep
men[2].pet != men[4].pet;
keep
men[2].drink != men[3].drink;
keep
men[2].drink != men[4].drink;
keep men[3].nationality !=
men[4].nationality;
keep men[3].house_color !=
men[4].house_color;
keep men[3].cigarette !=
men[4].cigarette;
keep
men[3].pet != men[4].pet;
keep
men[3].drink != men[4].drink;
};
Now we are ready to solve it. Let’s add some debug and
solution print statements.
extend {
post_generate() is also
{
for i from 0 to 4 {
outf ("\n");
outf ("men[%d].nationality = %s\n", i, men[i].nationality);
outf ("men[%d].house_color = %s\n", i, men[i].house_color);
outf ("men[%d].cigarette = %s\n", i,
men[i].cigarette );
outf ("men[%d].pet =
%s\n", i, men[i].pet );
outf ("men[%d].drink = %s\n", i,
men[i].drink );
};
outf
("===================================\n");
for i from 0 to 4 {
if
(men[i].pet == fish)
{
outf ("\nAnswer to the quesiton 'Who keeps fish?' is %s who lives in house
no %d with house color %s and smokes %s and drinks %s has %s as pet...\n",
men[i].nationality, i, men[i].house_color, men[i].cigarette, men[i].drink,
men[i].pet);
outf ("\n");
outf ("men[%d].nationality = %s\n", i, men[i].nationality);
outf ("men[%d].house_color = %s\n", i, men[i].house_color);
outf ("men[%d].cigarette = %s\n", i,
men[i].cigarette );
outf ("men[%d].pet =
%s\n", i, men[i].pet );
outf ("men[%d].drink = %s\n", i,
men[i].drink );
};
};
}; //post_generate() is also
}; //extend sys
After loading it into Specman and solving it, we get
following output.
Loading einsteins_puzle.e ...
Doing setup ...
Generating the test with IntelliGen using seed
1966611192...
men[0].nationality = norweigian
men[0].house_color = yellow
men[0].cigarette = dunhill
men[0].pet
= cat
men[0].drink =
water
men[1].nationality = dane
men[1].house_color = blue
men[1].cigarette = blend
men[1].pet
= horse
men[1].drink =
tea
men[2].nationality = english
men[2].house_color = red
men[2].cigarette = pall_mall
men[2].pet
= bird
men[2].drink =
milk
men[3].nationality = german
men[3].house_color = green
men[3].cigarette = prince
men[3].pet
= fish
men[3].drink =
coffee
men[4].nationality = swede
men[4].house_color = white
men[4].cigarette = blue_masters
men[4].pet
= dog
men[4].drink =
bier
===================================
Answer to the quesiton 'Who keeps fish?' is german
who lives in house no 3 with house color green and smokes prince and drinks
coffee has fish as pet...
men[3].nationality = german
men[3].house_color = green
men[3].cigarette = prince
men[3].pet
= fish
men[3].drink =
coffee
Starting the test ...
Running the test ...
No actual running requested.
Checking the test ...
Checking is complete - 0 DUT errors, 0 DUT warnings.
So the answer is “German keeps the Fish”. Now try to solve
this solution multiple times with random seed and you will get the same answer.
That way we can be sure that the constraints we’ve captured are correct.
One last observation I’ve made is that this solution can be
solved in IntelliGen Specman solver only. It does not work with PGen Specman
solver engine. The reason is quiet obvious. PGen depends on the order of
constraints declaration whereas IntelliGen is truly bi-directional constraints
solver which is natural way of solving all the constraints at the same time.
Hope you like this riddle and the solution. I am sure this
is not the optimal way of solving the problem, but it’s my lazy weekend stuff,
so I wrote whatever came to my mind first without thinking much about
optimizing it. If you have any suggestion to improve it, please do comment. If
you have solutions in other forms (XLS, Perl, tcl, python, C, C++, VB, PHP or
any other your favorite language) then please do post it in the comment.