# Solving Sudoku Puzzles With First Order Logic

last updated 2022-03-06 15:21:11 by Simon Vandevelde

Sudoku is probably one of the most well-known logic games of all time.
Naturally, people have written various computer programs to solve the game, using a multitude of techniques.
In fact, searching for the key words "Sudoku Solver" on GitHub lists a whopping number of repos: 26K at the time of writing.
We can also see that most implementations are in imperative programming languages, such as Python (9106 repos), Java (3805 repos) or C++ (2907 repos).

This post describes a different approach for a sudoku solver, where we use the IDP-Z3 system, a

Typically, we start by declaring

The solution to this is creating a separate predicate

This post describes a different approach for a sudoku solver, where we use the IDP-Z3 system, a

**declarative**logic-based reasoning engine. Here, declarative means that instead of expressing*how*to solve a problem, we express*the behavior*of the problem. If this distinction seems a bit unclear at first, here are two examples:- Declarative: "each number must appear exactly once in each row."
- Imperative: "
*if*a row contains only one possible position for a 3,*then*the 3 must go there."

*Knowledge Base*, which in itself is structured in three blocks:**Vocabulary**: defines all the symbols that are used**Theory**: contains a description of the problem domain in FO(·)**Structure**: describes interpretations (= known values for symbols)

### Vocabulary

In the vocabulary, we define all the symbols that will be used throughout the rest of the knowledge base. As such, it is important that we carefully select how we want to represent a sudoku puzzle.Typically, we start by declaring

*types*. You can think of a type as a "domain of possible values". For instance, IDP-Z3 has a few built-in types, such as Integer, Boolean and Real. Eg., in the case of sudoku, we introduce the type*Row*to represent a row index from 0 to 8. Similarly, we introduce*Column*and*Value*(for the cell values).type Row := {0..8} type Column := {0..8} type Value := {1..9}After declaring our types, we can start thinking about how to represent cells and their values. In FO(·), the most intuitive way is by using a

*function*: a function expresses a mapping from its input types to its output type. In the snippet below we introduce*CellValue*, a function mapping each pair of*Row*,*Col*on*Value*.CellValue: (Row, Col) -> ValueNext, we need to express when two cells are in the same row/column/box. Here, we use a

*predicate*, which expresses a certain relation over its types: the predicate is either True or False for each possible set of inputs of its types. In FO(·), a predicate is expressed like a function, mapping on Boolean.SameRow: (Row, Col, Row, Col) -> Bool SameCol: (Row, Col, Row, Col) -> Bool SameBox: (Row, Col, Row, Col) -> BoolLastly, we want a way to set those cell values that are given at the start of a sudoku. While it might make sense to use our previously defined

`CellValue`

for this purpose, there are two reasons why this is not possible.
Firstly, in IDP-Z3, functions need to be *complete*, i.e., we should define a value for each set of inputs. We cannot enter only*some*values, but we would have to enter*all*values. Secondly, setting the values of a function or predicate is regarded as setting their "final solution", meaning that IDP-Z3 will expand (or alter) them.The solution to this is creating a separate predicate

`Given`

, as demonstrated below.
Note that we do not use a function here for the first reason outlined in the paragraph above.
The value of `Given`

will be set later in the structure.
Given: (Row, Col, Value) -> Bool

### Theory

Now that we have introduced our required concepts, we can start expressing the rules of sudoku. We begin by defining when two cells are in the same row, column or box. We write these down as*definitions*, which are used to*define*a concept necessary and sufficient conditions. Rows are defined as two cells with the same`x`

but different `y`

, while columns are defined in the opposite way.
The defenition for `Block`

