A few weeks ago Sandeep Gor from DigitalVerification launched a challenge for the e-language speakers. The challenge requires solving Einstein’s five house riddle:
Variations of this riddle appear on the internet from time to time. It is sometimes attributed to Albert Einstein and it is claimed that 98% of the people are incapable of solving it. Some commentators suggest that Einstein created such puzzles not to test out intelligence, but to get rid of all the students who wanted him as an adviser. It is not likely that there is any truth to these stories. Wherever this comes from, it is a nice riddle.
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.
- 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 the fish?
Now the problem is on the table, so let’s see how you could solve it using e-language constraint random generation.
Let’s first define the data types we are going to use further on:
<'
type nationality_t : [englishman, swede, dane, norwegian, 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];
'>I need to create a model of the problem. It would be intuitive to encapsulate all those properties (nationality, house, cigar, pet, drink), in a structure like this:
<'
define NUM_OF_MEN 5;
struct man_s {
nationality : nationality_t;
house_color : house_color_t;
cigar : cigarette_t;
pet : pet_t;
drink : drink_t;
};
struct riddle_s {
men : list of man_s;
keep men.size() == NUM_OF_MEN;
keep men.nationality.is_a_permutation(all_values(nationality_t));
keep men.house_color.is_a_permutation(all_values(house_color_t));
keep men.pet.is_a_permutation(all_values(pet_t));
keep men.cigar.is_a_permutation(all_values(cigarette_t));
keep men.drink.is_a_permutation(all_values(drink_t));
};
'>As I need uniqueness for all properties, I’ve used 5 lines of “is_a_permutation”, but the compiler complains about it:
*** Error: GEN_NO_GENERATABLE_NOTIF:
Constraint without any generatable element.
at line 23 in riddle.e
keep men.nationality.is_a_permutation(all_values(nationality_t));
How can I do it differently? My first guess it that I need to trade encapsulation for generation:
<'
struct riddle_s {
nationality[NUM_OF_MEN] : list of nationality_t;
house_color[NUM_OF_MEN] : list of house_color_t;
cigar[NUM_OF_MEN] : list of cigarette_t;
pet[NUM_OF_MEN] : list of pet_t;
drink[NUM_OF_MEN] : list of drink_t;
keep nationality.is_a_permutation(all_values(nationality_t));
keep house_color.is_a_permutation(all_values(house_color_t));
keep pet.is_a_permutation(all_values(pet_t));
keep cigar.is_a_permutation(all_values(cigarette_t));
keep drink.is_a_permutation(all_values(drink_t));
};
'>I created 5 lists instead of one list.
Further on, implementing the constraints is a one liner code, except when I need to constrain neighboring property which takes 3 lines of code.
Since I use e(nglish)-language, it’s easy to understand the constraints I defined below:
<'
extend riddle_s {
keep for each using index (id) in nationality{
it == englishman => house_color[id] == red; //#1
it == swede => pet[id] == dog;//#2
it == dane => drink[id] == tea;//#3
it == norwegian => id == 0;//#9
it == german => cigar[id] == prince;//#13
id in [1..NUM_OF_MEN-2] and it == norwegian => house_color[id+1] == blue or house_color[id-1] == blue;//#14
id == 0 and it == norwegian => house_color[id+1] == blue;//#14
id == NUM_OF_MEN-1 and it == norwegian => house_color[id-1] == blue;//#14
};
keep for each using index (id) in house_color {
it == green => id != NUM_OF_MEN-1;//#4
it == green => house_color[id+1]== white;//#4
it == green => drink[id] == coffee;//#5
it == yellow => cigar[id] == dunhill;//#7
};
keep for each using index (id) in cigar {
it == pall_mall => pet[id] == bird;//#6
id in [1..NUM_OF_MEN-2] and it == blend => pet[id+1] == cat or pet[id-1] == cat;//#10
id == 0 and it == blend => pet[id+1] == cat;//#10
id == NUM_OF_MEN-1 and it == blend => pet[id-1] == cat;//#10
it == blue_masters => drink[id] == bier;//#11
id in [1..NUM_OF_MEN-2] and it == dunhill => pet[id+1] == horse or pet[id-1] == horse;//#12
id == 0 and it == dunhill => pet[id+1] == horse;//#12
id == NUM_OF_MEN-1 and it == dunhill => pet[id-1] == horse;//#12
id in [1..NUM_OF_MEN-2] and it == blend => drink[id+1] == water or drink[id-1] == water;//#15
id == 0 and it == blend => drink[id+1] == water;//#15
id == NUM_OF_MEN-1 and it == blend => drink[id-1] == water;//#15
};
keep for each using index (id) in drink {
it == milk => id == NUM_OF_MEN/2;//#8
};
};
'>Now let’s test my model and see if it is able to find the right solution.
<'
extend sys {
run() is also {
var solution : riddle_s;
var position : int;
gen solution;
position = solution.pet.first_index(it == fish);
messagef(LOW, "Solution is: %s lives in the %s house #%0d, keeps a %s, drinks %s and smokes %s\n",solution.nationality[position], solution.house_color[position], position, solution.pet[position], solution.drink[position], solution.cigar[position]);
};
};
'>I start Incisive 15.10-s005, run the program and the answer is…..german lives in the green house #3, keeps a fish, drinks coffee and smokes prince.
I hope you enjoyed reading this solution as much as I did working on it. I also challenge you to find a better solution since my intuition tells that encapsulation can be improved and the code for neighboring constraints could be reduced to less than 3 lines of code.
[UPDATE – 16-12-2015] Tudor Timisescu, the Verification Gentleman accepted my challenge and improved the solution. He wrote an article about it. You can read it here. Also, you can check out the full code on AMIQ’s GitHub.
7 Responses
Challenge accepted!
One small comment, though. To constrain the neighboring houses you made a small mistake when writing the constraint for houses located in the “middle” (i.e. not at the edges of the neighborhood). It should be something along the lines of:
id in [1..NUM_OF_MEN-2] and (it == norwegian => house_color[id+1] == blue or house_color[id-1] == blue);
You need the brackets in there because ‘and’ has precedence over ‘or’. Because of luck (or most likely other constraints that get solved first), you never “fall off” the list.
Hi, Tudor.
Good to see the challenge was accepted :).
Thanks for the critics, but please notice that in this constraint there is a boolean implication (=>) in between AND and OR, thus there is no need for parentheses. The operator precedence order (“Ch1.4 Operator precedence” in “Specman e Language Reference”) is this: and, or, =>
Cheers,
Aurelian
But shouldn’t
id in [1..NUM_OF_MEN-2] and it == norwegian => house_color[id+1] == blue or house_color[id-1] == blue;
then mean
(id in [1..NUM_OF_MEN-2] and it == norwegian) => (house_color[id+1] == blue or house_color[id-1] == blue);
since ‘and’ and ‘or’ grab operands before the ‘=>’.
Yes, Tudor.
That is exactly my intention. To have it like this:
(id in [1..NUM_OF_MEN-2] and it == norwegian) => (house_color[id+1] == blue or house_color[id-1] == blue);
Which in words translates to this:
“IF the norwegian lives in a house having 2 neighbours then either the neigbour to the left either the neighbour to the right should own a blue house”.
By the way implication operator (=>) can be expanded like this:
exp1 => exp2
is equivalent to
(not exp1) or exp2
I don’t understand the reason for your confusion. What do you think is wrong?
Cheers,
Aurelian
Yep, you’re right. Don’t really know what I was thinking.
You gave up on the encapsulated solution too early. Too bad, because it was a great idea. We can replace the ‘is_a_permutation(…)’ constraints you tried with:
extend neighborhood {
keep men.all_different(it.nationality);
// … for all fields
};
Afterwards, constraints not referencing any neighbors can be added to the ‘man’ struct:
extend man {
keep nationality == englishman => house_color == red; // #1
keep nationality == swede => pet == dog; // #2
// …
};
Fact #4 could be written as a single constraint:
keep for each (man) in men {
man.house_color == green => index
index 0 and men[index-1].pet == cat;
};
Since we need four “neighbor” constraints, we can define a macro for it, which ought to save us some typing:
define ” neighbors ” as {
extend neighborhood {
keep for each (man) in men {
man. => index < 4 and men[index+1]. or
index > 0 and men[index-1].;
};
};
};
I’ll post the full code and more detailed explanations on my site soon.
Tudor,
That’s a tip to remember; this all_different() pseudo-method.
I would be curious to see if even with the macro and a better encapsulation the number of code lines is smaller than my suggested solution.
Regards,
Aurelian