Course analysis for DD3501/FDD3501 Current Research in Proof Complexity, Winter 2011/12

Course data

Course	DD3501/FDD3501 Current Research in Proof Complexity (MSc-/PhD-level course code)
ECTS credits	9 ECTS credits
Semester/period	Winter 2011/12, periods 2-3
Examination	Problem sets; scribing of lecture notes
Lectures	22 lectures of 2 x 45 minutes (including 4 guest lectures by 3 guest lecturers)
Course literature	Research papers; lecture notes scribed by the course participants
# registered students	Not quite applicable — official registration of the course went through only towards the end of the course.
# students attending first lecture	14 students (5 MSc students; 9PhD students) plus 2 listeners
# students completing some course requirement	8 students handed in solutions to the first problem set; 1 other student scribed one of the first lectures.
# students passed	8 students in total, out of which 2 MSc students and 6 PhD students. 2 additional PhD students later took the course as a reading course.
Performance ratio (prestationsgrad)	100% according to VIS for MSc-level course DD3501; no such data available for FDD3501
Passing ratio (examinationsgrad)	100% according to VIS for MSc-level course DD3501; no such data available for FDD3501
Main instructor	Jakob Nordström
Other instructors	Guest lectures by Matti Järvisalo (Helsinki), Chris Beck (Princeton), and Samuel Lundqvist (Stockholm University)

Summary

This was an advanced course in proof complexity intended for PhD students and last-year MSc students. The course focused on recent research and open problems in proof complexity as well as on connections to applied SAT solving. Quite excitingly, it so happened that for a number of open problems stated in the introductory lectures of the course, lectures towards the end of the course covered solutions to these problems discovered while the course was being given.

The students found this to be a very challenging course (which was intentional) but also very rewarding. Comments in the course evaluation after the course (and in "opinion polls" conducted after some lectures during the course) were over all very positive. However, since this was the first time this course was given, some teething problems were inevitable. Many adjustments could be made already during the run of the course thanks to feed-back from the opinion polls, but there is also room for improvement if/when the course is given next time.

Students

The course was attended by 6 MSc students, 4 of which dropped out at an early stage, and 10 PhD students, 2 of which also dropped out fairly early. In addition, there were 2 listeners who attended lectures but did not take the course for credit.

The PhD students officially took the research-level course with course code FDD3501, but the requirements to pass were the same. The intention was that the PhD course should be graded pass/fail while the MSc course should have grades A-F, but due to an administrative error it turned out that DD3501 had also been registered as pass/fail and apparently it was not possible to correct this afterwards.

Course goals

This course was intended to

give an introduction to proof complexity (partly with a view towards connections to SAT solving),
survey some of the most recent exciting results in this area, and
present a number of open problems right at the frontier of current research,

so that that students after having completed the course

would have a good grasp of modern proof complexity,
would be able to reconstruct the proofs, at least in principle, of some of the major results during the last decade, and
would be well equipped to attack open problems in the area.

Actual course content

A fairly detailed description of the course content can be found in the schedule at www.csc.kth.se/~jakobn/teaching/proofcplx11/#schedule.

After the second lecture, the course participants voted on how much connections to practical SAT solving they wanted (slightly more than proposed in the original course planning) and on what they thought about having guest lectures on SAT solving (there was strong support for this). During the early spring semester we arranged a round of voting on what topics to cover during the final third of the course (see www.csc.kth.se/~jakobn/teaching/proofcplx11/possiblethemes.php) and mostly followed the results of this voting.

Teaching

The course was given in periods 2 and 3 during 2011/12. There were 11 lectures (of 2 x 45 minutes) in period 2 and 11 lectures in period 3. Out of the 22 lectures, there were a total of 4 guest lectures by

Matti Järvisalo (Helsinki) on SAT solvers based on resolution/conflict-driven clause learning,
Chris Beck (Princeton) on time-space trade-offs in proof complexity,
Samuel Lundqvist (Stockholm University) on algebraic SAT solving using Gröbner bases.

The students were very happy with the quality of the regular lectures. For the guest lectures the reviews were somewhat mixed (some were considered very good but some less so), but the students considered guest lectures as such to be a good idea.

All lectures were given in English.

Examination

The course examination was done by 5 problem sets and by scribing of 1-2 lectures.

