Using Formal To Solve The World’s Hardest Sudoku

It’s no secret that the OneSpin team loves contests. Last year around this time, we set a challenge to engineers everywhere: solve the famous Einstein’s Riddle using a formal tool.

After an enthusiastic response, we decided to make the holiday puzzle an annual event, with a different subject area each year. Our engineering team was challenged to come up with a new topic, and my idea, which centers on what has been called the “World’s Hardest Sudoku,” was chosen for this year’s puzzle. You can learn more about the contest here. Read on to find out how I came up with the challenge.

Several months back, I ran across a news article entitled, “Unsolvable Sudoku: Do you dare to try?” I spent a week’s worth of consecutive evenings working on the puzzle (pictured here) for a few hours every day, but I was only able to manage to jump back and forth between a handful of steps. It has been said that, on a difficulty scale of one to five stars, this puzzle would be an eleven—I believe it! I had all but given up until our marketing team reached out for ideas about this year’s holiday puzzle.

I’ve heard it said that any chess or Sudoku problem can be solved in a second by a formal engine. If I couldn’t crack this tough nut on my own, formal certainly could. The question was how to appropriately create an appropriate ‘nut’ to feed into a formal engine so that it could solve this puzzle. I don’t want to give away too many hints here, for those hoping to enter the contest themselves, but I will reveal a bit of my approach to the problem.

My goal was to minimize the time on my keyboard and let the tool do the hard part. Writing the design in VHDL seemed a good way to go, because by the standard you can define a signal as follows:

in_data : in integer range 1 to 9;

The fundamental rule of Sudoku is that only positive integers from 1 to 9 are accepted in any cell. The rest of the logic on the RTL level was creating the puzzle’s nine-by-nine matrix. The remaining rules regarding rows, columns, and three-by-three boxes I created in SystemVerilog Assertions with the constraints. As a proof problem, I created an assertion asking the tool if the given matrix can be fulfilled.

That’s all that I will reveal! Surely, there are a great many other ways to approach this problem—in fact, several engineers from around the world have submitted solutions that approach it differently than I did. I look forward to reviewing all of the contest entries with our judging panel of formal experts from across OneSpin once the contest closes January 7. I’ll post a follow-up blog here in due time to congratulate the winners and give overviews of their solutions. In the meantime: How about it? Will you give it a go?