And The Winners Are… 10 Formal Solutions To Einstein’s Riddle

A few months back, OneSpin asked engineers to solve the classic Einstein’s Riddle using a formal tool. The challenge became hugely popular, and we received many outstanding solutions. To check out the riddle itself and the top 10 solutions created by leading engineers, click here.

In this blog, we take another look at the riddle, review the best solutions and announce the winners.

We have no evidence, but legend has it that Einstein wrote his famous riddle as a boy, a riddle that 98% of the world population could not solve. Initially, I tried keeping track of the variables in my mind without notes and failed miserably.

With the help of paper and pencil, I constructed a table showing which national lived in each house, along with the rest of the permutations, and with time and patience, found the solution: The German owned the fish. I then spent time reviewing the table to make sure it satisfied all the riddle’s requirements. As I enjoyed what I thought was my well-deserved coffee, a doubt came to my mind: How could I be sure that I found the solution and not just a solution?

I am not the tidiest person, so trying to review my notes to retrace the steps that got me to the solution was not easy. I have no shame, just a little embarrassment, in confessing that a Google search revealed the answer.

Looking at one of the results coming from a reputable source, I found a discussion about orientation, which opened a can of worms. There are five houses in the game, which I had conveniently tagged with numbers from zero to four. The riddle states that the Norwegian lives in the first house, and I had assumed that the first house was number zero. Would anything change if it were number four? I guessed the result should not be affected, but I would rather have proof before betting on it. Even more unsettling, the riddle states that the green house is on the left of the white house. I had pictured “the left” to mean “my left.” What would happen if the observer were facing the opposite side? My left would actually be right.

It still amazes me to realize how ambiguous English can be and how many intriguing questions even a relatively simple (compared to modern hardware design) problem can generate. The time had come to put aside paper and pencil and open my laptop; after all, I was fortunate enough to have the OneSpin Formal Tool icon on my Windows desktop and the wisdom to apply it to these questions.

Luckily, engineers enjoy a good challenge, and when OneSpin proposed the creation of a formal solution to Einstein’s Riddle, there were many submissions. We selected the 10 best and let the community vote for their favorites. With these solutions at my disposal, I dispensed with reinventing the wheel and used my favorite.

Darren Galpin from Infineon submitted a solution using Specman ‘e’ language. The solution looked neat, and in fact was ranked among the top three in votes. However, it had two problems: The result was incorrect –– perhaps due to a typo on the milk drinker constrained to be in the wrong house –– and the use of ‘e’ did not fit the competition rules.

Johan Wouters from ICsense and Phani Kumar Peri from Infineon submitted two high-ranking solutions using VHDL/PSL and VHDL/ITL, respectively. In the last few years, my VHDL to Verilog time ratio has been around one to 10. Having the option, I passed on VHDL. Fortunately for me, Anthony Wood from Imagination Technologies, Ferdinando Pace of Sensirion, Verilab’s Jonathan Bromley, Laurent Arditi at ARM, Wolfgang Roessel of Nokia, Steve Holloway from Dialog Semiconductors, and Infineon’s Tudor Timisescu submitted beautifully coded SystemVerilog solutions.

I wanted to pick a short and readable solution and, frankly, it was not an easy choice. Finally, I went for Tudor’s that, to my great surprise, was not in the top four (although it did well). Clearly, personal preferences play a significant role in coding!

OneSpin’s DV-Verify running Wolfgang Roessel’s solution to Einstein’s Riddle.

After compiling and running Tudor’s solution in OneSpin’s DV-Verify, and before modifying it to examine other interpretations of the riddle, I reviewed his code more carefully. To my surprise, I found a typical copy-paste bug. The last assumption (STATEMENT_15) appeared incorrect, but Tudor had been lucky: Not once, but twice. First, the wrong assumption was not illegal, but merely redundant, as it was the exact copy of a previous one with a different name. Second, as it turned out, the assumption in its correct form was not needed to solve the puzzle.

This raised a new question: Did I need all of the hints in the riddle to find the (unique) solution? With the help of the formal tool, I found that the only redundant hint was the last one: “The man who smokes blend has a neighbor who drinks water.” This deserved a little more attention. Analyzing it carefully, I noted that it did not use the expression “next to.” Nevertheless, all 10 solutions had interpreted it as if it did. I thought, engineers are a social bunch and a neighbor is someone living near you, not just your next-door neighbor. I therefore choose to take the safe side and interpret it as, “The man who smokes blend lives somewhere near the one who drinks water.” Interestingly, the solution didn’t change, as one would expect when a redundant constraint is relaxed.

As it turned out from my experiments, the German was resilient in keeping her fish, but other attributes were prone to change. For example, she became flexible in picking the house she lived in. I still had many questions, but the final blow to my efforts came when I noted that the tool was telling me that the English person was drinking milk. My boss, the competition’s originator, is from England, and no EDA tool could convince me that he would pick milk when beer was in the game. Something was fundamentally wrong and it was not worth continued reasoning.

If you got here, thank you for reading through my ramblings and an even bigger thank you to all the participants. Reviewing these different and elegant solutions to the same problem was a great learning opportunity.

Finally, here are the winners! The four most-voted solutions to the OneSpin’s Einstein’s riddle were:

1. Nokia’s Wolfgang Roessel
2. Darren Galpin from Infineon
3. Laurent Arditi at ARM
4. Phani Kumar Peri of Infineon

You’ll notice that we added an extra prize. Although Darren’s solution did not quite get the right answer due to a typo, it was elegant and received a high number of well-deserved votes.

The top 10 participants received a mini drone as a special thank you for their excellent submissions. Winners will get a second, much larger flying machine equipped with a camera. Congratulations, and have fun with your new drones, but don’t use them to check on your neighbors’ drinking habits. We at OneSpin had fun with this challenge, and, looking at how many engineers got involved, it seems that you did, too. Stay tuned –– more is in store!