This short tutorial serves as an introduction to using Z3 through its Python interface as
well as learning how to encode general problems into SAT problems. The first step, if you
haven't done so before, is to install Z3 and its python bindings. Once your installation is
working, you can start going through the video tutorial.
The first video introduces basics commands and then explains how the Five Queens problem can
be encoded into a SAT problem. The second (bonus) video uses all the commands and techniques
presented in the first video to write a Sudoku solver in a few lines.
You can find a guide to the API here. However, in this tutorial we are only using a very restricted subset of the commands. In particular we are not using integers or any other variable types than booleans. You might find reading this guide confusing at first, but rest assured, you will learn how to use other features of the solver during the next tutorial.
In this tutorial, we will be using Z3's Python interface. The easiest way to install it, along with a Z3 binary, is to use Python's package manager pip. In this tutorial, we will be using Python 3.7. Start by installing the corresponding Z3 package with the command:
Remark that the corresponding package is z3-solver and not z3. Do not install the latter!
We will not need any other package in this tutorial, so you can create a virtual environment with this package only. You can also look for other installation methods on Z3' github page , and keep in mind that we want to use the Python interface. Once you are set up, you should be able to call the solver from your terminal and see:
$ z3 Error: input file was not specified. For usage information: z3 -h
To test your Python installation, launch the Python interpreter for which you installed Z3. You should be able to type the following commands:
$ python ... >>> from z3 import * >>> s = Solver() >>> s.check() sat
Now you have installed all the software we need in this tutorial. If you want to do some background reading, you can start here but the tutorial will be self contained. Z3 is much more than a simple SAT solver, but we will not use any of its SMT solving or theorem proving capabilities for now.
You can view the video on MyMedia by clicking on the following link or watch on YouTube below:
You can see the solution for the Five Queens problem presented in this video here.
In the first part of the video, we review the basic functionalities we need in order to write formulas and manipulate the solver.
To write a boolean formula, we will need to declare boolean variables for the solver. You can do this in Python using the Bool() constructor. For example, we can start by creating two boolean variables x and y:
>>> from z3 import * >>> x = Bool("x") >>> y = Bool("y")
With boolean variables, you can build boolean formulas. z3 gives you constructors for disjunctions and conjunctions, negation, and equivalence:
>>> x_or_y = Or([x,y]) # disjunction >>> x_and_y = And([x,y]) # conjunction >>> not_x = Not(x) # negation >>> x_or_y_iff_not_x = x_and_y == not_x # This is the formula (x_or_y <=> not_x) not a boolean!
Once we have built the clauses that compose our problem, we can pass them to a solver:
>>> s = Solver() # create a solver s >>> s.add(x_or_y) # add the clause: x or y >>> z = Bool("z") >>> s.add(Or[x,y,Not(z)]) # add another clause: x or y or !z
Calling s.check() at that point will ask the solver to find a satisfying assignment for the boolean formula built from the conjunction of all the clauses that have been added through s.add(..). In our running example, the call should return sat:
>>> s.check() sat
If the solver cannot find a satisfying assignment, then it will return unsat. In the case it returned sat, you can obtain the assignment itself with the model() method:
>>> s.model() [x = False, y = True, z = False]
And that is all you need for this tutorial, as well as for the assignment. The difficulty will be to design the encoding, not to use the solver!
You can view the video on MyMedia by clicking on the following link or watch on YouTube below:
You can see the solution for the Sudoku problem here. The python code is slightly different from the one presented in the video, but the encoding is exactly the same.
Here are a few input samples: grid0, grid1, grid2 and grid3.