One of the most exciting developments in computational social choice in recent years has been the use of tools for automated reasoning developed in AI, notably SAT solvers, to support researchers in social choice theory in their quest of getting a deeper understanding of the axiomatic foundations of collective decision making. In this project course, we are going to explore this approach in depth.
The course has three parts. The first part will consist of a couple of lectures introducing the approach, together with a complex hands-on exercise. In the second part, each participant will study a relevant paper from the literature and present it in the form of a seminar talk. In the final part, which will take up most of the time, you will work in small groups and try to identify an interesting research problem that can be tackled using the approach, work on that problem, and write up your results in the form of a paper. Along the way, there will be opportunities to practice giving talks, writing papers, and reviewing papers.
| Friday 24 September 2021 13:00-15:00, Room F1.15 |
Introductory lecture (slides, code). We'll mostly see how to automate proving the "base case" of the Gibbard-Satterthwaite Theorem using a SAT solver. If necessary, remind yourself what the G-S Theorem is. Bring your laptop and make sure you can use pylgl. |
| Friday 1 October 2021 16:00-17:00, Room D1.110 |
Talk by Oliviero Nardi in the COMSOC Seminar. Not part of the course, but relevant. |
| Tuesday 5 October 2021 16:00-18:00, Room F1.15 |
Second lecture (slides, code). We'll start with discussing your solutions to the Duggan-Schwartz exercise. Then we'll talk about inductive proofs to generalise base cases to full impossibility theorems, and about MUS extraction as a means of constructing human-readable proofs. Please install PicoSAT beforehand. |
| Monday 11 October 2021 16:00-18:00, Room F1.15 |
Two talks on papers:
|
| Monday 18 October 2021 16:00-18:00, Room F1.15 |
Two talks on papers:
|
| Monday 25 October 2021 15:15-16:15, Room F1.15 |
Just one talk today:
|
| Thursday 11 November 2021 11:15-13:00, Room F1.15 |
The final talk on papers, followed by the third lecture:
|
| Thursday 25 November 2021 13:45-17:30, Belle van Zuylenzaal |
Workshop on Social Choice Theory. Not part of the course, but relevant. |
| Friday 3 December 2021 12:00-13:00, Room F1.15 |
Plenary progress meeting. |
| Thursday, 20 January 2022 14:00-16:00, Room F3.20 |
Final presentations. |
For your final paper, please follow the formatting instructions of IJCAI-2022. Your paper can be shorter than what those guidelines permit, but it should not be longer. Structure your paper, and more generally try to make it look, like a typical COMSOC paper published in the proceeding sof an AI conference. As you work on your manuscript, please take note of my suggestions for how to write a paper.
Make your code available via public GitHub repository or similar, and include a link to that repository in your paper. Provide a reasonable level of documentation with your code. Keep in mind that your main deliverable is the paper; a reader should be able to understand and appreciate the paper without actually looking through the code.
As an intermediate step, each group will produce a 2-page draft, consisting of most of Section 2 ("The Model"), a few sentences of motivation (from Section 1), and a bullet list of any results you have already (without proof or detailed explanation). For each draft, everyone not involved in writing it will produce a short anonymous review (see how to write a review). Don't discuss the reviews with each other as you are writing them, so we really get independent opinions.
At the end, each group will give a presentation of their work in the form of a research seminar (see how to give a talk). Prepare for roughly 30 minutes of presentation, followed by 15 minutes of questions.
Deadlines:
Below is a selection of papers using the SAT-based approach to obtain axiomatic results in social choice theory and a couple of closely related fields. This list covers most of the contributions in this area to date.