Video Easter Egg: Incisive Formal Verifier driving a Rubik's Cube solving robot

Just in time for Easter, Team Verify's Apurva Kalia, Manu Chopra, and Suman Ray created a Rubik's Cube solving Lego robot. However, unlike any other such 'bot, the brains of this one are a single SVA assertion that is solved by Incisive Formal Verifier (IFV), a Formal verification tool by Cadence Design Systems, Inc. More details in this blog post: http://is.gd/TPG8vM

UPDATE: the team is working on a new & improved robot, to be revealed at CDNLive India in Bangalore on October 19, 2011 in Bangalore. http://is.gd/IxQe66 Stay tuned for more ...

Credits: This Rubik's Cube robot is based on a design by Hans Andersson (http://tiltedtwister.com/tiltedtwiste...)

• Category

  Science & Technology

[Joe Hupcey III]

Comment from another Formal team member:

"Just to add to this – it has been proven than any optimal cube solution can be found within 23 moves. This means that the cube may be jumbled any number of moves, but can be solved within 23. In this case also, the cube was jumbled more than 6 moves, but IFV was able to find a solution with 6 moves. I think today IFV will be able to go beyond 9-10 also – which is pretty good and will signify a pretty jumbled cube."

[Joe Hupcey III]

Answer to the previous question from R&D:

"We found that that IFV was able to find a quick solution even for 9 moves. Due to lack of time, we have not explored beyond 9. We agree with your guesstimation that if we feed a non-efficient generic modeling to IFV, somewhere around 20 moves IFV might get into trouble depending on the CPU&memory you were using. In general, Rubik's Cube is actually one of the harder problems for formal to solve."

[IAssemble]

- have you seen the the website cube20 dot org? I believe it has now been proven the worst case is 20 moves.

I'm impressed that a formal tool can find a solution beyond a 9-10 move scramble. However, only a very small fraction of scrambled positions, approximately 1 in 1.8e8, are reachable in 10 moves so I'm not sure it's really a "pretty jumbled cube" from a mathematical perspective, although I suspect most humans would have trouble finding even a 9-10 move solution :-)

[IAssemble]

Brilliant. An ingenious way to find a solution to the Rubik's Cube puzzle!

I notice this position only required 6 moves to solve. Can IFV find a solution to more complex positions such as "superflip" that require a minimum of 20 moves to solve? I speculate that solutions of this length would require too much CPU time and/or memory to be tractable.