系统与设计
的意见

和获奖者是…10正式解决爱因斯坦的谜题

有多少方式解决问题吗?

受欢迎程度

几个月前,OneSpin问工程师解决经典爱因斯坦的谜题使用一个正式的工具。挑战成为广受欢迎的,我们收到了很多优秀的解决方案。检出谜题本身和前十的解决方案由领先的工程师,点击这里

在这个博客中,我们来看另一个谜题,复习最好的解决方案宣布获胜者。

我们没有证据,但传说爱因斯坦写了他著名的谜题作为一个男孩,一个谜题,98%的世界人口也解决不了。最初,我试着跟踪变量在我脑海中没有笔记和失败。

纸和铅笔的帮助下,我构建了一个表显示哪个国家住在每个房子,其余的排列,时间和耐心,找到了解决方案:德国拥有鱼。然后我花时间检查表,以确保它满足所有谜题的要求。我喜欢什么我认为是当之无愧的咖啡,一个疑问来到我的脑海:我怎么能确保我找到解决方案,而不是一个解决方案呢?

我不整洁的人,所以努力复习我的笔记追溯解决方案让我的步骤并不容易。我没有遗憾,只是有点尴尬,在承认谷歌搜索显示的答案。

观察的结果来自有信誉的来源,我找到了一个讨论取向打开一罐蠕虫。在游戏中有五个房子,我有方便标记数字从0到4。谜语,挪威人住在第一个房子,,我曾以为,第一个房子是数字零。如果是4号会有改变?我猜结果应该不会受到影响,但我宁愿赌之前的证据。更令人不安的是,谜语州温室在离开白宫。我有见“左”的意思是“我的离开。“如果观察者面临对面吗?我的离开会是正确的。

它还使我认识到如何和模棱两可的英语多少有趣的问题甚至是一个相对简单的(相对于现代硬件设计)可以生成问题。时间来放下纸笔,打开我的笔记本电脑;毕竟,我是幸运的OneSpin正式的工具图标在我的Windows桌面和智慧应用到这些问题。

幸运的是,工程师们享受一个好挑战,当OneSpin提议建立一个正式的解决方案爱因斯坦的谜题有许多意见。我们选择十佳,让社区投票给他们的最爱。这些解决方案在我处置,我抛开了重新发明轮子和使用我的最爱。

达伦Galpin从英飞凌提交解决方案使用Specman“e”语言。解决方案看起来整洁,事实上排名前三名的选票。然而,它有两个问题:结果是错误的——或许是由于一个错字牛奶喝限制错误的房子,“e”的使用不符合比赛规则。

约翰伍特斯ICsense和Phani Kumar仙女英飞凌提交两个高级解决方案使用硬件描述语言(VHDL) / PSL和硬件描述语言(VHDL) / ITL,分别。在过去的几年里,我的硬件描述语言(VHDL) Verilog时间比已经存在1到10。有选择,我通过硬件描述语言(VHDL)。从想象力对我来说幸运的是,安东尼木材技术,并且发展速度Sensirion, Verilab的乔纳森•布罗姆利Laurent Arditi在手臂,沃尔夫冈•罗塞尔的诺基亚,从对话框中半导体史蒂夫·霍洛韦,英飞凌的都铎Timisescu提交编码SystemVerilog精美的解决方案。

我想选择一个短的和可读的解决方案,坦率地说,这不是一个容易的选择。最后,我去都铎王朝的让我大为吃惊的是,并不是在四大(尽管它做得很好)。显然,个人喜好扮演了一个重要的角色在编码!


OneSpin DV-Verify运行沃尔夫冈•罗塞尔对爱因斯坦的谜题的解决方法。

在编译和运行都铎式的解决方案OneSpin的DV-Verify在修改之前,检查其他解释的谜题,我更仔细地回顾他的代码。令我惊奇的是,我发现了一个典型的复制粘贴错误。最后一个假设(STATEMENT_15)出现错误,但都铎王朝已经幸运了:不是一次,而是两次。首先,错误的假设并不违法,而仅仅是多余的,因为它是精确地复制前一个不同的名称。第二,事实证明,其正确形式的假设是不需要来解决这个难题。