Using problem sets is the traditional way of examining advanced TCS courses. The students found the problems challenging but interesting, and seemed mostly happy with this form of examination. A couple of students suggested that there should be more frequent and smaller problem sets rather than a few big ones. One slightly non-standard feature of the problem sets was that we experimented with the possibility of "buying hints" for the problems. This set-up was described as follows on the course webpage: "For most of the problems, it will be possible to purchase 'hints' for a certain deduction from the max score of the problem. In this way, you can configure yourself whether you want the problems to be more creative and open-ended, where sometimes a lot can depend on finding the right idea, or whether you want them to be more of guided exercises providing a useful work-out on the concepts of proof complexity. Please feel free to use (or not use) this possibility to make the course more interesting and rewarding for you." This option was exercised for some problems by some students, but was not very frequently used. One comment in the course evaluation found that it was hard to know how to deal with the option of buying hints, although the idea as such seemed good.

The decision to scribe lecture notes, and to have this as a form of examination, was taken after a vote by course participants after the second lecture on the course. An overwhelming majority of the students found the process of scribing fairly or very useful, and even more students found the notes very useful for purposes of self-study. One problem with having scribed lecture notes was that this turned out to be very labour-intensive for the lecturer in the end, since even after a couple of iterations there were still many issues with the notes that needed to be fixed before the notes could be publicly published on the course webpage. For roughly the final third of lectures, the notes never made it into a polished enough state to publish, and were instead distributed informally to the students.

Course literature

The course contents covered recent research in proof complexity, and there was no textbook, or even survey article, that could be used as course literature. Instead, lectures were based on research articles (published and in preparation) and as mentioned above students also used the scribe notes for self-study.

Prerequisites

In the prerequisites on the course webpage, it said that "[t]his course is open to anyone, but the main target audience are grad students and advanced undergrads. Some background in computational complexity theory and/or discrete mathematics will probably be helpful, but all that should really be needed is 'mathematical maturity' and a willingness to learn new stuff." Students found this to be a reasonable description.

Changes from last time the course was given

Not applicable — this was the first time the course was given.

Course evaluation

The course was evaluated by a course evaluation conducted after the course (to which 8 students answered, 7 of which had passed the course) as well as on a number of "opinion polls" conducted at various intervals during the (first half of) the course, namely on October 27, October 31, November 28, and December 5. These opinion polls were also used to adjust the course planning as we went along.

The above documents contain a wealth of information concerning what students thought about the course. Below follows an attempt at a brief summary. (The percentages do not always round to 100% in the ACE evaluation tool used but have been left as computed by the tool.)

75% of respondents found the course hard or very hard, but 100% also found it fairly or very interesting. It was reasonably clear what the course goals and prerequisites were, and all students considered themselves to have the required prerequisites.

88% of students referred to the course webpage on a weekly basis or more often, and 100% found the webpages fairly or very good. 76% appreciated the course opinion polls and one commenter said it made the course feel configurable depending on student preferences, as the instructor had promised. Another comment was that it would have been good to have opinion polls also during the second half of the course (which we did not do, although we did have a vote on the content of the final third of the course as mentioned above).

Lectures were well-attended — 75% of students attended more than 80% of the lectures. The number of lectures was considered to be appropriate. 88% found the regular (non-guest) lectures good or very good from a pedagogical point of view. 63% found the pace about right, 25% found it a bit too fast and 13% way too fast. Judging from the opinion polls, MSc students found the pace of the lectures a bit more challenging than the PhD students, which seems natural. Some lectures were given with slides but most were on the board. 50% wanted to keep it that way and 25% had no particular opinion (this is similar to the replies to the same question during an opinion poll barely halfway through the course). In the comments, the students especially liked brief recaps at the start of each lecture what we did last time. A summary of the lecture at the end would also have been nice, but often we struggled to find time for that. The students thought that it was good to have guest lectures. Matti Järvisalo got very good grades for his lecture; Chris Beck and Samuel Lundqvist slightly less so.

The process of scribing lecture notes was very useful to 38% of the respondents and fairly useful to 50%. 75% found it very useful and 25% fairly useful to have the notes available for self-study. From the comments, however, it is clear that students found the task of scribing quite challenging, and one commenter raises the issue of whether the notes were worth the amount of time and work invested.

