Solving Sudoku Puzzles With First Order Logic

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 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:

1. Declarative: "each number must appear exactly once in each row."
2. Imperative: "if a row contains only one possible position for a 3, then the 3 must go there."

The notation of the IDP-Z3 engine is FO(·), an extension of First Order Logic. It attempts to strike a balance between readable for humans, but expressive enough to model practical problems. Knowledge on a problem is stored in FO(·) in a so-called Knowledge Base, which in itself is structured in three blocks:

1. Vocabulary: defines all the symbols that are used
2. Theory: contains a description of the problem domain in FO(·)
3. 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) -> Value

Next, 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) -> Bool

Lastly, 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!

Try it yourself!

You can try out this IDP specification in the online editor yourself. However, for the sake of simplicity, I have left out the definition of Row/Col/Block and have simply declared their values in the structure instead.