CTF-z3解数独
dummy

### Sudoku

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 1 through 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.