News
Response to Feedback on Practical Exercise Sheet 03
Written on 13.06.2019 09:59 by Alvaro Torralba
This is in response to anonymous feedback, because given some comments in the forum I think that many students will be thinking in similar way.
1) "I don't see the point behind using an outdated language like Z3"
I'm not sure why you think that Z3 is outdated. On the contrary, this is a theorem prover being developed by Microsoft and looking at the commit history in (https://github.com/Z3Prover/z3) I see that the last commit is from 2 days ago. Indeed, what Z3 implements is even beyond what we teach in this course (you can do predicate logic and CSP, but also SAT modulo theories which is an extension of SAT).
There are two ways of using Z3. One is with the language you use in the practical exercises. The second one is through an API (in python for example). There are two good reasons for using the former: one is that many students are struggling with the python programming (remember, we have students from different backgrounds), the second reason is that it is more representative of AI where you don't tell the computer how to solve a problem by programming an algorithm but rather specify your problem in a "logic" language and let the solver deal with it.
2) "I don't see the point of forbidding usage of mod and Quantifiers."
I know that there are many people thinking like this, so let me explain the logic behind this. We need to set a limit on what you use because Z3 incorporates so many things and we want you to solve this with CSP. Also, the Sudoku exercise is not a real-world problem, it is a very artificial problem that we find good for the practical exercise because it is very simple to understand and it minimizes the chances that some constraint is missinterpreted.
Therefore, we want constraints to be as easy to understand as possible so we chose very simple mathemathical expressions (like mod). But the purpose of this exercise is that you have to think how to encode these in CSP. In that sense, we were considering quantifiers part of the predicate logic exercise and considered that it is not very difficult to write 3-4 lines of code that print out the constraints.
Regarding mathematical expressions, in the lecture we consider only binary constraints but requiring you to model everything only with binary constraints would be an overkill. So we set the middle ground in using only some operations. Note that asking you to model only constraints that can be modeled in the language in a straightforward way makes not too much sense. The idea is that you have to think how to model things. In a real world problem this will be definitively the case, you'll have some constraints that are complex and do not correspond to a single command provided by the developers of Z3.
Note that this does not make the exercise very complicated. Some students asked why division cannot be used but the truth is that a/b = c can be rewritten as a = b*c.
Nevertheless, I think that next year we'll make some changes. We'll consider allowing quantifiers and we'll remove the "mod" constraint by something like prime numbers or some other expression that does not correspond to any primitive Z3 operation. This will not make the exercise any easier but probably will be less frustrating to not be able to use one particular feature of Z3.
So, thanks for the feedback, we'll definitively consider this when designing the exercises next year.
Cheers,
Alvaro