Getting started with z3
You can either use z3 online here or install it on your computer following the instructions on Z3's Github repository.
If you want to do some background reading, you can start here but the tutorial should be self contained. We will use the SMT-LIB v2 language to write our formulas and specify the problem for the solver, but you don't need to read the whole manual and we will use only a small subset of the language.
We will start by trying to solve the N-queens puzzle. The goal here is to understand how to encode a problem into a SAT problem. There is no great difficulty and we'll use a very small subset of SMT-LIB v2, but that's a good warm-up.
For the Job Shop scheduling problem, we need something more involved than propositional formulas. Another NP-hard problem that you will solve with the power of an SMT solver!