Sudoku is a very popular puzzle. The goal is to insert the numbers in the boxes to satisfy only one condition: each row, column and
3x3 box must contain the digits
9 exactly once.
The following example encodes the sudoku problem in Z3. Different sudoku instances can be solved by modifying the matrix
instance. This example makes heavy use of list comprehensions available in the Python programming language.
# 9x9 matrix of integer variables