这提出了一个新的问题:我需要所有谜语的提示找到(独特的)解决方案?正式的工具的帮助下,我发现唯一多余的提示是最后一个:“抽烟的人混合有邻居喝水。“这更值得重视。仔细分析,我注意到它没有使用表达式”旁边。“然而,所有10个解决方案已经解释它,就好像它了。我想,工程师们是一群社会的人,一个邻居是住在你附近的人,而不仅仅是你的邻居。因此我选择安全可靠并解释它,“抽烟的人住附近喝水的人。“有趣的是,解决方案并没有改变,正如预期的那样,当一个冗余约束放松。

从我的实验结果,德国是弹性保持她的鱼,但是其他属性是容易改变。例如,她变得灵活挑选房子她住在。我仍然有很多问题,但最终的打击我的努力时我注意到该工具告诉我,英国人喝牛奶。我的老板,竞争的发起者,来自英格兰,EDA工具无法说服我,他会拿牛奶当啤酒游戏。东西是根本错误的,这是不值得继续推理。

如果你在这里,谢谢你阅读我的乱七八糟的,一个更大的感谢所有的参与者。回顾这些不同和优雅的解决同样的问题是一个很好的学习机会。

最后,这是赢家!四大家最想解决OneSpin的爱因斯坦的谜题是:

  1. 诺基亚的沃尔夫冈•罗塞尔
  2. 达伦Galpin从英飞凌
  3. Laurent Arditi在一臂
  4. Phani Kumar仙女英飞凌的

你会注意到,我们添加了一个额外的奖励。尽管达伦的解决方案并没有得到正确答案由于错误,它是优雅和接收大量的当之无愧的选票。

前10名参与者收到了一个微型无人机作为一种特殊的感谢他们的出色的提交。获奖者将得到一个第二,更大的飞行机器配备了照相机。恭喜你,玩得开心和你的新无人机,但不要使用它们来检查你的邻居的饮酒习惯。我们在OneSpin乐趣与挑战,,看有多少工程师介入,看来你也这么做了。请继续关注——更多的是在商店!



5个评论

并且发展速度 说:

亲爱的塞吉奥,

你能解释为什么牛奶饮酒者限制错误的房子没有检测到ONESPIN验证工具?

最初的标准赢得这场比赛是最快的执行解决方案。然而所有这十项以相同的速度运行。

为什么ONESPINformal验证没有找到错误4获胜的解决方案?是一个需要目视检查?
提前感谢你的回答。
问候,
费迪南

并且发展速度 说:

亲爱的塞吉奥,
对不起,晚了,非常感谢你的明确的答案。我很欣赏!
祝你有美好的一天!
费迪南

塞吉奥Marchese 说:

你好费迪南

我很欣赏你的问题,我不幸的是今天才看到。谢谢你的耐心。

解决方案2是使用e语言(https://en.wikipedia.org/wiki/E_ (verification_language)),这是用于构建模拟测试长椅Specman工具。的解决方案是错误的,因为我知道这作者包括Specman日志文件。虽然不太满足比赛的规则,所有受访者的许可,我们将其作为我们认为它一个优雅的解决问题,可以借鉴,另一个人。我没有Specman工具可用,所以我不能实际运行解决方案2。不过,我看看它并指出代码中一个潜在的问题。

OneSpin是一个正式的验证工具,像所有其他形式验证工具,不支持e语言。因此,我们不能用OneSpin工具运行它。是可运行的,我们就会看到这个问题。OneSpin DV-Verify支持SystemVerilog和PSL断言语言,以及各种版本的Verilog, SystemVerilog,硬件描述语言(VHDL)的设计。我们甚至可以支持c++和SystemC-our直接竞争对手不能。

我希望回答了你的问题,再次感谢与我们这里!

——塞吉奥

Humera Ahsanullah 说:

你什么意思98%无法解决?我解决它在一个去我在2% ?我不确定这是任何难题或爱因斯坦的难题。

彼得Kornis 说:

我是一个在华邦电子(芯片设计)后端工程师。锁定在电晕的服务在国内,我决定学习Python。
我写了一个~ 250行Python代码详尽生成所有可能的组合和使用问题约束,通过消除,只剩下一个正确的解决方案。事实上德国和所有的房子位置约束都得到

留下一个回复


(注意:这个名字会显示公开)

Baidu