My name is Hans Zantema and I'm employed here at the Eindhoven University of Technology. This is the building where I usually spend my days. I'm going to present the MOOC on Automated Reasoning: Satisfiability Checking. This MOOC is about satisfiability checking, also called SAT solving. Technically, that means that we check by a tool whether a particular formula is satisfiable. That means, can you give values to the variables in such a way that the formula yields true. This looks very technical, but it's a big surprise that there's a wide range of problems to which this approach can be applied. In the MOOC, we will see examples of scheduling, of solving puzzles like Sudoku, rectangle fitting as it is applied on a poster printing as we will see later, and program correctness by bounded model checking. All applications of this approach. This MOOC consists of four modules. The first two give the basics and give some examples, and the last two give the underlying theory. There are two ways to follow this MOOC. The simplest way, the light weight version, is just follow the lectures and do the corresponding quizzes. But the much more interesting way is download the tool like Z3 and solve problems yourself. For instance, in particular, you can do the honor's assignment as they are given at the end of the second module. The general principle for doing so is always first decide what are the variables you want to declare and what is their meaning, and then you generate the formula on which the tool should be applied. Typically, these formulas can be very large, but the tool can easily deal with them. So, do not type the formula yourself, but write a program generating the formula. For that, it's good to have some programming skills. About the technical content and formulas, I want to say that they are really important. Sometimes, they are quite technical, then you need more time to read them. So, don't hesitate to use the pause button to read them carefully. I hope you will enjoy it as much as I do. Good luck. Welcome to Big Impact where we will see SMT solving in practice. Albert, can you tell us where we are here. Yes, we're here at Big Impact, a large printing company in the Netherlands. We print over more than one million square meters a year, and we use SMT, the SMT software to reduce the use of material. This is the tool where the characteristics of the posters are entered, in particular, the sizes, and the nesting is designed, that is the design, how to fit them on a material. Here, SMT solving is used to do this in an optimal way, in the way as it is explained in the MOOC. The result is sent to the printer, and by the optimality, the waste of material is reduced substantially. How much do you gain by this? Well, if you consider that we print over more than one million square meters a year, and we can reduce it by let's say three percent, and that's what we do here. Then we earn 60,000 Euro. Petar, can you tell me what's your role in this? Yeah. Well, I developed the software that has been used to nest those images at the company or at least 95 percent [inaudible] here. It was a part of my Master's thesis in the [inaudible]. You developed only techniques for SMT or also other techniques? I started off with SMT based in the techniques we see in the lectures. Furthermore, I added some more algorithms. That's it. But for small mess as we see in the example here, you mainly use SMT? Yes, for smaller tasks, SMT works perfectly. Yeah.
