This lecture is about planning-scheduling by SAT-SMT. Projects to plan or schedule typically split up into parts, let's call these parts jobs and you might think of all kind of project. If you build a house you can split up the jobs to be done before the house is finished. But if you develop software you can also split up the work to be done into jobs and to show that for all of these jobs we already know or can estimate the running time for it. We have to decide which job should start at which moment. Typical requirements that you meet is that some jobs should run before others. For instance, if you build a house it's quite obvious that you can not put the roof on it before the underlying floors have been finished. If you develop software one of the job could be testing software while you cannot run tests of software if the software is not yet there. So, it's quite obvious that in many situations you have that some jobs should run before another job. Next you could think of assigning people to jobs. You can also think of jobs that should run in a particular period, for instance, if they need a special resource of limited available. If you build a house and you should hire a crane, well, that you do that's for a limited period since it's quite expensive and then the parts of the jobs that need to the crane should be scheduled in these parallels. You can sometimes have that jobs may run in parallel or they may not run in parallel. For instance, if they need a special tool of which only one copy is available then two jobs may not run in parallel, both needing this special tool and many other jobs like requirements like these. Let's give an example. We have eight jobs numbered from 1-8 and let's say job one has a running time four, job two has running time five and so on until job eight having a running time 11. Each job should be executed by one of three persons, let's call them A, B and C. Jobs one and four need the specialism of person B, so they should be done both by person B. Job two should run after job six and job seven have finished. Well, then here we see a possible solution and total running time 21. Indeed, you see that two runs after six and seven have finished and both one and four are executed by person B. So, all the requirements hold. In fact, this is an optimal solution since this solution was found by approach I will just sketch in a minute. How to solve this? Well, of course we will use an SMT-solver, we will specified the problem in a formula and then called the SMT-solver. For every job typically we introduce the start time, the end time, and a person to execute it. Well, and then we should specify the requirements. As we said, we assume that for every job we have the running time. So for a job I, we can write down the end i minus the start of i is this given running time and that is what we do for every job. If we have a requirement of the shape, job j should run after job i has finished. We just write down the inequality S j should be greater or equal than E i. The start of j should be at least the end time of i. If i and j are not allowed to run in parallel for instance if I need a shared resource, then we get a requirement. S j is greater or equal than E i specify that j is after i or the other way around, S i is greater or equal than E j meaning that i is after j. Well, if we have n persons available we numbered them from 1-n and we write down the requirement that P i is greater or equal than one and less or equal than n for all jobs i. If job i should be executed by person B we simply write down P i is p. At every moment every person is involved in at most one job. It's not allowed, well, maybe in some variants but in the basic setting, it's not allowed that one person can do two jobs at the same time. That can be expressed in this formula. If P i is P j stating that i and j are executed by the same person, then, these jobs i and j should not run at the same time, they should not run in parallel. So, either j should run after E which is the requirement S j greater or equal E i or the other way around. This is the formula stating that i and j, if they are by the same person they are do not run in parallel. If we write down this requirement for all jobs i less than j, we have the full requirement at every moment every person is involved in at most one job. The next question is we want to minimize the total running time. How to do that? Well, let's introduce a variable T for the total running time and add requirements that. Well, all jobs should start greater or equal than zero. If we define zero as the start moment then all jobs should end before t. So, if we have this requirement for all jobs i, we know that this job runs between zero and T. Now, we want the smallest value of T such that the total formula is satisfiable. How to do that? Well, that can be done in two different ways. We can simply add the requirement T is v for several values of v and every time run SMT solver until we find a value of v for which it is satisfiable while for a v minus one it is unsatisfiable and then we know that v is the smallest value for which it holds. How to do this, well if we apply binary search it can be done quite quickly. Another easier approach is used the built in feature minimize that is available in some SMT solvers. To conclude by just introducing variables for starting times of the jobs and specifying all the requirements in these variables SMT solvers succeed in solving scheduling problems. Several variants are possible. You may think of finding class schedules for school and many other kinds of pleading and schedule the problems. Unfortunately, it does not always scale up, if you have a very big problem you should not expect that this approach, but for a limited size problems it can be a fruitful approach. Thank you.