Introduction to witchcraft and wizardry using Z3

Z3 is a high-performance theorem prover that was developed by Microsoft Research. It is used to solve SMT (Satisfiability Modulo Theories) problems.It supports a wide range of logical theories, including arithmetic, bitvectors, arrays, and quantifiers. It can be used to prove theorems and to check the satisfiability of formulas. It is used in many applications such as program analysis, software/hardware verification, and security. In this tutorial, we will introduce the basics of SMT and then dive into how to use Z3 to solve SMT problems.

What is SMT?

SMT is a problem-solving paradigm that combines the expressive power of first-order logic with efficient decision procedures for various theories. An SMT problem is a decision problem that asks whether a given formula in first-order logic with background theories is satisfiable. An SMT solver is a tool that can determine whether a given formula is satisfiable and, if so, provide a satisfying assignment (answer).

Using Z3

Z3 has bindings for many programming languages, including C, C++, Java, Python, and OCaml.

In this tutorial, we will use the Python bindings.

To install Z3, run the following command:

pip install z3-solver

To use Z3, we first need to import it:

Solving a system of linear equations

You can use z3 to solve a system of linear equations. For example

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

outputs: $\[y = 0, x = 7]$ which is the solution to the system of equations.

Z3 can also solve more complex systems of equations. For example, consider the following system of equations:

You can use the following more verbose way to solve this system of equations.

from z3 import *
x, y, z = Ints('x y z')
s = Solver()
s.add(x + y + z == 6)
s.add(2*x + y + 2*z == 8)
s.add(x + 2*y + 3*z == 14)
if s.check() == sat:
    print(s.model())

Click on the button below to see it in action.

You can do a lot more with z3.

Here I will show some of the cool things you can do with z3.

Logical Reasoning Using Z3

Given the following problem:

John, Aries, and Joseph are brothers with different ages. Who is the youngest if the following statements are true? I. Aries is the oldest. II. John is not the youngest.

We can use z3 to solve this problem. First, we need to define the variables. We will use an array of 3 integers to represent the ages of the brothers. The value of each integer represents the age of the brother in that position. For example, if the value of the first integer is 3, then the brother in the first position is 3 years old.

from z3 import Solver, Ints, Distinct, sat, If

def min(li):
    m = li[0]
    for i in li[1:]:
        m = If(i < m, i, m)
    return m
  
# Define variables for each brother's age
john, aries, joseph = Ints('john aries joseph')

# Define the constraints
constraints = [
    # Aries is the oldest
    aries > john,
    aries > joseph,
    # John is not the youngest
    john > joseph,
    # All ages are distinct
    Distinct(aries, john, joseph)
]

# Create a solver and add the constraints
solver = Solver()
solver.add(constraints)

# Check if the constraints are satisfiable
if solver.check() == sat:
    # If there is a solution, get the model and print the youngest brother
    model = solver.model()
    ages = [model[aries], model[john], model[joseph]]
    youngest = min(ages)
    if youngest == model[john]:
        print("John is the youngest")
    else:
        print("Joseph is the youngest")
else:
    # If there is no solution, print a message
    print("No solution found")

Click Run to see the output.

The 8 Queens Problem

The 8 queens problem is a classic problem in computer science. It asks whether it is possible to place 8 queens on a chessboard such that no two queens attack each other. A queen can attack another queen if it is on the same row, column, or diagonal. The following figure shows an example of a solution to the 8 queens problem. For some background about this problem you can check out this Wikipedia article.

In order to be able to place 8 queens on the chessboard, all the following must be satisfied:

• All queens must be in different rows.
• All queens must be in different columns.
• No two queens can be on the same diagonal.
• All queens must be on the board.
• There must be exactly 8 queens.

Now that the problem is defined as a set of constraints, Z3 can be used to solve it.

First, we need to define the variables. We will use an array of 8 integers to represent the queens. The value of each integer represents the column of the queen in that row. For example, if the value of the first integer is 3, then the queen in the first row is in the third column.

from z3 import *
queens = [Int(f'queen{i}') for i in range(8)] # This implicitely satisfies the first constraint.

Next, we need to add constraints to the solver. We will add the following constraints:

s = Solver()
s.add(Distinct(queens)) # All queens must be in different columns.

for i in range(8):
    s.add(queens[i] >= 0, queens[i] <= 7) # All queens must be on the board.
    for j in range(i):
        s.add(queens[i] != queens[j], queens[i] != queens[j] + (i - j), queens[i] != queens[j] - (i - j)) # No two queens can be on the same diagonal.

s.add(len(queens) == 8) # There must be exactly 8 queens.

Now we can check if the problem is satisfiable and print the solutions.

while s.check() == sat:
    m = s.model()
    print_solution(m)
    # Add a new constraint to avoid the current solution
    s.add(Or([queens[i] != m.evaluate(queens[i]) for i in range(8)]))

It is known that the 8 queens problem has 92 solutions. Running this code will print all the 92 solutions!

Z3 Sudoku Solver

Sudoku is a popular puzzle game. The goal of the game is to fill a 9x9 grid with numbers from 1 to 9 such that each row, column, and 3x3 subgrid contains all the numbers from 1 to 9. Here are the constraints of the game:

• Each row must contain all the numbers from 1 to 9.
• Each column must contain all the numbers from 1 to 9.
• Each 3x3 subgrid must contain all the numbers from 1 to 9.
• Each cell can only contain one number from 1 to 9.

You can learn more here.

The following code solves a given sudoku game using Z3. The code is based on this tutorial.

First, we define a 2d array of integer variables to represent the sudoku grid and a 9x9 matrix to hold the integer variables to be used for the constraints.

instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))
# 9x9 matrix of integer variables
X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(9)] for i in range(9)]

Then we define the constraints. The constraints are:

cells_c  = [And(1 <= X[i][j], X[i][j] <= 9) for i in range(9) for j in range(9)] # Each cell can only contain one number from 1 to 9.
rows_c = [Distinct(X[i]) for i in range(9)] # Each row must contain all the numbers from 1 to 9.
cols_c = [Distinct([ X[i][j] for i in range(9) ]) for j in range(9)] # Each column must contain all the numbers from 1 to 9.
sq_c = [Distinct([ X[3*i0 + i][3*j0 + j]
                        for i in range(3) for j in range(3)])
             for i0 in range(3) for j0 in range(3)] # Each 3x3 subgrid must contain all the numbers from 1 to 9.
sudoku_c = cells_c + rows_c + cols_c + sq_c # Sudoku constraints is the sum of all the constraints

We also need to let z3 know about the game we are trying to solve. We can do this using the following code that creates a list of constraints using list comprehension, such that, if the value of a cell in the game is 0, then we return a True constraint which essentially means no constraint. Otherwise, we have a constraint that X[i][j] must be equal to the value of the cell in the game.

instance_c = [If(instance[i][j] == 0, True, X[i][j] == instance[i][j]) 
              for i in range(9) for j in range(9)] # If(condition, true_value, false_value)

Finally, we add the constraints to the solver and check if the problem is satisfiable.

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    print_matrix(r)
else:
    print("failed to solve")

Conclusion

Z3 is an extremely powerful tool for solving constraint satisfaction problems. In this tutorial we touched the surface of what Z3 can do. You can find a lot more in this tutorial and in the official repository.