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 x2 – 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 x2 – 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!