close By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.

OneSpin Puzzler:
The Top 10 Solutions

Sudoku Holiday Puzzle - The winners!

It has become a time-honored tradition for OneSpin to pose a holiday puzzle challenge to engineers everywhere. This year, we asked you to solve the hardest Sudoku in the world using a formal tool, and to prove that the solution is unique.

We received a ton of superb, unique submissions from around the world.

Here are the winners:

We also decided to add an extra prize:

Hi, delighted that you’ve done another puzzle this year. It was fun and educational last year. My solution takes 3.5s to prove uniqueness, so I doubt it will be the fastest and it’s not particularly readable, so I’m sure it’ll not be up for a prize, but I really wanted to support this by taking part. Cheers, Anthony

All four winners will receive an Amazon Echo Plus and could use it to implement a voice-controlled Sudoku solver.

For next year, we have new ideas, not only for the puzzle but also for the format of the challenge. If you have feedback or proposals to share, please email us at We want to hear from you.

The Sudoku Challenge

Ah, Sudoku. Never did a puzzle offer such a variety of difficulty levels. These variable little brain teasers can make you feel like you’re out for a gentle stroll in the park, or they can give you the impression that you’re scaling a mountain with a refrigerator on your back—and everything in between.

In 2012, Finnish mathematician Arto Inkala came up with what was then regarded as the hardest Sudoku in the world (pictured at right). Apparently, on a difficulty scale from one to five stars, this Sudoku would score eleven stars. Sudoku’s Everest!

Faced with such a hard slog to complete this seemingly insurmountable puzzle, it’s only natural to look for ways to find a foothold and get a leg up (ha ha ha). Formal tools to the rescue! With a little programming, they can virtually teleport you to the summit.

What do you say? Are you up to the task?

Your mission—should you choose to accept it—is as follows:

Set up the problem. You can use VHLD/Verilog/SystemVerilog to write RTL code and SVA/PSL/ITL for assertions.

You can use any formal tool to find the solution, but make sure the tool script only uses the basic commands to compile and run the checks, so that your code is fit to run on other formal tools and even simulators.

Additionally, without using the information on the solution you have found, write an assertion to prove that the solution is unique. A simulator won’t be any good for that—ha!

Deadline has been passed on Sunday, January 7th, 2018

Winners will be announced by the end of March after a thorough review. Best of luck!