Solving Sudoku Using Cryptol

March 18th, 2009 by Levent Erkok

Cryptol is a language tailored for cryptographic algorithms. Sudoku is a popular puzzle the reader  is no-doubt already familiar with. We will offer no deep reason why anyone should try to solve Sudoku in Cryptol; other than the very fact that it’d be a shame if we couldn’t!

Needless to say, Cryptol has not been designed for encoding search algorithms. Nonetheless, some of the features of Cryptol and its associated toolset make it extremely suitable for expressing certain constraint satisfaction problems very concisely; and Sudoku very nicely falls into this category.

Representing the board

A Sudoku board can be represented in a variety of ways. We will pick the simplest: A sequence of 9 rows, each of which has 9 elements storing the digits. Each digit will require 4 bits; since they range from 1 to 9. So, a good Cryptol type for a board is:

     [9][9][4]

In Cryptol-speak, this type simply represents a sequence of precisely 9 elements, each of which is a sequence of 9 elements themselves, each of which are 4-bit words. (Technically, the type [4] also represents a sequence of precisely 4 elements, each of which are bits. But it’s easier to read that as 4-bit words. The type [4] and [4]Bit are synonymous in Cryptol, and can be used interchangeably in all contexts.)

Recognizing a valid row, column, or box

Let us tackle a much simpler problem to start with. How would we determine if a given set of 9 numbers form a valid Sudoku row, column, or a box? We should simply check that each number from 1 to 9 appears precisely once in the sequence:

check : [9][4] -> Bit;
check group = [| contains x  || x <- [1 .. 9] |] == ~zero
   where contains x = [| x == y || y <- group |] != zero;

We simply iterate over the numbers 1 through 9, and check that the given  group contains that number.  The function contains iterates through all the elements in the given group, and makes sure one of them is the currently looked for element.

(The Cryptol primitive  zero is a polymorphic constant representing all False’s. The operator ~ inverts all the bits. Hence, the test “== ~zero” makes sure all the components are True; and the test “!= zero” makes sure at least one bit is True.)

Recognizing a full board

Given a full Sudoku board, checking it’s a valid solution simply amounts to identifying rows, columns, and squares; and “check“-ing them all, in the above sense. The following Cryptol function accomplishes this task rather concisely:

