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

How many ways are there to solve a problem?

popularity

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!



5 comments

Ferdinando Pace says:

Dear Sergio,

Can you explain why the milk drinker constrained to be in the wrong house was not detected by the ONESPIN verification tool ?

The original criteria for winning the competition was the fastest executing solution. However all ten of these entries ran at about the same speed.

Why did the ONESPINformal verification not find the bug in one of the 4 winning solutions ? is a visual inspection required ?
Thanks in advance for your answer.
Regards,
Ferdinando

Ferdinando Pace says:

Dear Sergio,
Sorry for late and thanks a lot for your clear answer . I appreciate!
Have a nice day!
Ferdinando

Sergio Marchese says:

Hello Ferdinando,

I appreciate your question, which I unfortunately did not see until today. Thank you for your patience.

Solution 2 was written using the e language ( https://en.wikipedia.org/wiki/E_(verification_language) ), which is used to build simulation test benches for the Specman tool. I know that the solution was wrong because of the excerpt from the Specman log file that the author included. Although it didn’t quite meet the rules for the contest, with the permission of all the respondents, we included it as we thought it an elegant solution to the problem, and one that people could learn from. I did not have the Specman tool available, so I could not actually run Solution 2. Nevertheless, I did take a look at it and noted a potential problem in the code.

OneSpin is a formal verification tool and, like all other formal verification tools, does not support the e language. As such, we could not run it with the OneSpin tool. Had it been runnable, we would have seen the problem for sure. OneSpin DV-Verify supports the SystemVerilog and PSL assertion languages, as well as all the various versions of Verilog, SystemVerilog, and VHDL for designs. We can even support C++ and SystemC—our direct competitors can’t. 🙂

I hope that answers your question, and thanks again for engaging with us here!

– Sergio

Humera Ahsanullah says:

What do you mean 98% couldn’t solve? I solved it in one go go so I’m among the 2%? I’m not sure this is any hard puzzle or Einstein’s puzzle.

Peter Kornis says:

I am a (chip design) back-end engineer at Winbond. During the Corona lock-down at home, I decided to learn Python.
I wrote a ~250 line Python code that exhaustively generates all possible combinations and using the problem constraints, by elimination, leaves only one correct solution. Indeed the german and all house placement constraints are satified

Leave a Reply


(Note: This name will be displayed publicly)