The problem sets were considered to be fairly hard (63%) or very hard (38%). 63% considered the hardness level to be appropriate, however, while 25% found the problems a bit too hard and 13% far too hard. Again, MSc students appeared to feel that problems were harder than PhD students. The content of the problem sets was assessed to correspond well to the contents of the lectures. The number of problems and problem sets and the grading was "about right" according to a clear majority. The time given to solve the problems was about right or sometimes a bit too short (but we had votes about deadline extensions and extended accordingly when students so wished). The balance between theoretical and practical problems was about right. Most students assessed that they spent 30-40 hours of work per problem set. One commenter suggested splitting the problem sets into more, smaller set. Two commenters would have wanted the first problem set to have appeared earlier in the course.

88% of the students spent 30-50% of their total study/working time on the course while it was being given. 38% think that 9 ECTS credits was about right, but 63% feel that more than 9 credits would have been appropriate.

38% felt that a course like this should definitely be given on a regular basis (say, every second or third year) at KTH, and 25% thought that this should probably be the case. 25% were neutral and 13% thought that such a course should probably not be given on a regular basis.

According to the replies in the course evaluation, most aspects of the course should stay the same if the course is to be given again. The same question was also asked in an opinion poll halfway through the course, and the replies there mentioned the scribing, the choice of topics, the quality and speed of presentation during lectures, and the problem sets were all aspects that should stay the same.

As to suggestions for improvements, comments in the course evaluation mentioned that the number of ECTS credits could be increased. One commenter instead suggested lowering the ambitions of the course. One commenter was unhappy about the rules for the problem sets where students were allowed to work in pairs but not in larger groups. In the opinion poll halfway through the course, some suggestions for improvements were more frequent problem sets or fewer problems, recommendations on what to read before lectures, lowering the ambitions of the course a bit, and having less of recap at beginning of lectures (contradicting feed-back from other students as mentioned above).

Conclusions and future changes

All in all, this seems to have been a successful course. One central question, of course, is to what extent we could and should offer advanced, research-level courses at KTH CSC. But if we want MSc students to come into contact with research, which seems to be the officially stated goal, then that is an argument for giving this kind of courses. And given the result of the course evaluation and the opinion polls, it seems that things should be kept mostly the same if the course is to be given again.

However, some changes should also be considered as follows:

The content of the course would need to be substantially updated, since there have been continued quite dynamic developments in this research area.
The lecture on algebraic SAT solving was not very good and would need to be improved. Also, it would seem relevant to add another lecture about geometric SAT solvers based on cutting planes (so-called pseudo-Boolean solvers).
The grading on the MSc-level version of the course should be changed from pass/fail to A-F and the requirement to pass (E) should be lowered as compared to the passing grade in this offering of the course (for both MSc- and PhD-level).
Having students scribe lecture notes seems worth-while, but the amount of work needs to be decreased both for the students and the instructor. For some of the lectures, the already existing scribe notes could be reused for the next course offering. For the other lectures, one idea would be to have two students sign up to scribe each lecture. After the lecture the instructor could randomly assign one of the students to do the initial scribing and the other student to do a round of careful reviewing and suggest revisions. Once the lecture notes have been revised in response to the comments by the second student as the first student deems appropriate, the instructor could then look at both the initial draft with reviewing comments and the final version. This should help students learn more, since they would not only work on exposition (during scribing and problem sets) but also on reviewing, and if the final version from the students is in better shape this should hopefully also save time for the instructor.
Regarding problem sets, it seems worth considering having smaller and more frequent problem sets. Posting the first problem set early on during the course to get the students started on studying the course material right away seems like a good idea. One other approach that has been tried at other advanced TCS courses and seems appropriate for this course as well would be to have written peer evaluation of problem set solutions before final grading by the instructor. If the system with buying hints for problems is to be kept, there might be some thinking needed on how to configure this in a better way for the students. One idea could be to publish all hints for a problem set after the deadline, so that students can see what the hints looked like and what to expect for the next problem set.

One final remark is that the big challenge when organizing an advanced course like this is financing (and this holds true for other advanced TCS courses as well). This time, the course was paid for by the instructor's own research grants. It is not clear that this is a sustainable, long-term model of funding, but on the other hand it also seems hard to find money from the education budget for this kind of courses. This seems unfortunate, since one explicit goal of our education of MSc students is to get more connections to research in their courses, and this course was about as research-connected as it gets.