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 and Fall 2020 courses resulted in several papers that have been accepted at conferences or that are currently under submission. The accepted papers are shown below. One of them received the best student paper award at the International Conference on Theory and Applications of Satisfiability Testing 2020.

Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J.H. Heule, and Armin Biere (2021).
XOR Local Search for Boolean Brent Equations.
In Theory and Practice of Satisfiability Testing - SAT 2021, 417-435.
Lecture Notes in Computer Science 12831, Springer. [pdf, slides, recording, doi]

Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen (2021).
cake_lpr: Verified Propagation Redundancy Checking in CakeML.
In Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2021, pp. 223-241.
Lecture Notes in Computer Science 12651, Springer. [pdf, doi]

Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule (2021).
A Flexible Proof Format for SAT Solver-Elaborator Communication.
In Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2021, pp. 59-75.
Lecture Notes in Computer Science 12651, Springer. [pdf, doi]

Cayden Codel, Joseph Reeves, Marijn J. H. Heule and Randal E. Bryant (2021).
Bipartite Perfect Matching Benchmarks.
Accepted for Pragmatics of SAT (PoS'21). [pdf]

Changjian Zhang, Ryan Wagner, Pedro Orvalho, David Garlan, Vasco Manquinho, Ruben Martins, and Eunsuk Kang (2021).
AlloyMax: Bringing Maximum Satisfaction to Relational Specifications.
In European Software Engineering Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2021, pp. 155–167.
Distinguished Paper Award [pdf, doi]

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

Instructor: Marijn Heule

Lectures: MoWe 10:10-11:30pm in GHC 4303. First lecture on September 8.

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.