
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.

How safe and efficient are your rail control systems? Let’s find out!
Share this article

Learn more about how to develop specifications with Digital Twins
Fill out your information here.
More News & Articles
Explore how Prover is revolutionizing railway signaling with AI and formal methods. Discover Prover Labs: a hub for innovation, collaboration, and shaping AI-driven automation for enhanced safety, efficiency, and precision in signaling design.
Prover introducing Signaling Design Automation to students at CentraleSupélec in Paris.
Prover PSL, the leading model checker used for formal verification in the rail and metro signaling domain, is now even faster.