In a recent post we celebrated the 10th anniversary of the declarative, formal language HLL. The language is used extensively in the railway signaling domain for the formal verification of interlocking logic and CBTC subsystems (such as zone controllers). In this more technical post we will familiarize the reader further with HLL, by formalizing the famous Sudoku problem in the language, and using an off-the-shelf proof engine to solve Sudoku puzzles.

The Sudoku problem is a very easy problem for modern proof engines (such as SAT solvers), but it will serve us well in introducing the reader to HLL. To be sure, we will only be able to illustrate a relatively small subset of HLL, a language which has grown quite a bit over the years. To formalize and solve Sudoku problems we will mainly need integers, arrays and quantifiers.

### Creating the grid

We start by representing a partially filled Sudoku grid using a 9×9 matrix where each element is an integer in the range 0 to 9. Empty slots are filled with zeroes. The problem itself was in the “Very Difficult” category over at 7sudoku.

Declarations: int partialGrid[9][9]; Definitions: partialGrid := {{0, 7, 0, 4, 0, 0, 0, 9, 2}, {0, 0, 0, 0, 8, 0, 0, 0, 5}, {0, 0, 3, 0, 0, 0, 7, 0, 0}, {0, 0, 0, 0, 0, 0, 0, 8, 0}, {0, 0, 7, 0, 1, 0, 5, 0, 4}, {0, 0, 0, 2, 3, 7, 0, 0, 0}, {2, 0, 4, 0, 0, 5, 0, 0, 3}, {0, 0, 0, 0, 0, 0, 0, 0, 0}, {8, 0, 5, 0, 0, 0, 1, 0, 0}};

Then, we will define our problem grid by replacing the zeroes in the partial grid with unknown integers in the range 1 to 9. Creating unknown (or free) variables in HLL is very simple: we just need to declare them.

Declarations: int [1,9] unknown[9][9]; int [1,9] grid[9][9]; Definitions: grid[i][j] := if partialGrid[i][j] == 0 then unknown[i][j] else partialGrid[i][j];

### Expressing the Sudoku problem

Now, we will express the Sudoku problem itself over our grid, by using quantification. Remember that the objective of a Sudoku is to fill the grid so that all rows, all columns and all of the nine 3×3 subgrids each contains all the digits from 1 to 9. In HLL, array-indexing is 0-based, yielding the below formulation of our Sudoku-objective.

Definitions: objective := ALL digit:[1,9] ( ALL row:[0,8] SOME col:[0,8] (grid[row][col] == digit) & ALL col:[0,8] SOME row:[0,8] (grid[row][col] == digit) & ALL subgridRow:[0,2], subgridCol:[0,2] SOME sRow:[0,2], sCol:[0,2] (grid[subgridRow * 3 + sRow] [subgridCol * 3 + sCol] == digit));

Finally, we will ask a proof engine whether our objective is attainable (or satisfiable) or not. We do that by trying to prove that there is no solution (by negating the problem). If there is a solution (i.e. a counterexample to our proof), the proof engine will provide us with it.

Proof Obligations: ~objective;

Using a modern proof engine (such as Prover SL Certifier Edition) we will be provided with a solution in a fraction of a second.

$1*: grid[0][0] is [1] $2: grid[0][1] is [7] $3: grid[0][2] is [6] $4: grid[0][3] is [4] $5: grid[0][4] is [5] $6: grid[0][5] is [3] $7: grid[0][6] is [8] $8: grid[0][7] is [9] $9: grid[0][8] is [2] ... $80: grid[8][7] is [2] $81: grid[8][8] is [9]

### Improving the presentation

To improve the presentation a bit, we will use the temporal dimension of HLL (cf. LTL). HLL is a language based on streams, which are just infinite sequences of values, one for each discrete time step. The idea is to transform the 9×9 grid into 9 streams (representing the rows), of which we will inspect only the 9 first values. Doing this is a bit technical. We need to 1) redefine the grid as a memory that keeps its value in each time step, and 2) define a counter that counts time steps modulo 9 (starting at 0), before we can create our 9 “stream rows”.

Declarations: int [0,8] counter; int [1,9] rows[9]; Definitions: grid[i][j] := if partialGrid[i][j] == 0 then unknown[i][j] else partialGrid[i][j], grid[i][j]; // Keep value in next time step counter := 0, (counter + 1) % 9; rows[i] := grid[i][counter];

Finally, when asked to extend the solution up to the 9th time step, the proof engine provides us with a prettier view of the Sudoku-solution (without any measurable time penalty by the way).

$1*: rows[0] is 1 7 6 4 5 3 8 9 [2] $2: rows[1] is 9 4 2 7 8 1 3 6 [5] $3: rows[2] is 5 8 3 6 2 9 7 4 [1] $4: rows[3] is 3 9 1 5 4 6 2 8 [7] $5: rows[4] is 6 2 7 9 1 8 5 3 [4] $6: rows[5] is 4 5 8 2 3 7 9 1 [6] $7: rows[6] is 2 1 4 8 9 5 6 7 [3] $8: rows[7] is 7 3 9 1 6 2 4 5 [8] $9: rows[8] is 8 6 5 3 7 4 1 2 [9]

Note that this is the raw, unedited, output given by the proof engine’s “Why”-module, which can be used to interactively explore counterexamples.

### Summary

To summarize, we have shown how the well-known Sudoku problem can be formalized in HLL and solved using a general purpose proof engine (don’t hesitate to contact sales@prover.com to buy your own license!). The output has been optimized using prefixes of length 9 of streams (sequences of values), so that it looks almost like what one would expect from a purpose-built Sudoku solver.