valid : [9][9][4] -> Bit;
valid rows = [| check grp
             || grp <- rows # columns # squares |] == ~zero
 where {
   columns = transpose rows;
   regions = transpose [| groupBy (3, row) || row <- rows |];
   squares = [| join sq || sq <- groupBy(3, join regions) |]
 };

The function valid receives 9 rows; and calls check on all these rows, columns, and the squares. Columns are easy to compute: we simply use Cryptol’s transpose primitive. The squares are slightly more tricky, but not particularly hard. We first group all the rows in length 3 segments, and transpose these to align them, thus forming the regions. Then the squares are simply grouping of the regions 3 elements at a time. It’s a good exercise to precisely work out how the squares are formed using the above code, something we encourage the interested reader to do on a rainy afternoon..

Solving Sudoku

All we have done so far is to recognize a given Sudoku board as valid; we have not written a single line of code to actually fill a partially empty board. The good news is that we do not need to! We have all the bits and pieces ready to go. Sounds too good to be true? Well, read on!

Enter Formal methods

What if I told you that recognizing a valid Sudoku board is  sufficent to actually solve one that has empty squares on it, using Cryptol’s formal-methods toolbox? The idea is rather simple. But before we get there, we need to take a detour into the Cryptol toolbox.

Checking  satisfiability

Cryptol’s formal-methods tools can perform equivalence, safety, and satisfiability checking. We have talked about the former two in an earlier post. Today, we will look at satisfiability checking only. Given a function  f, the satisfiability checking problem asks if there is any  x such that f x = True. Here is a simple example. Let:

  f : [8] -> Bit;
  f x = x*x - 7*x + 12 == 0;

The function f returns True if its given 8-bit argument is a solution to the quadratic equation x² – 7x + 12 = 0.  We have:

Cryptol> :sat f
f 4
         = True

Indeed, 4 is a solution to this equation. Is there any other solution? It is easy to formulate a similar query using the lambda-notation:

Cryptol> :sat (\x -> f x & (x != 4))
((\x -> f x & (x != 4))) 3
         = True

Cryptol tells us 3 is a solution as well! Since this is a quadratic equation, there can be at most two solutions; let’s verify:

Cryptol> :sat (\x -> f x & (x != 4) & (x != 3))
No variable assignment satisfies this function

As expected, Cryptol confirms that 3 and 4 are the only  8-bit values that satisfy the equation x² – 7x + 12 = 0.

(I should mention  that the :sat command is available only in the symbolic and sbv backends of Cryptol; the two main backends of Cryptol that are capable of performing formal-verification.)

Back to Sudoku

Remember the valid function that returns True if a given full board is a correctly laid-out Sudoku board? With the magic of satisfiability checking, we can just use that definition to fill in the blanks for us! To illustrate, consider the board below.

How do we encode a board with empty cells in Cryptol? One simple idea is to represent the board as a function: It will take the values of its “empty” cells, and return the full board. In the Cryptol encoding below I have tried to align the variables so that they correspond exactly to the empty cells, and named them row-by-row:

  puzzle : [53][4] -> Bit;
  puzzle   [ a1    a3    a5 a6       a9
             b1       b4 b5    b7    b9
                c2    c4 c5 c6 c7 c8 c9
             d1 d2    d4    d6 d7 d8
             e1 e2 e3    e5    e7 e8 e9
                f2 f3 f4    f6    f8 f9
             g1 g2 g3 g4 g5 g6    g8
             h1    h3    h5 h6       h9
             i1       i4 i5    i7    i9 ]
   = valid [[a1  9 a3  7 a5 a6  8  6 a9]
            [b1  3  1 b4 b5  5 b7  2 b9]
            [ 8  c2 6 c4 c5 c6 c7 c8 c9]
            [d1 d2  7 d4  5 d6 d7 d8  6]
            [e1 e2 e3  3 e5  7 e7 e8 e9]
            [ 5 f2 f3 f4  1 f6  7 f8 f9]
            [g1 g2 g3 g4 g5 g6  1 g8  9]
            [h1  2 h3  6 h5 h6  3  5 h9]
            [i1  5  4 i4 i5  8 i7  7 i9]];

It might take a bit of staring at this definition; but the idea is strikingly simple.  Notice that the type of puzzle is [53][4] -> Bit, precisely because there are 53 empty cells. Also, instead of just returning the final board, I simply pass it to the function valid; so that the function puzzle will return True precisely when it is given the correct numbers that solve it!

By now, it must be obvious how we’ll solve Sudoku in Cryptol: All we need to do is to ask Cryptol to find the right input value to make the function return True, i.e., we need to find a satisfying assignment. Here’s the response from Cryptol:

Sudoku> :sat puzzle
puzzle [2 5 4 3 1 4 8 6 9 7 7 1 9 2 5 4 3 3 8 4
        9 2 1 6 1 2 8 4 9 5 4 9 2 6 3 8 7 6 3 5
        2 4 8 9 8 7 1 4 1 9 3 6 2]
         = True

If we plugin the numbers we get from Cryptol back into the grid, we get the full  solution depicted below. (I used italic for the numbers found by Cryptol.)

Well; that’s what we set out to do originally; so mission accomplished!

What just happened here?

Apologies if you were expecting to see Cryptol code that actually searched for the values of the empty cells! Note that we have not written a single line of code that tried to deduce what must go in the empty cells, nor  have we implemented a search algorithm. We merely viewed Sudoku as a satisfiability problem, and asked Cryptol’s formal-methods tools to find the missing values for us. The necessary search is all done by the underlying formal-methods engine, freeing us from the labor. Yet another instance of telling the computer “what” to do, instead of “how.”

Download

Here is the Cryptol code that contains all the definitions you need.  Enjoy!

6 Responses to “Solving Sudoku Using Cryptol”

Ivan Miljenovic says:

How does this compare efficiency-wise to the dedicated Sudoku solvers found here: http://haskell.org/haskellwiki/Sudoku ?

Levent Erkok says:

Hi Ivan:

I have not done any “efficiency” studies. As a data-point, it can solve the “nefarious” one given at the bottom of the page you linked in 7.53 seconds on a 2.4GHz Dual-Core Opteron machine with 4GB memory, running RedHat linux. I’m not sure how the other ones do on it. Please post if you’ve any data!

Andy Moreton says:

I’m not familiar with Cryptol, but surely:
f x = x*x – 7*x + 12 == x;
should be
f x = x*x – 7*x + 12 == 0;

Boris Lykah says:

It seems that function check does not check length of the group. So it can return True for group like [1..9,9,10,123].

Levent Erkok says:

Andy: You’re quite right with respect to the typo in the quadratic equation. Now fixed. Thanks!

Levent Erkok says:

Boris: You are correct that “check” should really verify its input has 9 elements; this is always true whenever it’s used in the code here, but it’s best to be explicit. Luckily, we can simply express this in it’s type; simply give it the following type signature: “check : [9][4] -> Bit;” and without any code change, Cryptol will make sure that it’s always called with 9-element sequences. I’ve updated the post and the associated code to include the type signature. Note that we did not have to change the code at all: This is one of the strong points about Cryptol and it’s precise size-types. Thanks for the note.

Leave a Reply

Name

Email address (will not be published)

Website (optional)

Comments