is a bit more complex, but works. :-)
{ // Define row, column & block ∀x1 ∈ X, y1 ∈ Y, x2 ∈ X, y2 ∈ Y: Row(x1, y1, x2, y2) ← x1 = x2 ∧ y1 ≠ y2. ∀x1 ∈ X, y1 ∈ Y, x2 ∈ X, y2 ∈ Y: Column(x1, y1, x2, y2) ← y1 = y2 ∧ x1 ≠ x2. ∀x1 ∈ X, y1 ∈ Y, x2 ∈ X, y2 ∈ Y: Block(x1, y1, x2, y2) ←(x1 - x1 %3 = x2 - x2 %3) ∧(y1 - y1 %3 = y2 - y2 %3) ∧(x1 ≠ x2 ∨ y1 ≠ y2). }Next, we add the rules of sudoku. This is where IDP-Z3 truly shines: encoding these rules is trivial. We simply state that

*if*two cells are in the same Row/Col/Box,*then*they cannot have the same value.∀x1 ∈ X, y1 ∈ Y, x2 ∈ X, y2 ∈ Y: Row(x1, y1, x2, y2) ⇒ GridValue(x1, y1) ≠ GridValue(x2, y2). ∀x1 ∈ X, y1 ∈ Y, x2 ∈ X, y2 ∈ Y: Column(x1, y1, x2, y2) ⇒ GridValue(x1, y1) ≠ GridValue(x2, y2). ∀x1 ∈ X, y1 ∈ Y, x2 ∈ X, y2 ∈ Y: Block(x1, y1, x2, y2) ⇒ GridValue(x1, y1) ≠ GridValue(x2, y2).Lastly, we add a rule to state that if a value is given, it should also appear in the solution.

∀x ∈ X, y ∈ Y, value ∈ Value: Given(x, y, value) ⇒ GridValue(x, y) = value

### Structure

In the structure, we set the "already-known" values of the problem. In this case, these values are the given values. This is done as follows:Given := {(0, 3, 1), (0, 5, 7), (0, 6, 3), (1, 1, 4), (1, 2, 9), (1, 6, 5), (2, 4, 5), (3, 0, 8), (3, 2, 5), (3, 4, 1), (3, 5, 4), (3, 7, 3), (4, 2, 6), (4, 4, 2), (4, 5, 5), (4, 8, 4), (5, 4, 8), (5, 7, 1), (5, 8, 5), (6, 1, 8), (6, 4, 4), (6, 5, 1), (6, 7, 7), (7, 2, 3), (7, 3, 5), (7, 7, 8), (8, 1, 9), (8, 3, 8), (8, 6, 4)}.

## Execution

Now all that's left is executing the specification! In IDP-Z3, we use the`main`

block to specify how we want to use our knowledge.
In this case, we use the `model_expand`

method to generate the sudoku solution.
pretty_print(model_expand(T,S,max=1))This gives us the following output:

GridValue := {(0,0)->2, (0,1)->5, (0,2)->8, (0,3)->1, (0,4)->6, (0,5)->7, (0,6)->3, (0,7)->4, (0,8)->9, (1,0)->1, (1,1)->4, (1,2)->9, (1,3)->2, (1,4)->3, (1,5)->8, (1,6)->5, (1,7)->6, (1,8)->7, (2,0)->3, (2,1)->6, (2,2)->7, (2,3)->4, (2,4)->5, (2,5)->9, (2,6)->1, (2,7)->2, (2,8)->8, (3,0)->8, (3,1)->2, (3,2)->5, (3,3)->9, (3,4)->1, (3,5)->4, (3,6)->7, (3,7)->3, (3,8)->6, (4,0)->7, (4,1)->1, (4,2)->6, (4,3)->3, (4,4)->2, (4,5)->5, (4,6)->8, (4,7)->9, (4,8)->4, (5,0)->9, (5,1)->3, (5,2)->4, (5,3)->7, (5,4)->8, (5,5)->6, (5,6)->2, (5,7)->1, (5,8)->5, (6,0)->5, (6,1)->8, (6,2)->2, (6,3)->6, (6,4)->4, (6,5)->1, (6,6)->9, (6,7)->7, (6,8)->3, (7,0)->4, (7,1)->7, (7,2)->3, (7,3)->5, (7,4)->9, (7,5)->2, (7,6)->6, (7,7)->8, (7,8)->1, (8,0)->6, (8,1)->9, (8,2)->1, (8,3)->8, (8,4)->7, (8,5)->3, (8,6)->4, (8,7)->5, (8,8)->2}.And that's it, we're done!