Sudoku solver and generator

This is a program for solving and generating sudoku puzzles using SAT.

The generated puzzles are guaranteed to have a unique solution, they are also completely random. Solutions are guaranteed to be as difficult as possible, that is, removing any number makes the sudoku solutions non unique.

The solver can find all possible solutions, if they exist. This is useful, as non random boards can be generated much faster, using an empty board as the starting state.

How it works

The algorithm to generate a random sudoku is as follows:

1. The program assigns a random number to a random position.
2. The sudoku is solved, then
   • If no solutions exist, then the assignment is undone and the program goes back to step 1.
   • If there is exactly one solution, return it.
   • If there is more then one valid solution, return to step 1 with the new board.

The actual solver uses a SAT model and looks for 2 solutions.

Preview

Play yourself here!

SAT - solver model

language Essence 1.3

letting D0 be domain int(0..9)
letting Id be domain int(1..3)
letting D  be domain int(1..9)

given initial : matrix indexed by [D, D] of D0

find sudoku : matrix indexed by [D, D] of D
find blocks : matrix indexed by [Id, Id] of (matrix indexed by [Id, Id] of D)

such that

$ Initialize the sudoku block with entries from initial
forAll i, j: D . !(initial[i, j] = 0) <-> sudoku[i, j] = initial[i, j],

$ Unique entries in each row and column
forAll i: D . allDiff(sudoku[i,..]) /\ allDiff(sudoku[..,i]),

$Unique entries in each block
forAll i, j: Id . allDiff ( flatten ( blocks[i, j] ) ),

$ The blocks are the sudoku blocks
forAll i, j, k, l: Id .
   blocks[i, j][k, l] = sudoku[3 * i - 3 + k, 3 * j - 3 + l],

$ The sudoku grid looks human random
 forAll i: D . !(sudoku[i,..] = [1,2,3,4,5,6,7,8,9]) /\
               !(sudoku[..,i] = [1,2,3,4,5,6,7,8,9]) /\
               $ Banned first patterns
               !(sudoku[1,1] = 1 /\ sudoku[1,2] = 2 /\ sudoku[1,3] = 3 /\ sudoku[1,4] = 4 /\ sudoku[1,5] = 5) /\
               !(sudoku[1,3] = 3 /\ sudoku[1,4] = 4 /\ sudoku[1,5] = 5 /\ sudoku[1,6] = 6 /\ sudoku[1,7] = 7) /\
               !(sudoku[1,5] = 5 /\ sudoku[1,6] = 6 /\ sudoku[1,7] = 7 /\ sudoku[1,8] = 8 /\ sudoku[1,9] = 4)

language Essence 1.3

letting SQ11 be [

   [ 0, 7, 2,   0, 0, 4,   9, 0, 0; int(1..9)],
   [ 3, 0, 4,   0, 8, 9,   1, 0, 0; int(1..9)],
   [ 8, 1, 9,   0, 0, 6,   2, 5, 4; int(1..9)],

   [ 7, 0, 1,   0, 0, 0,   0, 0, 9; int(1..9)],
   [ 9, 0, 0,   0, 0, 2,   0, 7, 0; int(1..9)],
   [ 0, 0, 0,   8, 0, 7,   0, 1, 2; int(1..9)],

   [ 4, 0, 5,   0, 0, 1,   6, 2, 0; int(1..9)],
   [ 2, 3, 7,   0, 0, 0,   5, 0, 1; int(1..9)],
   [ 0, 0, 0,   0, 2, 5,   7, 0, 0; int(1..9)],

      int(0..9)]

Advantages

The main advantage of this approach is simplicity. Using the AI to solve the problem is quite efficient, while the code itself is simple and small.

Other “low-level” approaches are faster, but not extendable. This approach can be used to generate other puzzles easily or add different constraints on top.

One way to extend this, is by solving a random board and then asking the AI to give a simpler version with more spaces filled.

How to install

For this project to work, you need a working version of conjure. A working compiler Go is also required. To begin generating, type:

go run main.go

This will save a new random sudoku inside the solutions folder.