Advanced Topics in Logic: Automated Reasoning and Satisfiability

Course Overview

Automated reasoning has become a powerful technology with applications ranging from verification of hardware and software to solving long-standing open problems in mathematics. This course covers several state-of-the-art automated reasoning techniques and provides hands-on experience with research questions in this area. Along the way, students will learn how to:

The course has two phases. The first phase consists of lectures and three (individual) homework assignments. In the second phase, students team up in groups of 2-3 to work on a joint project related to a research question. The final project should be described in a report in the style of a scientific paper.

The Fall 2019 course resulted in several papers that have been accepted at conferences or that are currently under submission. Two accepted papers are available below. One of them received the best student paper award at the International Conference on Theory and Applications of Satisfiability Testing 2020.

Emre Yolcu, Xinyu Wu, and Marijn J. H. Heule (2020).
Mycielski graphs and PR proofs.
In Theory and Practice of Satisfiability Testing - SAT 2020, pp. 201-217.
Lecture Notes in Computer Science 12178, Spinger. Best student paper award [pdf, doi]



Peter Oostema, Ruben Martins, and Marijn J. H. Heule (2020).
Coloring Unit-Distance Strips using SAT.
In Logic for Programming, Artificial Intelligence and Reasoning - LPAR-23, pp. 373-389.
EPiC Series in Computing 73, EasyChair. [pdf, doi]

Logistics

Zoom links (password via email):

Instructor: Marijn Heule and Ruben Martins

Lectures: MoWe 3:20-4:40pm (remote via zoom).
In this course, being able to see one another helps to facilitate a better learning environment and promote more engaging discussions. Therefore, our default will be to expect students to have their cameras on during lectures and discussions. However, we also completely understand there may be reasons students would not want to have their cameras on. If you have any concerns about sharing your video, please email me as soon as possible and we can discuss possible adjustments.

Grading: Grades are based on three homework assignments (15% × 3 = 45%), final project (45%), and participation (10%). The final project should raise novel research questions and provide some nontrivial answers. These projects should be described in a report and presented in class at the end of the semester.

Late policy: Homework assignments that are submitted late will be penalized by subtracting 5 points per day (10%).

Academic Integrity: Students are expected to complete each homework assignment on their own, and should be able to explain all of the work that they hand in. Copying material from other students or online sources is not allowed. If you have questions about whether something might be an issue, contact the course staff before discussing further. Please refer to the Carnegie Mellon Code for information about university policies regarding academic conduct.

Take care of yourself: Do your best to maintain a healthy lifestyle this semester by eating well, exercising, avoiding drugs and alcohol, getting enough sleep and taking some time to relax. This will help you achieve your goals and cope with stress. All of us benefit from support during times of struggle. You are not alone. There are many helpful resources available on campus and an important part of the college experience is learning how to ask for help. Asking for support sooner rather than later is often helpful. If you or anyone you know experiences any academic stress, difficult life events, or feelings like anxiety or depression, we strongly encourage you to seek support. Counseling and Psychological Services (CaPS) is here to help: call 412-268-2922 and visit their website. Consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.