This short tutorial is an introduction on using Z3 as a SMT solver, and also techniques to encode problems into SMT problems. We will briefly review two theories that can be used with Z3: Linear Integer Arithmetic (LIA) and uninterpreted functions. To illustrate a problem that can be solved using LIA, we will look at the Job Shop problem. Then, we will solve a small logic problem to illustrate how functions can be used to model a seating arrangment.
As in the previous tutorial, the interface to the solver is minimal and you should be able to memorize the few functions needed. The difficulty is to design the encoding of the problem, that is, the set of formulas or constraints that act as a definition of the problem.
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 only using integer, boolean and function literals.
You should already have installed Z3 and its python API in order to complete Assignment 3 and the tutorial on SAT solving. If not, head to the the first tutorial and follow the short installation guide.
Before watching the video, you should download the starter code for the Job Shop problem example here.
You can view the video on MyMedia by clicking on the following link or watch on YouTube below:
You can see the solutions for the job shop and the seating arrangment problems. Those are slightly different than the ones presented, but you should be able to understand why these diffferences do not change the solution.