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.
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 need to pass the 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!